let W be Universe; :: thesis: for a, b being Object of (Ens W) st Hom (a,b) <> {} holds
for f being Morphism of a,b st f is epi holds
@ f is surjective
let a, b be Object of (Ens W); :: thesis: ( Hom (a,b) <> {} implies for f being Morphism of a,b st f is epi holds
@ f is surjective )
assume Hom (a,b) <> {} ; :: thesis: for f being Morphism of a,b st f is epi holds
@ f is surjective
let f be Morphism of a,b; :: thesis: ( f is epi implies @ f is surjective )
( {} in W & {{}} in W ) by CLASSES2:56, CLASSES2:57;
then A1: {{},{{}}} in W by CLASSES2:58;
( {} in {{},{{}}} & {{}} in {{},{{}}} ) by TARSKI:def 2;
hence ( f is epi implies @ f is surjective ) by A1, Th36; :: thesis: verum