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

let a be Morphism of o1,o2; :: thesis: (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 ;

:: thesis: verum

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

let a be Morphism of o1,o2; :: thesis: (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 ;

:: thesis: verum