let C be non empty with_units AltCatStr ; :: thesis: for o being Object of C holds
( idm o is retraction & idm o is coretraction )
let o be Object of C; :: thesis: ( idm o is retraction & idm o is coretraction )
<^o,o^> <> {} by ALTCAT_1:19;
then (idm o) * (idm o) = idm o by ALTCAT_1:def 17;
then idm o is_left_inverse_of idm o ;
hence ( idm o is retraction & idm o is coretraction ) ; :: thesis: verum