let C be non empty with_units AltCatStr ; for o1, o2 being Object of C st <^o1,o2^> <> {} holds
for a being Morphism of o1,o2 holds (idm o2) * a = a
let o1, o2 be Object of C; ( <^o1,o2^> <> {} implies for a being Morphism of o1,o2 holds (idm o2) * a = a )
assume A1:
<^o1,o2^> <> {}
; for a being Morphism of o1,o2 holds (idm o2) * a = a
let a be Morphism of o1,o2; (idm o2) * a = a
the Comp of C is with_left_units
by Def16;
then consider d being set such that
A2:
d in the Arrows of C . (o2,o2)
and
A3:
for o9 being Element of C
for f being set st f in the Arrows of C . (o9,o2) holds
( the Comp of C . (o9,o2,o2)) . (d,f) = f
;
reconsider d = d as Morphism of o2,o2 by A2;
idm o2 in <^o2,o2^>
by Th13;
then d =
d * (idm o2)
by Def17
.=
( the Comp of C . (o2,o2,o2)) . (d,(idm o2))
by A2, Def8
.=
idm o2
by A3, Th13
;
hence (idm o2) * a =
( the Comp of C . (o1,o2,o2)) . (d,a)
by A1, A2, Def8
.=
a
by A1, A3
;
verum