let C be category; :: thesis: 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; :: thesis: ( <^o1,o2^> <> {} & <^o2,o1^> <> {} implies for A being Morphism of o1,o2 st A is retraction & A is coretraction holds
(A " ) " = A )
assume A1: ( <^o1,o2^> <> {} & <^o2,o1^> <> {} ) ; :: thesis: for A being Morphism of o1,o2 st A is retraction & A is coretraction holds
(A " ) " = A
let A be Morphism of o1,o2; :: thesis: ( A is retraction & A is coretraction implies (A " ) " = A )
assume ( A is retraction & A is coretraction ) ; :: thesis: (A " ) " = A
then A2: ( A " is_left_inverse_of A & A " is_right_inverse_of A ) by A1, Def4;
then ( A " is retraction & A " is coretraction ) by Def2, Def3;
then A3: (A " ) " is_right_inverse_of A " by A1, Def4;
thus (A " ) " = (idm o2) * ((A " ) " ) by A1, ALTCAT_1:24
.= (A * (A " )) * ((A " ) " ) by A2, Def1
.= A * ((A " ) * ((A " ) " )) by A1, ALTCAT_1:25
.= A * (idm o1) by A3, Def1
.= A by A1, ALTCAT_1:def 19 ; :: thesis: verum