let A, B, C, D, E be non empty set ; :: thesis: 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; :: thesis: ( ( 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 ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: for d being Element of D holds f1 . [a,b,c,d] = f2 . [a,b,c,d]
let d be Element of D; :: thesis: 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; :: thesis: verum

end;

hence f1 = f2 by Th7; :: thesis: verum