let C be category; for D being non empty subcategory of C
for o being Object of D
for o9 being Object of C st o = o9 holds
idm o = idm o9
let D be non empty subcategory of C; for o being Object of D
for o9 being Object of C st o = o9 holds
idm o = idm o9
let o be Object of D; for o9 being Object of C st o = o9 holds
idm o = idm o9
let o9 be Object of C; ( o = o9 implies idm o = idm o9 )
assume A1:
o = o9
; idm o = idm o9
then reconsider m = idm o9 as Morphism of o,o by Def14;
A2:
idm o9 in <^o,o^>
by A1, Def14;
now for p being Object of D st <^o,p^> <> {} holds
for a being Morphism of o,p holds a * m = alet p be
Object of
D;
( <^o,p^> <> {} implies for a being Morphism of o,p holds a * m = a )assume A3:
<^o,p^> <> {}
;
for a being Morphism of o,p holds a * m = areconsider p9 =
p as
Object of
C by Th29;
A4:
<^o9,p9^> <> {}
by A1, A3, Th31, XBOOLE_1:3;
let a be
Morphism of
o,
p;
a * m = areconsider n =
a as
Morphism of
o9,
p9 by A1, A3, Th33;
thus a * m =
n * (idm o9)
by A1, A2, A3, Th32
.=
a
by A4, ALTCAT_1:def 17
;
verum end;
hence
idm o = idm o9
by ALTCAT_1:def 17; verum