let C be category; for o1, o2 being Object of C st <^o1,o2^> <> {} & <^o2,o1^> <> {} holds
for A being Morphism of o1,o2 st A is retraction holds
A is epi
let o1, o2 be Object of C; ( <^o1,o2^> <> {} & <^o2,o1^> <> {} implies for A being Morphism of o1,o2 st A is retraction holds
A is epi )
assume A1:
( <^o1,o2^> <> {} & <^o2,o1^> <> {} )
; for A being Morphism of o1,o2 st A is retraction holds
A is epi
let A be Morphism of o1,o2; ( A is retraction implies A is epi )
assume
A is retraction
; A is epi
then consider R being Morphism of o2,o1 such that
A2:
R is_right_inverse_of A
;
let o be Object of C; ALTCAT_3:def 8 ( <^o2,o^> <> {} implies for B, C being Morphism of o2,o st B * A = C * A holds
B = C )
assume A3:
<^o2,o^> <> {}
; for B, C being Morphism of o2,o st B * A = C * A holds
B = C
let B, C be Morphism of o2,o; ( B * A = C * A implies B = C )
assume A4:
B * A = C * A
; B = C
thus B =
B * (idm o2)
by A3, ALTCAT_1:def 17
.=
B * (A * R)
by A2
.=
(C * A) * R
by A1, A3, A4, ALTCAT_1:21
.=
C * (A * R)
by A1, A3, ALTCAT_1:21
.=
C * (idm o2)
by A2
.=
C
by A3, ALTCAT_1:def 17
; verum