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 ;
A3: idm p in <^o,o^> by ;
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 ;
reconsider n9 = m9 as Morphism of p9,p by ;
thus i * m9 = (idm p) * n9 by A2, A3, A4, Th32
.= m9 by ; :: 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 ;
reconsider n99 = m99 as Morphism of p,p9 by ;
thus m99 * i = n99 * (idm p) by A2, A3, A6, Th32
.= m99 by ; :: thesis: verum