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

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