for C being non empty category
for f being morphism of C st f is identity holds
for g being morphism of (OrdC 2) holds (MORPHISM f) . g = f