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 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
then for x, y, z being object st x in A & y in B & z in C holds
f1 . [x,y,z] = f2 . [x,y,z] ;
hence f1 = f2 by Th1; :: thesis: verum