:: by Michal Muzalewski and Wojciech Skaba

::

:: Received October 2, 1990

:: Copyright (c) 1990-2012 Association of Mizar Users

begin

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

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

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

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

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

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

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;

scheme :: MULTOP_1:sch 1

FuncEx3D{ F_{1}() -> non empty set , F_{2}() -> non empty set , F_{3}() -> non empty set , F_{4}() -> non empty set , P_{1}[ set , set , set , set ] } :

FuncEx3D{ F

ex f being Function of [:F_{1}(),F_{2}(),F_{3}():],F_{4}() st

for x being Element of F_{1}()

for y being Element of F_{2}()

for z being Element of F_{3}() holds P_{1}[x,y,z,f . [x,y,z]]

providedfor x being Element of F

for y being Element of F

for z being Element of F

A1:
for x being Element of F_{1}()

for y being Element of F_{2}()

for z being Element of F_{3}() ex t being Element of F_{4}() st P_{1}[x,y,z,t]

for y being Element of F

for z being Element of F

proof end;

scheme :: MULTOP_1:sch 3

Lambda3D{ F_{1}() -> non empty set , F_{2}() -> non empty set , F_{3}() -> non empty set , F_{4}() -> non empty set , F_{5}( Element of F_{1}(), Element of F_{2}(), Element of F_{3}()) -> Element of F_{4}() } :

Lambda3D{ F

ex f being Function of [:F_{1}(),F_{2}(),F_{3}():],F_{4}() st

for x being Element of F_{1}()

for y being Element of F_{2}()

for z being Element of F_{3}() holds f . [x,y,z] = F_{5}(x,y,z)

for x being Element of F

for y being Element of F

for z being Element of F

proof end;

scheme :: MULTOP_1:sch 4

TriOpLambda{ F_{1}() -> non empty set , F_{2}() -> non empty set , F_{3}() -> non empty set , F_{4}() -> non empty set , F_{5}( Element of F_{1}(), Element of F_{2}(), Element of F_{3}()) -> Element of F_{4}() } :

TriOpLambda{ F

ex o being Function of [:F_{1}(),F_{2}(),F_{3}():],F_{4}() st

for a being Element of F_{1}()

for b being Element of F_{2}()

for c being Element of F_{3}() holds o . (a,b,c) = F_{5}(a,b,c)

for a being Element of F

for b being Element of F

for c being Element of F

proof end;

:: FOUR ARGUMENT OPERATIONS

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

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

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

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

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

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

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;

scheme :: MULTOP_1:sch 5

FuncEx4D{ F_{1}() -> non empty set , F_{2}() -> non empty set , F_{3}() -> non empty set , F_{4}() -> non empty set , F_{5}() -> non empty set , P_{1}[ set , set , set , set , set ] } :

FuncEx4D{ F

ex f being Function of [:F_{1}(),F_{2}(),F_{3}(),F_{4}():],F_{5}() st

for x being Element of F_{1}()

for y being Element of F_{2}()

for z being Element of F_{3}()

for s being Element of F_{4}() holds P_{1}[x,y,z,s,f . [x,y,z,s]]

providedfor x being Element of F

for y being Element of F

for z being Element of F

for s being Element of F

A1:
for x being Element of F_{1}()

for y being Element of F_{2}()

for z being Element of F_{3}()

for s being Element of F_{4}() ex t being Element of F_{5}() st P_{1}[x,y,z,s,t]

for y being Element of F

for z being Element of F

for s being Element of F

proof end;

scheme :: MULTOP_1:sch 7

Lambda4D{ F_{1}() -> non empty set , F_{2}() -> non empty set , F_{3}() -> non empty set , F_{4}() -> non empty set , F_{5}() -> non empty set , F_{6}( Element of F_{1}(), Element of F_{2}(), Element of F_{3}(), Element of F_{4}()) -> Element of F_{5}() } :

Lambda4D{ F

ex f being Function of [:F_{1}(),F_{2}(),F_{3}(),F_{4}():],F_{5}() st

for x being Element of F_{1}()

for y being Element of F_{2}()

for z being Element of F_{3}()

for s being Element of F_{4}() holds f . [x,y,z,s] = F_{6}(x,y,z,s)

for x being Element of F

for y being Element of F

for z being Element of F

for s being Element of F

proof end;