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