let X, Y be non empty set ; 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; ( ( 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)
; 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 ;
( [x,y] in dom R implies R . (x,y) = S . (x,y) )
assume A3:
[x,y] in dom R
;
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)
;
verum
end;
( dom R = [:X,Y:] & dom S = [:X,Y:] )
by FUNCT_2:def 1;
hence
R = S
by A2, BINOP_1:20; verum