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