the Comp of C is with_right_units
by Def16;

then consider e being set such that

A1: e in the Arrows of C . (o,o) and

A2: for o9 being Element of C

for f being set st f in the Arrows of C . (o,o9) holds

( the Comp of C . (o,o,o9)) . (f,e) = f ;

reconsider e = e as Morphism of o,o by A1;

take e ; :: thesis: for o9 being Object of C st <^o,o9^> <> {} holds

for a being Morphism of o,o9 holds a * e = a

let o9 be Object of C; :: thesis: ( <^o,o9^> <> {} implies for a being Morphism of o,o9 holds a * e = a )

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

let a be Morphism of o,o9; :: thesis: a * e = a

thus a * e = ( the Comp of C . (o,o,o9)) . (a,e) by A1, A3, Def8

.= a by A2, A3 ; :: thesis: verum

then consider e being set such that

A1: e in the Arrows of C . (o,o) and

A2: for o9 being Element of C

for f being set st f in the Arrows of C . (o,o9) holds

( the Comp of C . (o,o,o9)) . (f,e) = f ;

reconsider e = e as Morphism of o,o by A1;

take e ; :: thesis: for o9 being Object of C st <^o,o9^> <> {} holds

for a being Morphism of o,o9 holds a * e = a

let o9 be Object of C; :: thesis: ( <^o,o9^> <> {} implies for a being Morphism of o,o9 holds a * e = a )

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

let a be Morphism of o,o9; :: thesis: a * e = a

thus a * e = ( the Comp of C . (o,o,o9)) . (a,e) by A1, A3, Def8

.= a by A2, A3 ; :: thesis: verum