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 by Def1;
hence ( idm o is retraction & idm o is coretraction ) by Def2, Def3; :: thesis: verum