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 ) )

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

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;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;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

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