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)

hence R = S by A2, BINOP_1:20; :: thesis: verum

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

( dom R = [:X,Y:] & dom S = [:X,Y:] )
by FUNCT_2:def 1;
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;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

hence R = S by A2, BINOP_1:20; :: thesis: verum