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 & A is coretraction holds
(A ") " = A
let o1, o2 be Object of C; ( <^o1,o2^> <> {} & <^o2,o1^> <> {} implies for A being Morphism of o1,o2 st A is retraction & A is coretraction holds
(A ") " = A )
assume that
A1:
<^o1,o2^> <> {}
and
A2:
<^o2,o1^> <> {}
; for A being Morphism of o1,o2 st A is retraction & A is coretraction holds
(A ") " = A
let A be Morphism of o1,o2; ( A is retraction & A is coretraction implies (A ") " = A )
assume A3:
( A is retraction & A is coretraction )
; (A ") " = A
then
A " is_left_inverse_of A
by A1, A2, Def4;
then A4:
A " is retraction
;
A5:
A " is_right_inverse_of A
by A1, A2, A3, Def4;
then
A " is coretraction
;
then A6:
(A ") " is_right_inverse_of A "
by A1, A2, A4, Def4;
thus (A ") " =
(idm o2) * ((A ") ")
by A1, ALTCAT_1:20
.=
(A * (A ")) * ((A ") ")
by A5
.=
A * ((A ") * ((A ") "))
by A1, A2, ALTCAT_1:21
.=
A * (idm o1)
by A6
.=
A
by A1, ALTCAT_1:def 17
; verum