:: deftheorem Def5 defines right_identity CAT_6:def 5 :
for C being CategoryStr
for f being morphism of C holds
( f is right_identity iff for f1 being morphism of C st f1 |> f holds
f1 (*) f = f1 );