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