theorem :: ALTCAT_1:20

for C being 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