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; :: 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 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 ;

:: thesis: verum

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; :: 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 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 ;

:: thesis: verum