let A, B, C, D be 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
let f1, f2 be Function of [:A,B,C:],D; ( ( 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) ) implies f1 = f2 )
assume A1:
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)
; f1 = f2
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]
proof
let a be
Element of
A;
for b being Element of B
for c being Element of C holds f1 . [a,b,c] = f2 . [a,b,c]let b be
Element of
B;
for c being Element of C holds f1 . [a,b,c] = f2 . [a,b,c]let c be
Element of
C;
f1 . [a,b,c] = f2 . [a,b,c]
(
f1 . (
a,
b,
c)
= f1 . [a,b,c] &
f2 . (
a,
b,
c)
= f2 . [a,b,c] )
;
hence
f1 . [a,b,c] = f2 . [a,b,c]
by A1;
verum
end;
hence
f1 = f2
by Th2; verum