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

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