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


definition
let f be Function;
let a, b, c be object ;
func f . (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 object 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 func f . (a,b,c) -> Element of D;
coherence
f . (a,b,c) is Element of D
proof 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 object st x in X & y in Y & z in Z holds
f1 . [x,y,z] = f2 . [x,y,z] ) holds
f1 = f2
proof 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 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 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[ object , object , object , object ] } :
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 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 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 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 end;

:: FOUR ARGUMENT OPERATIONS
definition
let f be Function;
let a, b, c, d be set ;
func f . (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 func f . (a,b,c,d) -> Element of E;
coherence
f . (a,b,c,d) is Element of E
proof 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 object 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 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 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 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[ object , object , object , object , object ] } :
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 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 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 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 end;