theorem Th24: :: CAT_1:29

for C being Category
for b, c being Object of C
for g being Morphism of b,c st Hom (b,c) <> {} holds
g * (id b) = g