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
; ObCat o is id-inheriting
now 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);
for o2 being Object of C st o1 = o2 holds
idm o2 in <^o1,o1^>let o2 be
Object of
C;
( o1 = o2 implies idm o2 in <^o1,o1^> )assume A2:
o1 = o2
;
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;
verum end;
hence
ObCat o is id-inheriting
by Def14; verum