:: deftheorem Def9 defines right_composable CAT_6:def 9 :
for C being CategoryStr holds
( C is right_composable iff for f, f1, f2 being morphism of C st f1 |> f2 holds
( f |> f1 (*) f2 iff f |> f1 ) );