begin
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;
.redefine func f . (
a,
b,
c)
-> Element of
D;
coherence
f . (a,b,c) is Element of D
end;
theorem Th1:
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
theorem Th2:
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
theorem
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
scheme
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]
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;
.redefine func f . (
a,
b,
c,
d)
-> Element of
E;
coherence
f . (a,b,c,d) is Element of E
end;
theorem Th4:
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
theorem Th5:
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
theorem
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
scheme
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
scheme
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]
scheme
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)
scheme
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)