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

begin

definition

let f be Function;
let a, b, c be set ;
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 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 func f . (a,b,c) -> Element of D;
coherence
f . (a,b,c) is Element of D

proof end;

end;

theorem :: MULTOP_1:1

canceled;

theorem Th2: :: MULTOP_1:2

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

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

theorem :: MULTOP_1:4

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{ F₁() -> non empty set , F₂() -> non empty set , F₃() -> non empty set , F₄() -> non empty set , P₁[ set , set , set , set ] } :

ex f being Function of [:F₁(),F₂(),F₃():],F₄() st
for x being Element of F₁()
for y being Element of F₂()
for z being Element of F₃() holds P₁[x,y,z,f . [x,y,z]]

provided

A1: for x being Element of F₁()
for y being Element of F₂()
for z being Element of F₃() ex t being Element of F₄() st P₁[x,y,z,t]

proof end;

scheme :: MULTOP_1:sch 2
TriOpEx{ F₁() -> non empty set , P₁[ Element of F₁(), Element of F₁(), Element of F₁(), Element of F₁()] } :

ex o being TriOp of F₁() st
for a, b, c being Element of F₁() holds P₁[a,b,c,o . (a,b,c)]

provided

A1: for x, y, z being Element of F₁() ex t being Element of F₁() st P₁[x,y,z,t]

proof end;

scheme :: MULTOP_1:sch 3
Lambda3D{ F₁() -> non empty set , F₂() -> non empty set , F₃() -> non empty set , F₄() -> non empty set , F₅( Element of F₁(), Element of F₂(), Element of F₃()) -> Element of F₄() } :

ex f being Function of [:F₁(),F₂(),F₃():],F₄() st
for x being Element of F₁()
for y being Element of F₂()
for z being Element of F₃() holds f . [x,y,z] = F₅(x,y,z)

proof end;

scheme :: MULTOP_1:sch 4
TriOpLambda{ F₁() -> non empty set , F₂() -> non empty set , F₃() -> non empty set , F₄() -> non empty set , F₅( Element of F₁(), Element of F₂(), Element of F₃()) -> Element of F₄() } :

ex o being Function of [:F₁(),F₂(),F₃():],F₄() st
for a being Element of F₁()
for b being Element of F₂()
for c being Element of F₃() holds o . (a,b,c) = F₅(a,b,c)

proof end;

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 :: MULTOP_1:5

canceled;

theorem Th6: :: MULTOP_1:6

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

theorem Th7: :: MULTOP_1:7

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

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{ F₁() -> non empty set , F₂() -> non empty set , F₃() -> non empty set , F₄() -> non empty set , F₅() -> non empty set , P₁[ set , set , set , set , set ] } :

ex f being Function of [:F₁(),F₂(),F₃(),F₄():],F₅() st
for x being Element of F₁()
for y being Element of F₂()
for z being Element of F₃()
for s being Element of F₄() holds P₁[x,y,z,s,f . [x,y,z,s]]

provided

A1: for x being Element of F₁()
for y being Element of F₂()
for z being Element of F₃()
for s being Element of F₄() ex t being Element of F₅() st P₁[x,y,z,s,t]

proof end;

scheme :: MULTOP_1:sch 6
QuaOpEx{ F₁() -> non empty set , P₁[ Element of F₁(), Element of F₁(), Element of F₁(), Element of F₁(), Element of F₁()] } :

ex o being QuaOp of F₁() st
for a, b, c, d being Element of F₁() holds P₁[a,b,c,d,o . (a,b,c,d)]

provided

A1: for x, y, z, s being Element of F₁() ex t being Element of F₁() st P₁[x,y,z,s,t]

proof end;

scheme :: MULTOP_1:sch 7
Lambda4D{ F₁() -> non empty set , F₂() -> non empty set , F₃() -> non empty set , F₄() -> non empty set , F₅() -> non empty set , F₆( Element of F₁(), Element of F₂(), Element of F₃(), Element of F₄()) -> Element of F₅() } :

ex f being Function of [:F₁(),F₂(),F₃(),F₄():],F₅() st
for x being Element of F₁()
for y being Element of F₂()
for z being Element of F₃()
for s being Element of F₄() holds f . [x,y,z,s] = F₆(x,y,z,s)

proof end;

scheme :: MULTOP_1:sch 8
QuaOpLambda{ F₁() -> non empty set , F₂( Element of F₁(), Element of F₁(), Element of F₁(), Element of F₁()) -> Element of F₁() } :

ex o being QuaOp of F₁() st
for a, b, c, d being Element of F₁() holds o . (a,b,c,d) = F₂(a,b,c,d)

proof end;