let o be Object of C; :: thesis: ( <^o,o^> <> {} & <^o,o^> <> {} & ex A being Morphism of o,o st A is iso )
thus A1: ( <^o,o^> <> {} & <^o,o^> <> {} ) by ALTCAT_1:19; :: thesis: ex A being Morphism of o,o st A is iso
take idm o ; :: thesis: idm o is iso
set A = idm o;
A2: ((idm o) ") * (idm o) = (idm o) * (idm o) by Th4
.= idm o by A1, ALTCAT_1:def 17 ;
(idm o) * ((idm o) ") = (idm o) * (idm o) by Th4
.= idm o by A1, ALTCAT_1:def 17 ;
hence idm o is iso by A2; :: thesis: verum