let C be category; for o1, o2 being object of C
for A being Morphism of o1,o2 st A is retraction & A is mono & <^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 retraction & A is mono & <^o1,o2^> <> {} & <^o2,o1^> <> {} holds
A is iso
let A be Morphism of o1,o2; ( A is retraction & A is mono & <^o1,o2^> <> {} & <^o2,o1^> <> {} implies A is iso )
assume that
A1:
A is retraction
and
A2:
A is mono
and
A3:
<^o1,o2^> <> {}
and
A4:
<^o2,o1^> <> {}
; A is iso
consider B being Morphism of o2,o1 such that
A5:
B is_right_inverse_of A
by A1, Def2;
(A * B) * A = (idm o2) * A
by A5, Def1;
then
A * (B * A) = (idm o2) * A
by A3, A4, ALTCAT_1:25;
then
A * (B * A) = A
by A3, ALTCAT_1:24;
then A6:
( <^o1,o1^> <> {} & A * (B * A) = A * (idm o1) )
by A3, ALTCAT_1:23, ALTCAT_1:def 19;
then
B * A = idm o1
by A2, Def7;
then A7:
B is_left_inverse_of A
by Def1;
then A8:
A is coretraction
by Def3;
then A9: A * (A " ) =
A * B
by A1, A3, A4, A5, A7, Def4
.=
idm o2
by A5, Def1
;
(A " ) * A =
B * A
by A1, A3, A4, A5, A7, A8, Def4
.=
idm o1
by A2, A6, Def7
;
hence
A is iso
by A9, Def5; verum