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 b_{1} being Element of the carrier of (Ens V) holds

( Hom (b,b_{1}) = {} or for b_{2}, b_{3} being Morphism of b,b_{1} holds

( not b_{2} * f = b_{3} * f or b_{2} = b_{3} ) )

let c be Object of (Ens V); :: thesis: ( Hom (b,c) = {} or for b_{1}, b_{2} being Morphism of b,c holds

( not b_{1} * f = b_{2} * f or b_{1} = b_{2} ) )

assume A3: Hom (b,c) <> {} ; :: thesis: for b_{1}, b_{2} being Morphism of b,c holds

( not b_{1} * f = b_{2} * f or b_{1} = b_{2} )

let f1, f2 be Morphism of b,c; :: thesis: ( not f1 * f = f2 * f or f1 = f2 )

A4: dom f1 = b by A3, CAT_1:5

.= cod f by A1, CAT_1:5 ;

A5: dom f2 = b by A3, CAT_1:5

.= cod f by A1, CAT_1:5 ;

A6: cod f1 = c by A3, CAT_1:5

.= cod f2 by A3, CAT_1:5 ;

assume A7: f1 * f = f2 * f ; :: thesis: f1 = f2

set m1 = @ f1;

set m2 = @ f2;

A8: (@ f1) * (@ f) = f1 (*) f by A4, Th27

.= f1 * f by A1, A3, CAT_1:def 13 ;

A9: (@ f2) * (@ f) = f2 (*) f by A5, Th27

.= f2 * f by A1, A3, CAT_1:def 13 ;

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 A5, A12, Def6;

A16: dom (@ f1) = dom f1 by Def9;

then (@ f1) * (@ f) = [[(dom (@ f)),(cod (@ f1))],(((@ f1) `2) * ((@ f) `2))] by A4, A14, Def6;

then A17: ((@ f1) `2) * ((@ f) `2) = ((@ f2) `2) * ((@ f) `2) by A7, A8, A15, A9, XTUPLE_0:1;

dom ((@ f1) `2) = dom f1 by A16, Lm3;

then (@ f1) `2 = (@ f2) `2 by A2, A4, A5, A14, A17, A13, FUNCT_1:86;

hence f1 = f2 by A4, A5, A6, A16, A12, A11, A10, Th8; :: thesis: verum

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 b

( Hom (b,b

( not b

let c be Object of (Ens V); :: thesis: ( Hom (b,c) = {} or for b

( not b

assume A3: Hom (b,c) <> {} ; :: thesis: for b

( not b

let f1, f2 be Morphism of b,c; :: thesis: ( not f1 * f = f2 * f or f1 = f2 )

A4: dom f1 = b by A3, CAT_1:5

.= cod f by A1, CAT_1:5 ;

A5: dom f2 = b by A3, CAT_1:5

.= cod f by A1, CAT_1:5 ;

A6: cod f1 = c by A3, CAT_1:5

.= cod f2 by A3, CAT_1:5 ;

assume A7: f1 * f = f2 * f ; :: thesis: f1 = f2

set m1 = @ f1;

set m2 = @ f2;

A8: (@ f1) * (@ f) = f1 (*) f by A4, Th27

.= f1 * f by A1, A3, CAT_1:def 13 ;

A9: (@ f2) * (@ f) = f2 (*) f by A5, Th27

.= f2 * f by A1, A3, CAT_1:def 13 ;

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 A5, A12, Def6;

A16: dom (@ f1) = dom f1 by Def9;

then (@ f1) * (@ f) = [[(dom (@ f)),(cod (@ f1))],(((@ f1) `2) * ((@ f) `2))] by A4, A14, Def6;

then A17: ((@ f1) `2) * ((@ f) `2) = ((@ f2) `2) * ((@ f) `2) by A7, A8, A15, A9, XTUPLE_0:1;

dom ((@ f1) `2) = dom f1 by A16, Lm3;

then (@ f1) `2 = (@ f2) `2 by A2, A4, A5, A14, A17, A13, FUNCT_1:86;

hence f1 = f2 by A4, A5, A6, A16, A12, A11, A10, Th8; :: thesis: verum