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 = idm o1 & A * (A ") = idm o2 )
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 = idm o1 & A * (A ") = idm o2 ) )
assume A1:
( <^o1,o2^> <> {} & <^o2,o1^> <> {} )
; for A being Morphism of o1,o2 st A is retraction & A is coretraction holds
( (A ") * A = idm o1 & A * (A ") = idm o2 )
let A be Morphism of o1,o2; ( A is retraction & A is coretraction implies ( (A ") * A = idm o1 & A * (A ") = idm o2 ) )
assume
( A is retraction & A is coretraction )
; ( (A ") * A = idm o1 & A * (A ") = idm o2 )
then
( A " is_left_inverse_of A & A " is_right_inverse_of A )
by A1, Def4;
hence
( (A ") * A = idm o1 & A * (A ") = idm o2 )
; verum