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 ; :: thesis: ObCat o is id-inheriting

now :: thesis: for o1 being Object of (ObCat o)
for o2 being Object of C st o1 = o2 holds
idm o2 in <^o1,o1^>

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 Th23;
then <^o1,o1^> = ((o,o) :-> <^o,o^>) . (o,o) by Def12
.= <^o2,o2^> by A3, A2, FUNCT_4:80 ;
hence idm o2 in <^o1,o1^> by ALTCAT_1:19; :: thesis: verum

end;

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