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:19;
( 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 17
.= idm o by A2 ; :: thesis: verum