let X be non empty set ; :: thesis: for x being object st x in Membership_Funcs X holds

ex f being Membership_Func of X st

( x = f & dom f = X )

let x be object ; :: thesis: ( x in Membership_Funcs X implies ex f being Membership_Func of X st

( x = f & dom f = X ) )

assume x in Membership_Funcs X ; :: thesis: ex f being Membership_Func of X st

( x = f & dom f = X )

then reconsider f = x as Membership_Func of X by Def1;

take f ; :: thesis: ( x = f & dom f = X )

thus x = f ; :: thesis: dom f = X

thus dom f = X by FUNCT_2:def 1; :: thesis: verum

ex f being Membership_Func of X st

( x = f & dom f = X )

let x be object ; :: thesis: ( x in Membership_Funcs X implies ex f being Membership_Func of X st

( x = f & dom f = X ) )

assume x in Membership_Funcs X ; :: thesis: ex f being Membership_Func of X st

( x = f & dom f = X )

then reconsider f = x as Membership_Func of X by Def1;

take f ; :: thesis: ( x = f & dom f = X )

thus x = f ; :: thesis: dom f = X

thus dom f = X by FUNCT_2:def 1; :: thesis: verum