let C be category; for o1, o2 being Object of C
for A being Morphism of o1,o2 st A is coretraction & A is epi & <^o1,o2^> <> {} & <^o2,o1^> <> {} holds
A is iso
let o1, o2 be Object of C; for A being Morphism of o1,o2 st A is coretraction & A is epi & <^o1,o2^> <> {} & <^o2,o1^> <> {} holds
A is iso
let A be Morphism of o1,o2; ( A is coretraction & A is epi & <^o1,o2^> <> {} & <^o2,o1^> <> {} implies A is iso )
assume that
A1:
A is coretraction
and
A2:
A is epi
and
A3:
<^o1,o2^> <> {}
and
A4:
<^o2,o1^> <> {}
; A is iso
consider B being Morphism of o2,o1 such that
A5:
B is_left_inverse_of A
by A1;
A * (B * A) = A * (idm o1)
by A5;
then
A * (B * A) = A
by A3, ALTCAT_1:def 17;
then
A * (B * A) = (idm o2) * A
by A3, ALTCAT_1:20;
then A6:
( <^o2,o2^> <> {} & (A * B) * A = (idm o2) * A )
by A3, A4, ALTCAT_1:19, ALTCAT_1:21;
then
A * B = idm o2
by A2;
then A7:
B is_right_inverse_of A
;
then A8:
A is retraction
;
then A9: (A ") * A =
B * A
by A1, A3, A4, A5, A7, Def4
.=
idm o1
by A5
;
A * (A ") =
A * B
by A1, A3, A4, A5, A7, A8, Def4
.=
idm o2
by A2, A6
;
hence
A is iso
by A9; verum