:: MULTOP_1 semantic presentation

definition
let c1 be Function;
let c2, c3, c4 be set ;
func c1 . c2,c3,c4 -> set equals :: MULTOP_1:def 1
a1 . [a2,a3,a4];
correctness
coherence
c1 . [c2,c3,c4] is set ;
;
end;

:: deftheorem Def1 defines . MULTOP_1:def 1 :
for b1 being Function
for b2, b3, b4 being set holds b1 . b2,b3,b4 = b1 . [b2,b3,b4];

definition
let c1, c2, c3, c4 be non empty set ;
let c5 be Function of [:c1,c2,c3:],c4;
let c6 be Element of c1;
let c7 be Element of c2;
let c8 be Element of c3;
redefine func . as c5 . c6,c7,c8 -> Element of a4;
coherence
c5 . c6,c7,c8 is Element of c4
proof end;
end;

theorem Th1: :: MULTOP_1:1
canceled;

theorem Th2: :: MULTOP_1:2
for b1 being non empty set
for b2, b3, b4 being set
for b5, b6 being Function of [:b2,b3,b4:],b1 st ( for b7, b8, b9 being set st b7 in b2 & b8 in b3 & b9 in b4 holds
b5 . [b7,b8,b9] = b6 . [b7,b8,b9] ) holds
b5 = b6
proof end;

theorem Th3: :: MULTOP_1:3
for b1, b2, b3, b4 being non empty set
for b5, b6 being Function of [:b1,b2,b3:],b4 st ( for b7 being Element of b1
for b8 being Element of b2
for b9 being Element of b3 holds b5 . [b7,b8,b9] = b6 . [b7,b8,b9] ) holds
b5 = b6
proof end;

theorem Th4: :: MULTOP_1:4
for b1, b2, b3, b4 being non empty set
for b5, b6 being Function of [:b1,b2,b3:],b4 st ( for b7 being Element of b1
for b8 being Element of b2
for b9 being Element of b3 holds b5 . b7,b8,b9 = b6 . b7,b8,b9 ) holds
b5 = b6
proof end;

definition
let c1 be set ;
mode TriOp of a1 is Function of [:a1,a1,a1:],a1;
end;

scheme :: MULTOP_1:sch 1
s1{ F1() -> non empty set , F2() -> non empty set , F3() -> non empty set , F4() -> non empty set , P1[ set , set , set , set ] } :
ex b1 being Function of [:F1(),F2(),F3():],F4() st
for b2 being Element of F1()
for b3 being Element of F2()
for b4 being Element of F3() holds P1[b2,b3,b4,b1 . [b2,b3,b4]]
provided
E3: for b1 being Element of F1()
for b2 being Element of F2()
for b3 being Element of F3() ex b4 being Element of F4() st P1[b1,b2,b3,b4]
proof end;

scheme :: MULTOP_1:sch 2
s2{ F1() -> non empty set , P1[ Element of F1(), Element of F1(), Element of F1(), Element of F1()] } :
ex b1 being TriOp of F1() st
for b2, b3, b4 being Element of F1() holds P1[b2,b3,b4,b1 . b2,b3,b4]
provided
E3: for b1, b2, b3 being Element of F1() ex b4 being Element of F1() st P1[b1,b2,b3,b4]
proof end;

scheme :: MULTOP_1:sch 3
s3{ 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 b1 being Function of [:F1(),F2(),F3():],F4() st
for b2 being Element of F1()
for b3 being Element of F2()
for b4 being Element of F3() holds b1 . [b2,b3,b4] = F5(b2,b3,b4)
proof end;

scheme :: MULTOP_1:sch 4
s4{ 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 b1 being Function of [:F1(),F2(),F3():],F4() st
for b2 being Element of F1()
for b3 being Element of F2()
for b4 being Element of F3() holds b1 . b2,b3,b4 = F5(b2,b3,b4)
proof end;

definition
let c1 be Function;
let c2, c3, c4, c5 be set ;
func c1 . c2,c3,c4,c5 -> set equals :: MULTOP_1:def 2
a1 . [a2,a3,a4,a5];
correctness
coherence
c1 . [c2,c3,c4,c5] is set ;
;
end;

:: deftheorem Def2 defines . MULTOP_1:def 2 :
for b1 being Function
for b2, b3, b4, b5 being set holds b1 . b2,b3,b4,b5 = b1 . [b2,b3,b4,b5];

definition
let c1, c2, c3, c4, c5 be non empty set ;
let c6 be Function of [:c1,c2,c3,c4:],c5;
let c7 be Element of c1;
let c8 be Element of c2;
let c9 be Element of c3;
let c10 be Element of c4;
redefine func . as c6 . c7,c8,c9,c10 -> Element of a5;
coherence
c6 . c7,c8,c9,c10 is Element of c5
proof end;
end;

theorem Th5: :: MULTOP_1:5
canceled;

theorem Th6: :: MULTOP_1:6
for b1 being non empty set
for b2, b3, b4, b5 being set
for b6, b7 being Function of [:b2,b3,b4,b5:],b1 st ( for b8, b9, b10, b11 being set st b8 in b2 & b9 in b3 & b10 in b4 & b11 in b5 holds
b6 . [b8,b9,b10,b11] = b7 . [b8,b9,b10,b11] ) holds
b6 = b7
proof end;

theorem Th7: :: MULTOP_1:7
for b1, b2, b3, b4, b5 being non empty set
for b6, b7 being Function of [:b1,b2,b3,b4:],b5 st ( for b8 being Element of b1
for b9 being Element of b2
for b10 being Element of b3
for b11 being Element of b4 holds b6 . [b8,b9,b10,b11] = b7 . [b8,b9,b10,b11] ) holds
b6 = b7
proof end;

theorem Th8: :: MULTOP_1:8
for b1, b2, b3, b4, b5 being non empty set
for b6, b7 being Function of [:b1,b2,b3,b4:],b5 st ( for b8 being Element of b1
for b9 being Element of b2
for b10 being Element of b3
for b11 being Element of b4 holds b6 . b8,b9,b10,b11 = b7 . b8,b9,b10,b11 ) holds
b6 = b7
proof end;

definition
let c1 be non empty set ;
mode QuaOp of a1 is Function of [:a1,a1,a1,a1:],a1;
end;

scheme :: MULTOP_1:sch 5
s5{ 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 b1 being Function of [:F1(),F2(),F3(),F4():],F5() st
for b2 being Element of F1()
for b3 being Element of F2()
for b4 being Element of F3()
for b5 being Element of F4() holds P1[b2,b3,b4,b5,b1 . [b2,b3,b4,b5]]
provided
E5: for b1 being Element of F1()
for b2 being Element of F2()
for b3 being Element of F3()
for b4 being Element of F4() ex b5 being Element of F5() st P1[b1,b2,b3,b4,b5]
proof end;

scheme :: MULTOP_1:sch 6
s6{ F1() -> non empty set , P1[ Element of F1(), Element of F1(), Element of F1(), Element of F1(), Element of F1()] } :
ex b1 being QuaOp of F1() st
for b2, b3, b4, b5 being Element of F1() holds P1[b2,b3,b4,b5,b1 . b2,b3,b4,b5]
provided
E5: for b1, b2, b3, b4 being Element of F1() ex b5 being Element of F1() st P1[b1,b2,b3,b4,b5]
proof end;

scheme :: MULTOP_1:sch 7
s7{ 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 b1 being Function of [:F1(),F2(),F3(),F4():],F5() st
for b2 being Element of F1()
for b3 being Element of F2()
for b4 being Element of F3()
for b5 being Element of F4() holds b1 . [b2,b3,b4,b5] = F6(b2,b3,b4,b5)
proof end;

scheme :: MULTOP_1:sch 8
s8{ F1() -> non empty set , F2( Element of F1(), Element of F1(), Element of F1(), Element of F1()) -> Element of F1() } :
ex b1 being QuaOp of F1() st
for b2, b3, b4, b5 being Element of F1() holds b1 . b2,b3,b4,b5 = F2(b2,b3,b4,b5)
proof end;