the Comp of C is with_right_units by Def18;
then consider e being set such that
A1: e in the Arrows of C . o,o and
A2: for o' being Element of
for f being set st f in the Arrows of C . o,o' holds
(the Comp of C . o,o,o') . f,e = f by Def8;
reconsider e = e as Morphism of o,o by A1;
take e ; :: thesis: for o' being object of C st <^o,o'^> <> {} holds
for a being Morphism of o,o' holds a * e = a
let o' be object of C; :: thesis: ( <^o,o'^> <> {} implies for a being Morphism of o,o' holds a * e = a )
assume A3: <^o,o'^> <> {} ; :: thesis: for a being Morphism of o,o' holds a * e = a
let a be Morphism of o,o'; :: thesis: a * e = a
thus a * e = (the Comp of C . o,o,o') . a,e by A1, A3, Def10
.= a by A2, A3 ; :: thesis: verum