:: deftheorem Def7 defines with_right_identities CAT_6:def 7 :
for C being CategoryStr holds
( C is with_right_identities iff for f1 being morphism of C st f1 in the carrier of C holds
ex f being morphism of C st
( f1 |> f & f is right_identity ) );