let V be non empty set ; :: thesis: for a, b being Object of (Ens V) st Hom (a,b) <> {} holds
for f being Morphism of a,b st @ f is surjective holds
f is epi

let a, b be Object of (Ens V); :: thesis: ( Hom (a,b) <> {} implies for f being Morphism of a,b st @ f is surjective holds
f is epi )

assume A1: Hom (a,b) <> {} ; :: thesis: for f being Morphism of a,b st @ f is surjective holds
f is epi

let f be Morphism of a,b; :: thesis: ( @ f is surjective implies f is epi )
set m = @ f;
assume A2: rng ((@ f) `2) = cod (@ f) ; :: according to ENS_1:def 8 :: thesis: f is epi
thus Hom (a,b) <> {} by A1; :: according to CAT_1:def 15 :: thesis: for b1 being Element of the carrier of (Ens V) holds
( Hom (b,b1) = {} or for b2, b3 being Morphism of b,b1 holds
( not b2 * f = b3 * f or b2 = b3 ) )

let c be Object of (Ens V); :: thesis: ( Hom (b,c) = {} or for b1, b2 being Morphism of b,c holds
( not b1 * f = b2 * f or b1 = b2 ) )

assume A3: Hom (b,c) <> {} ; :: thesis: for b1, b2 being Morphism of b,c holds
( not b1 * f = b2 * f or b1 = b2 )

let f1, f2 be Morphism of b,c; :: thesis: ( not f1 * f = f2 * f or f1 = f2 )
A4: dom f1 = b by
.= cod f by ;
A5: dom f2 = b by
.= cod f by ;
A6: cod f1 = c by
.= cod f2 by ;
assume A7: f1 * f = f2 * f ; :: thesis: f1 = f2
set m1 = @ f1;
set m2 = @ f2;
A8: (@ f1) * (@ f) = f1 (*) f by
.= f1 * f by ;
A9: (@ f2) * (@ f) = f2 (*) f by
.= f2 * f by ;
A10: @ f1 = [[(dom (@ f1)),(cod (@ f1))],((@ f1) `2)] by Th8;
A11: ( cod (@ f1) = cod f1 & cod (@ f2) = cod f2 ) by Def10;
A12: dom (@ f2) = dom f2 by Def9;
then A13: dom ((@ f2) `2) = dom f2 by Lm3;
A14: cod (@ f) = cod f by Def10;
then A15: (@ f2) * (@ f) = [[(dom (@ f)),(cod (@ f2))],(((@ f2) `2) * ((@ f) `2))] by ;
A16: dom (@ f1) = dom f1 by Def9;
then (@ f1) * (@ f) = [[(dom (@ f)),(cod (@ f1))],(((@ f1) `2) * ((@ f) `2))] by ;
then A17: ((@ f1) `2) * ((@ f) `2) = ((@ f2) `2) * ((@ f) `2) by ;
dom ((@ f1) `2) = dom f1 by ;
then (@ f1) `2 = (@ f2) `2 by ;
hence f1 = f2 by A4, A5, A6, A16, A12, A11, A10, Th8; :: thesis: verum