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 coretraction holds
A is mono
let o1, o2 be Object of C; ( <^o1,o2^> <> {} & <^o2,o1^> <> {} implies for A being Morphism of o1,o2 st A is coretraction holds
A is mono )
assume A1:
( <^o1,o2^> <> {} & <^o2,o1^> <> {} )
; for A being Morphism of o1,o2 st A is coretraction holds
A is mono
let A be Morphism of o1,o2; ( A is coretraction implies A is mono )
assume
A is coretraction
; A is mono
then consider R being Morphism of o2,o1 such that
A2:
R is_left_inverse_of A
;
let o be Object of C; ALTCAT_3:def 7 ( <^o,o1^> <> {} implies for B, C being Morphism of o,o1 st A * B = A * C holds
B = C )
assume A3:
<^o,o1^> <> {}
; for B, C being Morphism of o,o1 st A * B = A * C holds
B = C
let B, C be Morphism of o,o1; ( A * B = A * C implies B = C )
assume A4:
A * B = A * C
; B = C
thus B =
(idm o1) * B
by A3, ALTCAT_1:20
.=
(R * A) * B
by A2
.=
R * (A * C)
by A1, A3, A4, ALTCAT_1:21
.=
(R * A) * C
by A1, A3, ALTCAT_1:21
.=
(idm o1) * C
by A2
.=
C
by A3, ALTCAT_1:20
; verum