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 = idm o1 & A * (A " ) = idm o2 )
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 = idm o1 & A * (A " ) = idm o2 ) )
assume A1: ( <^o1,o2^> <> {} & <^o2,o1^> <> {} ) ; :: thesis: 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; :: thesis: ( A is retraction & A is coretraction implies ( (A " ) * A = idm o1 & A * (A " ) = idm o2 ) )
assume ( A is retraction & A is coretraction ) ; :: thesis: ( (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 ) by Def1; :: thesis: verum