theorem :: NATTRA_1:16

for A being Category
for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds (id A) /. f = f