:: 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;