let V be non empty set ; 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); ( Hom (a,b) <> {} implies for f being Morphism of a,b st @ f is surjective holds
f is epi )
assume A1:
Hom (a,b) <> {}
; for f being Morphism of a,b st @ f is surjective holds
f is epi
let f be Morphism of a,b; ( @ f is surjective implies f is epi )
set m = @ f;
assume A2:
rng ((@ f) `2) = cod (@ f)
; ENS_1:def 8 f is epi
thus
Hom (a,b) <> {}
by A1; CAT_1:def 15 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); ( 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) <> {}
; 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; ( 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
; 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; verum