let C be category; :: thesis: 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; :: thesis: 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; :: thesis: for o9 being Object of C st o = o9 holds

idm o = idm o9

let o9 be Object of C; :: thesis: ( o = o9 implies idm o = idm o9 )

assume A1: o = o9 ; :: thesis: 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;

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; :: thesis: 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; :: thesis: for o9 being Object of C st o = o9 holds

idm o = idm o9

let o9 be Object of C; :: thesis: ( o = o9 implies idm o = idm o9 )

assume A1: o = o9 ; :: thesis: 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 :: thesis: for p being Object of D st <^o,p^> <> {} holds

for a being Morphism of o,p holds a * m = a

hence
idm o = idm o9
by ALTCAT_1:def 17; :: thesis: verumfor a being Morphism of o,p holds a * m = a

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

reconsider 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; :: thesis: a * m = a

reconsider 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 ; :: thesis: verum

end;assume A3: <^o,p^> <> {} ; :: thesis: for a being Morphism of o,p holds a * m = a

reconsider 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; :: thesis: a * m = a

reconsider 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 ; :: thesis: verum