the Comp of C is with_left_units by Def18;
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 by Def9;
reconsider d = d as Morphism of o,o by A4;
let a1, a2 be Morphism of o,o; :: thesis: ( ( 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 ; :: thesis: a1 = a2
A8: <^o,o^> <> {} by Th21;
hence a1 = (the Comp of C . o,o,o) . d,a1 by A5
.= d * a1 by A8, Def10
.= d by A6, Th21
.= d * a2 by A7, Th21
.= (the Comp of C . o,o,o) . d,a2 by A8, Def10
.= a2 by A5, A8 ;
:: thesis: verum