for C being Category
for f being Morphism of C holds (id* C) . f = f opp