A1: the carrier of (ObCat o) = {o} by Def12;
thus ObCat o is full :: thesis: ObCat o is id-inheriting

proof

thus 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 ; :: according to ALTCAT_2:def 13 :: thesis: verum

end;

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^> )
A2: o1 = o by Th24;
assume A3: o1 = o2 ; :: thesis: idm o2 in <^o1,o1^>
<^o1,o1^> = (o,o :-> <^o,o^>) . o,o by A2, Def12
.= <^o2,o2^> by A2, A3, ALTCAT_1:12 ;
hence idm o2 in <^o1,o1^> by ALTCAT_1:23; :: thesis: verum

end;

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