let f be Denumeration of X; :: thesis: f is with_cardinal_domain

per cases ( X = {} or X <> {} ) ;

suppose X = {} ; :: thesis: f is with_cardinal_domain

hence f is with_cardinal_domain ; :: thesis: verum

end;

suppose X <> {} ; :: thesis: f is with_cardinal_domain

hence f is with_cardinal_domain ; :: thesis: verum

end;

end;