let X, Y, Z be set ; :: thesis: for f1, f2 being Function of [:X,Y:],Z st ( for x, y being set st x in X & y in Y holds
f1 . (x,y) = f2 . (x,y) ) holds
f1 = f2
let f1, f2 be Function of [:X,Y:],Z; :: thesis: ( ( for x, y being set st x in X & y in Y holds
f1 . (x,y) = f2 . (x,y) ) implies f1 = f2 )
assume A1: for x, y being set st x in X & y in Y holds
f1 . (x,y) = f2 . (x,y) ; :: thesis: f1 = f2
for z being object st z in [:X,Y:] holds
f1 . z = f2 . z

proof

let z be object ; :: thesis: ( z in [:X,Y:] implies f1 . z = f2 . z )
assume z in [:X,Y:] ; :: thesis: f1 . z = f2 . z
then consider x, y being object such that
A2: ( x in X & y in Y ) and
A3: z = [x,y] by ZFMISC_1:def 2;
( f1 . (x,y) = f1 . z & f2 . (x,y) = f2 . z ) by A3;
hence f1 . z = f2 . z by A1, A2; :: thesis: verum

end;

hence f1 = f2 by FUNCT_2:12; :: thesis: verum