let X, Y be set ; :: thesis: for f, g being Function st dom f = [:X,Y:] & dom g = [:X,Y:] & ( for x, y being set 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 set 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 set st x in X & y in Y holds
f . x,y = g . x,y ; :: thesis: f = g
for p being set st p in [:X,Y:] holds
f . p = g . p

proof

let p be set ; :: 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 set such that
A3: ( x in X & y in Y & p = [x,y] ) by ZFMISC_1:def 2;
f . x,y = g . x,y by A2, A3;
hence f . p = g . p by A3; :: thesis: verum

end;

hence f = g by A1, FUNCT_1:9; :: thesis: verum