let C be category; :: thesis: for D being non empty subcategory of C
for o being object of D
for o' being object of C st o = o' holds
idm o = idm o'
let D be non empty subcategory of C; :: thesis: for o being object of D
for o' being object of C st o = o' holds
idm o = idm o'
let o be object of D; :: thesis: for o' being object of C st o = o' holds
idm o = idm o'
let o' be object of C; :: thesis: ( o = o' implies idm o = idm o' )
assume A1: o = o' ; :: thesis: idm o = idm o'
then A2: idm o' in <^o,o^> by Def14;
reconsider m = idm o' as Morphism of o,o by A1, Def14;

now

let p be object of D; :: thesis: ( <^o,p^> <> {} implies for a being Morphism of o,p holds a * m = a )
assume A3: <^o,p^> <> {} ; :: thesis: for a being Morphism of o,p holds a * m = a
let a be Morphism of o,p; :: thesis: a * m = a
reconsider p' = p as object of C by Th30;
A4: <^o',p'^> <> {} by A1, A3, Th32, XBOOLE_1:3;
reconsider n = a as Morphism of o',p' by A1, A3, Th34;
thus a * m = n * (idm o') by A1, A2, A3, Th33
.= a by A4, ALTCAT_1:def 19 ; :: thesis: verum

end;

hence idm o = idm o' by ALTCAT_1:def 19; :: thesis: verum