:: MULTOP_1 semantic presentation begin definition let f be Function; let a, b, c be set ; funcf . (a,b,c) -> set equals :: MULTOP_1:def 1 f . [a,b,c]; correctness coherence f . [a,b,c] is set ; ; end; :: deftheorem defines . MULTOP_1:def_1_:_ for f being Function for a, b, c being set holds f . (a,b,c) = f . [a,b,c]; definition let A, B, C, D be non empty set ; let f be Function of [:A,B,C:],D; let a be Element of A; let b be Element of B; let c be Element of C; :: original: . redefine funcf . (a,b,c) -> Element of D; coherence f . (a,b,c) is Element of D proof f . [a,b,c] is Element of D ; hence f . (a,b,c) is Element of D ; ::_thesis: verum end; end; theorem Th1: :: MULTOP_1:1 for D being non empty set for X, Y, Z being set for f1, f2 being Function of [:X,Y,Z:],D st ( for x, y, z being set st x in X & y in Y & z in Z holds f1 . [x,y,z] = f2 . [x,y,z] ) holds f1 = f2 proof let D be non empty set ; ::_thesis: for X, Y, Z being set for f1, f2 being Function of [:X,Y,Z:],D st ( for x, y, z being set st x in X & y in Y & z in Z holds f1 . [x,y,z] = f2 . [x,y,z] ) holds f1 = f2 let X, Y, Z be set ; ::_thesis: for f1, f2 being Function of [:X,Y,Z:],D st ( for x, y, z being set st x in X & y in Y & z in Z holds f1 . [x,y,z] = f2 . [x,y,z] ) holds f1 = f2 let f1, f2 be Function of [:X,Y,Z:],D; ::_thesis: ( ( for x, y, z being set st x in X & y in Y & z in Z holds f1 . [x,y,z] = f2 . [x,y,z] ) implies f1 = f2 ) assume A1: for x, y, z being set st x in X & y in Y & z in Z holds f1 . [x,y,z] = f2 . [x,y,z] ; ::_thesis: f1 = f2 for t being set st t in [:X,Y,Z:] holds f1 . t = f2 . t proof let t be set ; ::_thesis: ( t in [:X,Y,Z:] implies f1 . t = f2 . t ) assume t in [:X,Y,Z:] ; ::_thesis: f1 . t = f2 . t then ex x, y, z being set st ( x in X & y in Y & z in Z & t = [x,y,z] ) by MCART_1:68; hence f1 . t = f2 . t by A1; ::_thesis: verum end; hence f1 = f2 by FUNCT_2:12; ::_thesis: verum end; theorem Th2: :: MULTOP_1:2 for A, B, C, D being non empty set for f1, f2 being Function of [:A,B,C:],D st ( for a being Element of A for b being Element of B for c being Element of C holds f1 . [a,b,c] = f2 . [a,b,c] ) holds f1 = f2 proof let A, B, C, D be non empty set ; ::_thesis: for f1, f2 being Function of [:A,B,C:],D st ( for a being Element of A for b being Element of B for c being Element of C holds f1 . [a,b,c] = f2 . [a,b,c] ) holds f1 = f2 let f1, f2 be Function of [:A,B,C:],D; ::_thesis: ( ( for a being Element of A for b being Element of B for c being Element of C holds f1 . [a,b,c] = f2 . [a,b,c] ) implies f1 = f2 ) assume for a being Element of A for b being Element of B for c being Element of C holds f1 . [a,b,c] = f2 . [a,b,c] ; ::_thesis: f1 = f2 then for x, y, z being set st x in A & y in B & z in C holds f1 . [x,y,z] = f2 . [x,y,z] ; hence f1 = f2 by Th1; ::_thesis: verum end; theorem :: MULTOP_1:3 for A, B, C, D being non empty set for f1, f2 being Function of [:A,B,C:],D st ( for a being Element of A for b being Element of B for c being Element of C holds f1 . (a,b,c) = f2 . (a,b,c) ) holds f1 = f2 proof let A, B, C, D be non empty set ; ::_thesis: for f1, f2 being Function of [:A,B,C:],D st ( for a being Element of A for b being Element of B for c being Element of C holds f1 . (a,b,c) = f2 . (a,b,c) ) holds f1 = f2 let f1, f2 be Function of [:A,B,C:],D; ::_thesis: ( ( for a being Element of A for b being Element of B for c being Element of C holds f1 . (a,b,c) = f2 . (a,b,c) ) implies f1 = f2 ) assume A1: for a being Element of A for b being Element of B for c being Element of C holds f1 . (a,b,c) = f2 . (a,b,c) ; ::_thesis: f1 = f2 for a being Element of A for b being Element of B for c being Element of C holds f1 . [a,b,c] = f2 . [a,b,c] proof let a be Element of A; ::_thesis: for b being Element of B for c being Element of C holds f1 . [a,b,c] = f2 . [a,b,c] let b be Element of B; ::_thesis: for c being Element of C holds f1 . [a,b,c] = f2 . [a,b,c] let c be Element of C; ::_thesis: f1 . [a,b,c] = f2 . [a,b,c] ( f1 . (a,b,c) = f1 . [a,b,c] & f2 . (a,b,c) = f2 . [a,b,c] ) ; hence f1 . [a,b,c] = f2 . [a,b,c] by A1; ::_thesis: verum end; hence f1 = f2 by Th2; ::_thesis: verum end; definition let A be set ; mode TriOp of A is Function of [:A,A,A:],A; end; scheme :: MULTOP_1:sch 1 FuncEx3D{ F1() -> non empty set , F2() -> non empty set , F3() -> non empty set , F4() -> non empty set , P1[ set , set , set , set ] } : ex f being Function of [:F1(),F2(),F3():],F4() st for x being Element of F1() for y being Element of F2() for z being Element of F3() holds P1[x,y,z,f . [x,y,z]] provided A1: for x being Element of F1() for y being Element of F2() for z being Element of F3() ex t being Element of F4() st P1[x,y,z,t] proof defpred S1[ set , set ] means for x being Element of F1() for y being Element of F2() for z being Element of F3() st \$1 = [x,y,z] holds P1[x,y,z,\$2]; A2: for p being Element of [:F1(),F2(),F3():] ex t being Element of F4() st S1[p,t] proof let p be Element of [:F1(),F2(),F3():]; ::_thesis: ex t being Element of F4() st S1[p,t] consider x1, y1, z1 being set such that A3: x1 in F1() and A4: y1 in F2() and A5: z1 in F3() and A6: p = [x1,y1,z1] by MCART_1:68; reconsider z1 = z1 as Element of F3() by A5; reconsider y1 = y1 as Element of F2() by A4; reconsider x1 = x1 as Element of F1() by A3; consider t being Element of F4() such that A7: P1[x1,y1,z1,t] by A1; take t ; ::_thesis: S1[p,t] let x be Element of F1(); ::_thesis: for y being Element of F2() for z being Element of F3() st p = [x,y,z] holds P1[x,y,z,t] let y be Element of F2(); ::_thesis: for z being Element of F3() st p = [x,y,z] holds P1[x,y,z,t] let z be Element of F3(); ::_thesis: ( p = [x,y,z] implies P1[x,y,z,t] ) assume A8: p = [x,y,z] ; ::_thesis: P1[x,y,z,t] then ( x1 = x & y1 = y ) by A6, XTUPLE_0:3; hence P1[x,y,z,t] by A6, A7, A8, XTUPLE_0:3; ::_thesis: verum end; consider f being Function of [:F1(),F2(),F3():],F4() such that A9: for p being Element of [:F1(),F2(),F3():] holds S1[p,f . p] from FUNCT_2:sch_3(A2); take f ; ::_thesis: for x being Element of F1() for y being Element of F2() for z being Element of F3() holds P1[x,y,z,f . [x,y,z]] let x be Element of F1(); ::_thesis: for y being Element of F2() for z being Element of F3() holds P1[x,y,z,f . [x,y,z]] let y be Element of F2(); ::_thesis: for z being Element of F3() holds P1[x,y,z,f . [x,y,z]] let z be Element of F3(); ::_thesis: P1[x,y,z,f . [x,y,z]] thus P1[x,y,z,f . [x,y,z]] by A9; ::_thesis: verum end; scheme :: MULTOP_1:sch 2 TriOpEx{ F1() -> non empty set , P1[ Element of F1(), Element of F1(), Element of F1(), Element of F1()] } : ex o being TriOp of F1() st for a, b, c being Element of F1() holds P1[a,b,c,o . (a,b,c)] provided A1: for x, y, z being Element of F1() ex t being Element of F1() st P1[x,y,z,t] proof defpred S1[ Element of F1(), Element of F1(), Element of F1(), Element of F1()] means for r being Element of F1() st r = \$4 holds P1[\$1,\$2,\$3,r]; A2: for x, y, z being Element of F1() ex t being Element of F1() st S1[x,y,z,t] proof let x, y, z be Element of F1(); ::_thesis: ex t being Element of F1() st S1[x,y,z,t] consider t being Element of F1() such that A3: P1[x,y,z,t] by A1; take t ; ::_thesis: S1[x,y,z,t] thus S1[x,y,z,t] by A3; ::_thesis: verum end; consider f being Function of [:F1(),F1(),F1():],F1() such that A4: for a, b, c being Element of F1() holds S1[a,b,c,f . [a,b,c]] from MULTOP_1:sch_1(A2); take f ; ::_thesis: for a, b, c being Element of F1() holds P1[a,b,c,f . (a,b,c)] let a, b, c be Element of F1(); ::_thesis: P1[a,b,c,f . (a,b,c)] thus P1[a,b,c,f . (a,b,c)] by A4; ::_thesis: verum end; scheme :: MULTOP_1:sch 3 Lambda3D{ F1() -> non empty set , F2() -> non empty set , F3() -> non empty set , F4() -> non empty set , F5( Element of F1(), Element of F2(), Element of F3()) -> Element of F4() } : ex f being Function of [:F1(),F2(),F3():],F4() st for x being Element of F1() for y being Element of F2() for z being Element of F3() holds f . [x,y,z] = F5(x,y,z) proof defpred S1[ Element of F1(), Element of F2(), Element of F3(), Element of F4()] means \$4 = F5(\$1,\$2,\$3); A1: for x being Element of F1() for y being Element of F2() for z being Element of F3() ex t being Element of F4() st S1[x,y,z,t] ; ex f being Function of [:F1(),F2(),F3():],F4() st for x being Element of F1() for y being Element of F2() for z being Element of F3() holds S1[x,y,z,f . [x,y,z]] from MULTOP_1:sch_1(A1); hence ex f being Function of [:F1(),F2(),F3():],F4() st for x being Element of F1() for y being Element of F2() for z being Element of F3() holds f . [x,y,z] = F5(x,y,z) ; ::_thesis: verum end; scheme :: MULTOP_1:sch 4 TriOpLambda{ F1() -> non empty set , F2() -> non empty set , F3() -> non empty set , F4() -> non empty set , F5( Element of F1(), Element of F2(), Element of F3()) -> Element of F4() } : ex o being Function of [:F1(),F2(),F3():],F4() st for a being Element of F1() for b being Element of F2() for c being Element of F3() holds o . (a,b,c) = F5(a,b,c) proof consider f being Function of [:F1(),F2(),F3():],F4() such that A1: for a being Element of F1() for b being Element of F2() for c being Element of F3() holds f . [a,b,c] = F5(a,b,c) from MULTOP_1:sch_3(); take f ; ::_thesis: for a being Element of F1() for b being Element of F2() for c being Element of F3() holds f . (a,b,c) = F5(a,b,c) let a be Element of F1(); ::_thesis: for b being Element of F2() for c being Element of F3() holds f . (a,b,c) = F5(a,b,c) let b be Element of F2(); ::_thesis: for c being Element of F3() holds f . (a,b,c) = F5(a,b,c) let c be Element of F3(); ::_thesis: f . (a,b,c) = F5(a,b,c) thus f . (a,b,c) = F5(a,b,c) by A1; ::_thesis: verum end; definition let f be Function; let a, b, c, d be set ; funcf . (a,b,c,d) -> set equals :: MULTOP_1:def 2 f . [a,b,c,d]; correctness coherence f . [a,b,c,d] is set ; ; end; :: deftheorem defines . MULTOP_1:def_2_:_ for f being Function for a, b, c, d being set holds f . (a,b,c,d) = f . [a,b,c,d]; definition let A, B, C, D, E be non empty set ; let f be Function of [:A,B,C,D:],E; let a be Element of A; let b be Element of B; let c be Element of C; let d be Element of D; :: original: . redefine funcf . (a,b,c,d) -> Element of E; coherence f . (a,b,c,d) is Element of E proof f . [a,b,c,d] is Element of E ; hence f . (a,b,c,d) is Element of E ; ::_thesis: verum end; end; theorem Th4: :: MULTOP_1:4 for D being non empty set for X, Y, Z, S being set for f1, f2 being Function of [:X,Y,Z,S:],D st ( for x, y, z, s being set 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 D be non empty set ; ::_thesis: for X, Y, Z, S being set for f1, f2 being Function of [:X,Y,Z,S:],D st ( for x, y, z, s being set 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 let X, Y, Z, S be set ; ::_thesis: for f1, f2 being Function of [:X,Y,Z,S:],D st ( for x, y, z, s being set 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 let f1, f2 be Function of [:X,Y,Z,S:],D; ::_thesis: ( ( for x, y, z, s being set st x in X & y in Y & z in Z & s in S holds f1 . [x,y,z,s] = f2 . [x,y,z,s] ) implies f1 = f2 ) assume A1: for x, y, z, s being set st x in X & y in Y & z in Z & s in S holds f1 . [x,y,z,s] = f2 . [x,y,z,s] ; ::_thesis: f1 = f2 for t being set st t in [:X,Y,Z,S:] holds f1 . t = f2 . t proof let t be set ; ::_thesis: ( t in [:X,Y,Z,S:] implies f1 . t = f2 . t ) assume t in [:X,Y,Z,S:] ; ::_thesis: f1 . t = f2 . t then ex x, y, z, s being set st ( x in X & y in Y & z in Z & s in S & t = [x,y,z,s] ) by MCART_1:79; hence f1 . t = f2 . t by A1; ::_thesis: verum end; hence f1 = f2 by FUNCT_2:12; ::_thesis: verum end; theorem Th5: :: MULTOP_1:5 for A, B, C, D, E being non empty set for f1, f2 being Function of [:A,B,C,D:],E st ( for a being Element of A for b being Element of B for c being Element of C for d being Element of D holds f1 . [a,b,c,d] = f2 . [a,b,c,d] ) holds f1 = f2 proof let A, B, C, D, E be non empty set ; ::_thesis: for f1, f2 being Function of [:A,B,C,D:],E st ( for a being Element of A for b being Element of B for c being Element of C for d being Element of D holds f1 . [a,b,c,d] = f2 . [a,b,c,d] ) holds f1 = f2 let f1, f2 be Function of [:A,B,C,D:],E; ::_thesis: ( ( for a being Element of A for b being Element of B for c being Element of C for d being Element of D holds f1 . [a,b,c,d] = f2 . [a,b,c,d] ) implies f1 = f2 ) assume for a being Element of A for b being Element of B for c being Element of C for d being Element of D holds f1 . [a,b,c,d] = f2 . [a,b,c,d] ; ::_thesis: f1 = f2 then for x, y, z, s being set 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 f1 = f2 by Th4; ::_thesis: verum end; theorem :: MULTOP_1:6 for A, B, C, D, E being non empty set for f1, f2 being Function of [:A,B,C,D:],E st ( for a being Element of A for b being Element of B for c being Element of C for d being Element of D holds f1 . (a,b,c,d) = f2 . (a,b,c,d) ) holds f1 = f2 proof let A, B, C, D, E be non empty set ; ::_thesis: for f1, f2 being Function of [:A,B,C,D:],E st ( for a being Element of A for b being Element of B for c being Element of C for d being Element of D holds f1 . (a,b,c,d) = f2 . (a,b,c,d) ) holds f1 = f2 let f1, f2 be Function of [:A,B,C,D:],E; ::_thesis: ( ( for a being Element of A for b being Element of B for c being Element of C for d being Element of D holds f1 . (a,b,c,d) = f2 . (a,b,c,d) ) implies f1 = f2 ) assume A1: for a being Element of A for b being Element of B for c being Element of C for d being Element of D holds f1 . (a,b,c,d) = f2 . (a,b,c,d) ; ::_thesis: f1 = f2 for a being Element of A for b being Element of B for c being Element of C for d being Element of D holds f1 . [a,b,c,d] = f2 . [a,b,c,d] proof let a be Element of A; ::_thesis: for b being Element of B for c being Element of C for d being Element of D holds f1 . [a,b,c,d] = f2 . [a,b,c,d] let b be Element of B; ::_thesis: for c being Element of C for d being Element of D holds f1 . [a,b,c,d] = f2 . [a,b,c,d] let c be Element of C; ::_thesis: for d being Element of D holds f1 . [a,b,c,d] = f2 . [a,b,c,d] let d be Element of D; ::_thesis: f1 . [a,b,c,d] = f2 . [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 f1 . [a,b,c,d] = f2 . [a,b,c,d] by A1; ::_thesis: verum end; hence f1 = f2 by Th5; ::_thesis: verum end; definition let A be non empty set ; mode QuaOp of A is Function of [:A,A,A,A:],A; end; scheme :: MULTOP_1:sch 5 FuncEx4D{ F1() -> non empty set , F2() -> non empty set , F3() -> non empty set , F4() -> non empty set , F5() -> non empty set , P1[ set , set , set , set , set ] } : ex f being Function of [:F1(),F2(),F3(),F4():],F5() st for x being Element of F1() for y being Element of F2() for z being Element of F3() for s being Element of F4() holds P1[x,y,z,s,f . [x,y,z,s]] provided A1: for x being Element of F1() for y being Element of F2() for z being Element of F3() for s being Element of F4() ex t being Element of F5() st P1[x,y,z,s,t] proof defpred S1[ set , set ] means for x being Element of F1() for y being Element of F2() for z being Element of F3() for s being Element of F4() st \$1 = [x,y,z,s] holds P1[x,y,z,s,\$2]; A2: for p being Element of [:F1(),F2(),F3(),F4():] ex t being Element of F5() st S1[p,t] proof let p be Element of [:F1(),F2(),F3(),F4():]; ::_thesis: ex t being Element of F5() st S1[p,t] consider x1, y1, z1, s1 being set such that A3: x1 in F1() and A4: y1 in F2() and A5: z1 in F3() and A6: s1 in F4() and A7: p = [x1,y1,z1,s1] by MCART_1:79; reconsider s1 = s1 as Element of F4() by A6; reconsider z1 = z1 as Element of F3() by A5; reconsider y1 = y1 as Element of F2() by A4; reconsider x1 = x1 as Element of F1() by A3; consider t being Element of F5() such that A8: P1[x1,y1,z1,s1,t] by A1; take t ; ::_thesis: S1[p,t] let x be Element of F1(); ::_thesis: for y being Element of F2() for z being Element of F3() for s being Element of F4() st p = [x,y,z,s] holds P1[x,y,z,s,t] let y be Element of F2(); ::_thesis: for z being Element of F3() for s being Element of F4() st p = [x,y,z,s] holds P1[x,y,z,s,t] let z be Element of F3(); ::_thesis: for s being Element of F4() st p = [x,y,z,s] holds P1[x,y,z,s,t] let s be Element of F4(); ::_thesis: ( p = [x,y,z,s] implies P1[x,y,z,s,t] ) assume A9: p = [x,y,z,s] ; ::_thesis: P1[x,y,z,s,t] then A10: z1 = z by A7, XTUPLE_0:5; ( x1 = x & y1 = y ) by A7, A9, XTUPLE_0:5; hence P1[x,y,z,s,t] by A7, A8, A9, A10, XTUPLE_0:5; ::_thesis: verum end; consider f being Function of [:F1(),F2(),F3(),F4():],F5() such that A11: for p being Element of [:F1(),F2(),F3(),F4():] holds S1[p,f . p] from FUNCT_2:sch_3(A2); take f ; ::_thesis: for x being Element of F1() for y being Element of F2() for z being Element of F3() for s being Element of F4() holds P1[x,y,z,s,f . [x,y,z,s]] let x be Element of F1(); ::_thesis: for y being Element of F2() for z being Element of F3() for s being Element of F4() holds P1[x,y,z,s,f . [x,y,z,s]] let y be Element of F2(); ::_thesis: for z being Element of F3() for s being Element of F4() holds P1[x,y,z,s,f . [x,y,z,s]] let z be Element of F3(); ::_thesis: for s being Element of F4() holds P1[x,y,z,s,f . [x,y,z,s]] let s be Element of F4(); ::_thesis: P1[x,y,z,s,f . [x,y,z,s]] thus P1[x,y,z,s,f . [x,y,z,s]] by A11; ::_thesis: verum end; scheme :: MULTOP_1:sch 6 QuaOpEx{ F1() -> non empty set , P1[ Element of F1(), Element of F1(), Element of F1(), Element of F1(), Element of F1()] } : ex o being QuaOp of F1() st for a, b, c, d being Element of F1() holds P1[a,b,c,d,o . (a,b,c,d)] provided A1: for x, y, z, s being Element of F1() ex t being Element of F1() st P1[x,y,z,s,t] proof defpred S1[ Element of F1(), Element of F1(), Element of F1(), Element of F1(), Element of F1()] means for r being Element of F1() st r = \$5 holds P1[\$1,\$2,\$3,\$4,\$5]; A2: for x, y, z, s being Element of F1() ex t being Element of F1() st S1[x,y,z,s,t] proof let x, y, z, s be Element of F1(); ::_thesis: ex t being Element of F1() st S1[x,y,z,s,t] consider t being Element of F1() such that A3: P1[x,y,z,s,t] by A1; take t ; ::_thesis: S1[x,y,z,s,t] thus S1[x,y,z,s,t] by A3; ::_thesis: verum end; consider f being Function of [:F1(),F1(),F1(),F1():],F1() such that A4: for a, b, c, d being Element of F1() holds S1[a,b,c,d,f . [a,b,c,d]] from MULTOP_1:sch_5(A2); take f ; ::_thesis: for a, b, c, d being Element of F1() holds P1[a,b,c,d,f . (a,b,c,d)] let a, b, c, d be Element of F1(); ::_thesis: P1[a,b,c,d,f . (a,b,c,d)] thus P1[a,b,c,d,f . (a,b,c,d)] by A4; ::_thesis: verum end; scheme :: MULTOP_1:sch 7 Lambda4D{ F1() -> non empty set , F2() -> non empty set , F3() -> non empty set , F4() -> non empty set , F5() -> non empty set , F6( Element of F1(), Element of F2(), Element of F3(), Element of F4()) -> Element of F5() } : ex f being Function of [:F1(),F2(),F3(),F4():],F5() st for x being Element of F1() for y being Element of F2() for z being Element of F3() for s being Element of F4() holds f . [x,y,z,s] = F6(x,y,z,s) proof defpred S1[ Element of F1(), Element of F2(), Element of F3(), Element of F4(), Element of F5()] means \$5 = F6(\$1,\$2,\$3,\$4); A1: for x being Element of F1() for y being Element of F2() for z being Element of F3() for s being Element of F4() ex t being Element of F5() st S1[x,y,z,s,t] ; ex f being Function of [:F1(),F2(),F3(),F4():],F5() st for x being Element of F1() for y being Element of F2() for z being Element of F3() for s being Element of F4() holds S1[x,y,z,s,f . [x,y,z,s]] from MULTOP_1:sch_5(A1); hence ex f being Function of [:F1(),F2(),F3(),F4():],F5() st for x being Element of F1() for y being Element of F2() for z being Element of F3() for s being Element of F4() holds f . [x,y,z,s] = F6(x,y,z,s) ; ::_thesis: verum end; scheme :: MULTOP_1:sch 8 QuaOpLambda{ F1() -> non empty set , F2( Element of F1(), Element of F1(), Element of F1(), Element of F1()) -> Element of F1() } : ex o being QuaOp of F1() st for a, b, c, d being Element of F1() holds o . (a,b,c,d) = F2(a,b,c,d) proof deffunc H1( Element of F1(), Element of F1(), Element of F1(), Element of F1()) -> Element of F1() = F2(\$1,\$2,\$3,\$4); consider f being Function of [:F1(),F1(),F1(),F1():],F1() such that A1: for a, b, c, d being Element of F1() holds f . [a,b,c,d] = H1(a,b,c,d) from MULTOP_1:sch_7(); take f ; ::_thesis: for a, b, c, d being Element of F1() holds f . (a,b,c,d) = F2(a,b,c,d) let a, b, c, d be Element of F1(); ::_thesis: f . (a,b,c,d) = F2(a,b,c,d) thus f . (a,b,c,d) = F2(a,b,c,d) by A1; ::_thesis: verum end;