let X, Y, Z be set ; :: thesis: for f1, f2 being Function of [:X,Y:],Z st ( for a being Element of X
for b being Element of Y holds f1 . (a,b) = f2 . (a,b) ) holds
f1 = f2
let f1, f2 be Function of [:X,Y:],Z; :: thesis: ( ( for a being Element of X
for b being Element of Y holds f1 . (a,b) = f2 . (a,b) ) implies f1 = f2 )
assume for a being Element of X
for b being Element of Y holds f1 . (a,b) = f2 . (a,b) ; :: thesis: f1 = f2
then for x, y being set st x in X & y in Y holds
f1 . (x,y) = f2 . (x,y) ;
hence f1 = f2 by Th1; :: thesis: verum