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