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 for x being Element of X holds R . x = S . x ; :: thesis: R = S
then A1: for x being Element of X st x in dom R holds
R . x = S . x ;
( dom R = X & dom S = X ) by FUNCT_2:def 1;
hence R = S by A1, PARTFUN1:5; :: thesis: verum