let X be non empty set ; :: thesis: for R, S being Membership_Func of X st ( for x being Element of X holds R . x = S . x ) holds
R = S
let R, S be Membership_Func of X; :: thesis: ( ( for x being Element of X holds R . x = S . x ) implies R = S )
assume A1: for x being Element of X holds R . x = S . x ; :: thesis: R = S
A2: ( dom R = X & dom S = X ) by FUNCT_2:def 1;
for x being Element of X st x in dom R holds
R . x = S . x by A1;
hence R = S by A2, PARTFUN1:34; :: thesis: verum