multop_1.miz

    begin

    definition

      let f be Function;

      let a,b,c be object;

      :: MULTOP_1:def1

      func f . (a,b,c) -> set equals (f . [a, b, c]);

      correctness ;

    end

    reserve A,B,C,D,E for non empty set,

a for Element of A,

b for Element of B,

c for Element of C,

d for Element of D,

X,Y,Z,S for set,

x,y,z,s,t for object;

    definition

      let A, B, C, D;

      let f be Function of [:A, B, C:], D;

      let a, b, c;

      :: original: .

      redefine

      func f . (a,b,c) -> Element of D ;

      coherence

      proof

        (f . [a, b, c]) is Element of D;

        hence thesis;

      end;

    end

    theorem :: MULTOP_1:1



     Th1: for f1,f2 be Function of [:X, Y, Z:], D st for x, y, z st x in X & y in Y & z in Z holds (f1 . [x, y, z]) = (f2 . [x, y, z]) holds f1 = f2

    proof

      let f1,f2 be Function of [:X, Y, Z:], D such that

       A1: for x, y, z st x in X & y in Y & z in Z holds (f1 . [x, y, z]) = (f2 . [x, y, z]);

      for t be object st t in [:X, Y, Z:] holds (f1 . t) = (f2 . t)

      proof

        let t be object;

        assume t in [:X, Y, Z:];

        then ex x, y, z st x in X & y in Y & z in Z & t = [x, y, z] by MCART_1: 68;

        hence thesis by A1;

      end;

      hence thesis by FUNCT_2: 12;

    end;

    theorem :: MULTOP_1:2



     Th2: for f1,f2 be Function of [:A, B, C:], D st for a, b, c holds (f1 . [a, b, c]) = (f2 . [a, b, c]) holds f1 = f2

    proof

      let f1,f2 be Function of [:A, B, C:], D;

      assume for a, b, c holds (f1 . [a, b, c]) = (f2 . [a, b, c]);

      then for x, y, z st x in A & y in B & z in C holds (f1 . [x, y, z]) = (f2 . [x, y, z]);

      hence thesis by Th1;

    end;

    theorem :: MULTOP_1:3

    for f1,f2 be Function of [:A, B, C:], D st for a be Element of A holds for b be Element of B holds for c be Element of C holds (f1 . (a,b,c)) = (f2 . (a,b,c)) holds f1 = f2

    proof

      let f1,f2 be Function of [:A, B, C:], D such that

       A1: for a be Element of A holds for b be Element of B holds for c be Element of C holds (f1 . (a,b,c)) = (f2 . (a,b,c));

      for a be Element of A holds for b be Element of B holds for c be Element of C holds (f1 . [a, b, c]) = (f2 . [a, b, c])

      proof

        let a be Element of A;

        let b be Element of B;

        let c be Element of C;

        (f1 . (a,b,c)) = (f1 . [a, b, c]) & (f2 . (a,b,c)) = (f2 . [a, b, c]);

        hence thesis by A1;

      end;

      hence thesis by Th2;

    end;

    definition

      let A be set;

      mode TriOp of A is Function of [:A, A, A:], A;

    end

    scheme :: MULTOP_1:sch1

    FuncEx3D { X,Y,Z,T() -> non empty set , P[ object, object, object, object] } :

ex f be Function of [:X(), Y(), Z():], T() st for x be Element of X() holds for y be Element of Y() holds for z be Element of Z() holds P[x, y, z, (f . [x, y, z])]

      provided

       A1: for x be Element of X() holds for y be Element of Y() holds for z be Element of Z() holds ex t be Element of T() st P[x, y, z, t];

      defpred Q[ set, set] means (for x be Element of X(), y be Element of Y(), z be Element of Z() st $1 = [x, y, z] holds P[x, y, z, $2]);



       A2: for p be Element of [:X(), Y(), Z():] holds ex t be Element of T() st Q[p, t]

      proof

        let p be Element of [:X(), Y(), Z():];

        consider x1,y1,z1 be object such that

         A3: x1 in X() and

         A4: y1 in Y() and

         A5: z1 in Z() and

         A6: p = [x1, y1, z1] by MCART_1: 68;

        reconsider z1 as Element of Z() by A5;

        reconsider y1 as Element of Y() by A4;

        reconsider x1 as Element of X() by A3;

        consider t be Element of T() such that

         A7: P[x1, y1, z1, t] by A1;

        take t;

        let x be Element of X(), y be Element of Y(), z be Element of Z();

        assume

         A8: p = [x, y, z];

        then x1 = x & y1 = y by A6, XTUPLE_0: 3;

        hence thesis by A6, A7, A8, XTUPLE_0: 3;

      end;

      consider f be Function of [:X(), Y(), Z():], T() such that

       A9: for p be Element of [:X(), Y(), Z():] holds Q[p, (f . p)] from FUNCT_2:sch 3( A2);

      take f;

      let x be Element of X();

      let y be Element of Y();

      let z be Element of Z();

      thus thesis by A9;

    end;

    scheme :: MULTOP_1:sch2

    TriOpEx { A() -> non empty set , P[ Element of A(), Element of A(), Element of A(), Element of A()] } :

ex o be TriOp of A() st for a,b,c be Element of A() holds P[a, b, c, (o . (a,b,c))]

      provided

       A1: for x,y,z be Element of A() holds ex t be Element of A() st P[x, y, z, t];

      defpred Q[ Element of A(), Element of A(), Element of A(), Element of A()] means for r be Element of A() st r = $4 holds P[$1, $2, $3, r];



       A2: for x,y,z be Element of A() holds ex t be Element of A() st Q[x, y, z, t]

      proof

        let x,y,z be Element of A();

        consider t be Element of A() such that

         A3: P[x, y, z, t] by A1;

        take t;

        thus thesis by A3;

      end;

      consider f be Function of [:A(), A(), A():], A() such that

       A4: for a,b,c be Element of A() holds Q[a, b, c, (f . [a, b, c])] from FuncEx3D( A2);

      take f;

      let a,b,c be Element of A();

      thus thesis by A4;

    end;

    scheme :: MULTOP_1:sch3

    Lambda3D { X,Y,Z,T() -> non empty set , F( Element of X(), Element of Y(), Element of Z()) -> Element of T() } :

ex f be Function of [:X(), Y(), Z():], T() st for x be Element of X() holds for y be Element of Y() holds for z be Element of Z() holds (f . [x, y, z]) = F(x,y,z);

      defpred Q[ Element of X(), Element of Y(), Element of Z(), Element of T()] means $4 = F($1,$2,$3);



       A1: for x be Element of X() holds for y be Element of Y() holds for z be Element of Z() holds ex t be Element of T() st Q[x, y, z, t];

      ex f be Function of [:X(), Y(), Z():], T() st for x be Element of X() holds for y be Element of Y() holds for z be Element of Z() holds Q[x, y, z, (f . [x, y, z])] from FuncEx3D( A1);

      hence thesis;

    end;

    scheme :: MULTOP_1:sch4

    TriOpLambda { A,B,C,D() -> non empty set , O( Element of A(), Element of B(), Element of C()) -> Element of D() } :

ex o be Function of [:A(), B(), C():], D() st for a be Element of A(), b be Element of B(), c be Element of C() holds (o . (a,b,c)) = O(a,b,c);

      consider f be Function of [:A(), B(), C():], D() such that

       A1: for a be Element of A(), b be Element of B(), c be Element of C() holds (f . [a, b, c]) = O(a,b,c) from Lambda3D;

      take f;

      let a be Element of A(), b be Element of B(), c be Element of C();

      thus thesis by A1;

    end;

    definition

      let f be Function;

      let a,b,c,d be set;

      :: MULTOP_1:def2

      func f . (a,b,c,d) -> set equals (f . [a, b, c, d]);

      correctness ;

    end

    definition

      let A, B, C, D, E;

      let f be Function of [:A, B, C, D:], E;

      let a, b, c, d;

      :: original: .

      redefine

      func f . (a,b,c,d) -> Element of E ;

      coherence

      proof

        (f . [a, b, c, d]) is Element of E;

        hence thesis;

      end;

    end

    theorem :: MULTOP_1:4



     Th4: for f1,f2 be Function of [:X, Y, Z, S:], D st for x, y, z, s st x in X & y in Y & z in Z & s in S holds (f1 . [x, y, z, s]) = (f2 . [x, y, z, s]) holds f1 = f2

    proof

      let f1,f2 be Function of [:X, Y, Z, S:], D such that

       A1: for x, y, z, s st x in X & y in Y & z in Z & s in S holds (f1 . [x, y, z, s]) = (f2 . [x, y, z, s]);

      for t be object st t in [:X, Y, Z, S:] holds (f1 . t) = (f2 . t)

      proof

        let t be object;

        assume t in [:X, Y, Z, S:];

        then ex x, y, z, s st x in X & y in Y & z in Z & s in S & t = [x, y, z, s] by MCART_1: 79;

        hence thesis by A1;

      end;

      hence thesis by FUNCT_2: 12;

    end;

    theorem :: MULTOP_1:5



     Th5: for f1,f2 be Function of [:A, B, C, D:], E st for a, b, c, d holds (f1 . [a, b, c, d]) = (f2 . [a, b, c, d]) holds f1 = f2

    proof

      let f1,f2 be Function of [:A, B, C, D:], E;

      assume for a, b, c, d holds (f1 . [a, b, c, d]) = (f2 . [a, b, c, d]);

      then for x, y, z, s st x in A & y in B & z in C & s in D holds (f1 . [x, y, z, s]) = (f2 . [x, y, z, s]);

      hence thesis by Th4;

    end;

    theorem :: MULTOP_1:6

    for f1,f2 be Function of [:A, B, C, D:], E st for a, b, c, d holds (f1 . (a,b,c,d)) = (f2 . (a,b,c,d)) holds f1 = f2

    proof

      let f1,f2 be Function of [:A, B, C, D:], E such that

       A1: for a, b, c, d holds (f1 . (a,b,c,d)) = (f2 . (a,b,c,d));

      for a, b, c, d holds (f1 . [a, b, c, d]) = (f2 . [a, b, c, d])

      proof

        let a, b, c, d;

        (f1 . (a,b,c,d)) = (f1 . [a, b, c, d]) & (f2 . (a,b,c,d)) = (f2 . [a, b, c, d]);

        hence thesis by A1;

      end;

      hence thesis by Th5;

    end;

    definition

      let A;

      mode QuaOp of A is Function of [:A, A, A, A:], A;

    end

    scheme :: MULTOP_1:sch5

    FuncEx4D { X,Y,Z,S,T() -> non empty set , P[ object, object, object, object, object] } :

ex f be Function of [:X(), Y(), Z(), S():], T() st for x be Element of X() holds for y be Element of Y() holds for z be Element of Z() holds for s be Element of S() holds P[x, y, z, s, (f . [x, y, z, s])]

      provided

       A1: for x be Element of X() holds for y be Element of Y() holds for z be Element of Z() holds for s be Element of S() holds ex t be Element of T() st P[x, y, z, s, t];

      defpred Q[ set, set] means for x be Element of X(), y be Element of Y(), z be Element of Z(), s be Element of S() st $1 = [x, y, z, s] holds P[x, y, z, s, $2];



       A2: for p be Element of [:X(), Y(), Z(), S():] holds ex t be Element of T() st Q[p, t]

      proof

        let p be Element of [:X(), Y(), Z(), S():];

        consider x1,y1,z1,s1 be object such that

         A3: x1 in X() and

         A4: y1 in Y() and

         A5: z1 in Z() and

         A6: s1 in S() and

         A7: p = [x1, y1, z1, s1] by MCART_1: 79;

        reconsider s1 as Element of S() by A6;

        reconsider z1 as Element of Z() by A5;

        reconsider y1 as Element of Y() by A4;

        reconsider x1 as Element of X() by A3;

        consider t be Element of T() such that

         A8: P[x1, y1, z1, s1, t] by A1;

        take t;

        let x be Element of X(), y be Element of Y(), z be Element of Z(), s be Element of S();

        assume

         A9: p = [x, y, z, s];

        then

         A10: z1 = z by A7, XTUPLE_0: 5;

        x1 = x & y1 = y by A7, A9, XTUPLE_0: 5;

        hence thesis by A7, A8, A9, A10, XTUPLE_0: 5;

      end;

      consider f be Function of [:X(), Y(), Z(), S():], T() such that

       A11: for p be Element of [:X(), Y(), Z(), S():] holds Q[p, (f . p)] from FUNCT_2:sch 3( A2);

      take f;

      let x be Element of X();

      let y be Element of Y();

      let z be Element of Z();

      let s be Element of S();

      thus thesis by A11;

    end;

    scheme :: MULTOP_1:sch6

    QuaOpEx { A() -> non empty set , P[ Element of A(), Element of A(), Element of A(), Element of A(), Element of A()] } :

ex o be QuaOp of A() st for a,b,c,d be Element of A() holds P[a, b, c, d, (o . (a,b,c,d))]

      provided

       A1: for x,y,z,s be Element of A() holds ex t be Element of A() st P[x, y, z, s, t];

      defpred Q[ Element of A(), Element of A(), Element of A(), Element of A(), Element of A()] means for r be Element of A() st r = $5 holds P[$1, $2, $3, $4, $5];



       A2: for x,y,z,s be Element of A() holds ex t be Element of A() st Q[x, y, z, s, t]

      proof

        let x,y,z,s be Element of A();

        consider t be Element of A() such that

         A3: P[x, y, z, s, t] by A1;

        take t;

        thus thesis by A3;

      end;

      consider f be Function of [:A(), A(), A(), A():], A() such that

       A4: for a,b,c,d be Element of A() holds Q[a, b, c, d, (f . [a, b, c, d])] from FuncEx4D( A2);

      take f;

      let a,b,c,d be Element of A();

      thus thesis by A4;

    end;

    scheme :: MULTOP_1:sch7

    Lambda4D { X,Y,Z,S,T() -> non empty set , F( Element of X(), Element of Y(), Element of Z(), Element of S()) -> Element of T() } :

ex f be Function of [:X(), Y(), Z(), S():], T() st for x be Element of X() holds for y be Element of Y() holds for z be Element of Z() holds for s be Element of S() holds (f . [x, y, z, s]) = F(x,y,z,s);

      defpred P[ Element of X(), Element of Y(), Element of Z(), Element of S(), Element of T()] means $5 = F($1,$2,$3,$4);



       A1: for x be Element of X() holds for y be Element of Y() holds for z be Element of Z() holds for s be Element of S() holds ex t be Element of T() st P[x, y, z, s, t];

      ex f be Function of [:X(), Y(), Z(), S():], T() st for x be Element of X() holds for y be Element of Y() holds for z be Element of Z() holds for s be Element of S() holds P[x, y, z, s, (f . [x, y, z, s])] from FuncEx4D( A1);

      hence thesis;

    end;

    scheme :: MULTOP_1:sch8

    QuaOpLambda { A() -> non empty set , O( Element of A(), Element of A(), Element of A(), Element of A()) -> Element of A() } :

ex o be QuaOp of A() st for a,b,c,d be Element of A() holds (o . (a,b,c,d)) = O(a,b,c,d);

      deffunc F( Element of A(), Element of A(), Element of A(), Element of A()) = O($1,$2,$3,$4);

      consider f be Function of [:A(), A(), A(), A():], A() such that

       A1: for a,b,c,d be Element of A() holds (f . [a, b, c, d]) = F(a,b,c,d) from Lambda4D;

      take f;

      let a,b,c,d be Element of A();

      thus thesis by A1;

    end;