let C be non empty with_units AltCatStr ; :: thesis: 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; :: thesis: ( <^o1,o2^> <> {} implies for a being Morphism of o1,o2 holds (idm o2) * a = a )
assume A1: <^o1,o2^> <> {} ; :: thesis: for a being Morphism of o1,o2 holds (idm o2) * a = a
the Comp of C is with_left_units by Def18;
then consider d being set such that
A2: d in the Arrows of C . o2,o2 and
A3: for o' being Element of C
for f being set st f in the Arrows of C . o',o2 holds
(the Comp of C . o',o2,o2) . d,f = f by Def9;
reconsider d = d as Morphism of o2,o2 by A2;
idm o2 in <^o2,o2^> by Th23;
then A4: d = d * (idm o2) by Def19
.= (the Comp of C . o2,o2,o2) . d,(idm o2) by A2, Def10
.= idm o2 by A3, Th23 ;
let a be Morphism of o1,o2; :: thesis: (idm o2) * a = a
thus (idm o2) * a = (the Comp of C . o1,o2,o2) . d,a by A1, A2, A4, Def10
.= a by A1, A3 ; :: thesis: verum