let D be non empty SubCatStr of C; :: thesis: ( D is id-inheriting & D is transitive implies D is with_units )
assume that
A1: D is id-inheriting and
A2: D is transitive ; :: thesis: D is with_units
let o be Object of D; :: according to ALTCAT_2:def 9 :: thesis: ( <^o,o^> <> {} & ex i being Morphism of o,o st
for o9 being Object of D
for m9 being Morphism of o9,o
for m99 being Morphism of o,o9 holds
( ( <^o9,o^> <> {} implies i * m9 = m9 ) & ( <^o,o9^> <> {} implies m99 * i = m99 ) ) )
reconsider p = o as Object of C by Th29;
reconsider i = idm p as Morphism of o,o by A1, Def14;
A3: idm p in <^o,o^> by A1, Def14;
hence <^o,o^> <> {} ; :: thesis: ex i being Morphism of o,o st
for o9 being Object of D
for m9 being Morphism of o9,o
for m99 being Morphism of o,o9 holds
( ( <^o9,o^> <> {} implies i * m9 = m9 ) & ( <^o,o9^> <> {} implies m99 * i = m99 ) )
take i ; :: thesis: for o9 being Object of D
for m9 being Morphism of o9,o
for m99 being Morphism of o,o9 holds
( ( <^o9,o^> <> {} implies i * m9 = m9 ) & ( <^o,o9^> <> {} implies m99 * i = m99 ) )
let o9 be Object of D; :: thesis: for m9 being Morphism of o9,o
for m99 being Morphism of o,o9 holds
( ( <^o9,o^> <> {} implies i * m9 = m9 ) & ( <^o,o9^> <> {} implies m99 * i = m99 ) )
let m9 be Morphism of o9,o; :: thesis: for m99 being Morphism of o,o9 holds
( ( <^o9,o^> <> {} implies i * m9 = m9 ) & ( <^o,o9^> <> {} implies m99 * i = m99 ) )
let m99 be Morphism of o,o9; :: thesis: ( ( <^o9,o^> <> {} implies i * m9 = m9 ) & ( <^o,o9^> <> {} implies m99 * i = m99 ) )

hereby :: thesis: ( <^o,o9^> <> {} implies m99 * i = m99 )

reconsider p9 = o9 as Object of C by Th29;
assume A4: <^o9,o^> <> {} ; :: thesis: i * m9 = m9
then A5: <^p9,p^> <> {} by Th31, XBOOLE_1:3;
reconsider n9 = m9 as Morphism of p9,p by A4, Th33;
thus i * m9 = (idm p) * n9 by A2, A3, A4, Th32
.= m9 by A5, ALTCAT_1:20 ; :: thesis: verum

end;

reconsider p9 = o9 as Object of C by Th29;
assume A6: <^o,o9^> <> {} ; :: thesis: m99 * i = m99
then A7: <^p,p9^> <> {} by Th31, XBOOLE_1:3;
reconsider n99 = m99 as Morphism of p,p9 by A6, Th33;
thus m99 * i = n99 * (idm p) by A2, A3, A6, Th32
.= m99 by A7, ALTCAT_1:def 17 ; :: thesis: verum