let X, Y be non empty set ; :: thesis: for R, S being RMembership_Func of X,Y st ( for x being Element of X
for y being Element of Y holds R . (x,y) = S . (x,y) ) holds
R = S
let R, S be RMembership_Func of X,Y; :: thesis: ( ( for x being Element of X
for y being Element of Y holds R . (x,y) = S . (x,y) ) implies R = S )
assume A1: for x being Element of X
for y being Element of Y holds R . (x,y) = S . (x,y) ; :: thesis: R = S
A2: for x, y being object st [x,y] in dom R holds
R . (x,y) = S . (x,y)

proof

let x, y be object ; :: thesis: ( [x,y] in dom R implies R . (x,y) = S . (x,y) )
assume A3: [x,y] in dom R ; :: thesis: R . (x,y) = S . (x,y)
then reconsider x = x as Element of X by ZFMISC_1:87;
reconsider y = y as Element of Y by A3, ZFMISC_1:87;
R . (x,y) = S . (x,y) by A1;
hence R . (x,y) = S . (x,y) ; :: thesis: verum

end;

( dom R = [:X,Y:] & dom S = [:X,Y:] ) by FUNCT_2:def 1;
hence R = S by A2, BINOP_1:20; :: thesis: verum