theorem Th43: :: ENS_1:44

for C being Category
for a, c being Object of C holds hom ((id c),a) = id (Hom (c,a))