:: Three-Argument Operations and Four-Argument Operations
:: by Michal Muzalewski and Wojciech Skaba
::
:: Received October 2, 1990
:: Copyright (c) 1990-2012 Association of Mizar Users


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

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

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

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]
proofend;

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]
proofend;

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)
proofend;

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)
proofend;

:: FOUR ARGUMENT OPERATIONS
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
proofend;
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
proofend;

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

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

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]
proofend;

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]
proofend;

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)
proofend;

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)
proofend;