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<sub>1</sub> being Element of the carrier of (Ens V) holds
( Hom (b,b<sub>1</sub>) = {} or for b<sub>2</sub>, b<sub>3</sub> being Morphism of b,b<sub>1</sub> holds
( not b<sub>2</sub> * f = b<sub>3</sub> * f or b<sub>2</sub> = b<sub>3</sub> ) )
let c be Object of (Ens V); :: thesis: ( Hom (b,c) = {} or for b<sub>1</sub>, b<sub>2</sub> being Morphism of b,c holds
( not b<sub>1</sub> * f = b<sub>2</sub> * f or b<sub>1</sub> = b<sub>2</sub> ) )
assume A3: Hom (b,c) <> {} ; :: thesis: for b<sub>1</sub>, b<sub>2</sub> being Morphism of b,c holds
( not b<sub>1</sub> * f = b<sub>2</sub> * f or b<sub>1</sub> = b<sub>2</sub> )
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