let C be category; :: thesis: for o being object of C holds (idm o) " = idm o
let o be object of C; :: thesis: (idm o) " = idm o
A1: <^o,o^> <> {} by ALTCAT_1:23;
( idm o is retraction & idm o is coretraction ) by Th1;
then A2: (idm o) " is_left_inverse_of idm o by A1, Def4;
thus (idm o) " = ((idm o) " ) * (idm o) by A1, ALTCAT_1:def 19
.= idm o by A2, Def1 ; :: thesis: verum