:: MULTOP_1 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th2: :: MULTOP_1:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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[ 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 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;

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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th6: :: MULTOP_1:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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[ 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 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;