the Comp of C is with_left_units
by Def16;
then consider d being set such that
A4:
d in the Arrows of C . (o,o)
and
A5:
for o9 being Element of C
for f being set st f in the Arrows of C . (o9,o) holds
( the Comp of C . (o9,o,o)) . (d,f) = f
;
reconsider d = d as Morphism of o,o by A4;
let a1, a2 be Morphism of o,o; ( ( for o9 being Object of C st <^o,o9^> <> {} holds
for a being Morphism of o,o9 holds a * a1 = a ) & ( for o9 being Object of C st <^o,o9^> <> {} holds
for a being Morphism of o,o9 holds a * a2 = a ) implies a1 = a2 )
assume that
A6:
for o9 being Object of C st <^o,o9^> <> {} holds
for a being Morphism of o,o9 holds a * a1 = a
and
A7:
for o9 being Object of C st <^o,o9^> <> {} holds
for a being Morphism of o,o9 holds a * a2 = a
; a1 = a2
A8:
<^o,o^> <> {}
by Th12;
hence a1 =
( the Comp of C . (o,o,o)) . (d,a1)
by A5
.=
d * a1
by A8, Def8
.=
d
by A6, Th12
.=
d * a2
by A7, Th12
.=
( the Comp of C . (o,o,o)) . (d,a2)
by A8, Def8
.=
a2
by A5, A8
;
verum