let X, Y be set ; :: thesis: for f, g being Function st dom f = [:X,Y:] & dom g = [:X,Y:] & ( for x, y being object st x in X & y in Y holds
f . (x,y) = g . (x,y) ) holds
f = g
let f, g be Function; :: thesis: ( dom f = [:X,Y:] & dom g = [:X,Y:] & ( for x, y being object st x in X & y in Y holds
f . (x,y) = g . (x,y) ) implies f = g )
assume that
A1: ( dom f = [:X,Y:] & dom g = [:X,Y:] ) and
A2: for x, y being object st x in X & y in Y holds
f . (x,y) = g . (x,y) ; :: thesis: f = g
for p being object st p in [:X,Y:] holds
f . p = g . p

proof

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

end;

hence f = g by A1; :: thesis: verum