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

end;

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