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