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

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

hence
f1 = f2
by FUNCT_2:12; :: thesis: verum
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;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