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 set st [x,y] in dom R holds
R . x,y = S . x,y

proof

let x, y be set ; :: 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:106;
reconsider y = y as Element of Y by A3, ZFMISC_1:106;
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:32; :: thesis: verum