A1: the carrier of (ObCat o) = {o} by Def12;
the Arrows of (ObCat o) = (o,o) :-> <^o,o^> by Def12
.= the Arrows of C || the carrier of (ObCat o) by A1, FUNCT_7:8 ;
hence ObCat o is full by Def13; :: thesis: ObCat o is id-inheriting

now

let o1 be object of (ObCat o); :: thesis: for o2 being object of C st o1 = o2 holds
idm o2 in <^o1,o1^>
let o2 be object of C; :: thesis: ( o1 = o2 implies idm o2 in <^o1,o1^> )
assume A2: o1 = o2 ; :: thesis: idm o2 in <^o1,o1^>
A3: o1 = o by Th24;
then <^o1,o1^> = ((o,o) :-> <^o,o^>) . (o,o) by Def12
.= <^o2,o2^> by A3, A2, ALTCAT_1:10 ;
hence idm o2 in <^o1,o1^> by ALTCAT_1:19; :: thesis: verum

end;

hence ObCat o is id-inheriting by Def14; :: thesis: verum