:: deftheorem Def1 defines COMPOSITION CAT_8:def 1 :
for C being non empty category
for f1, f2 being morphism of C st f1 |> f2 holds
for b₄ being covariant Functor of (OrdC 3),C holds
( b₄ = COMPOSITION (f1,f2) iff for g1, g2 being morphism of (OrdC 3) st g1 |> g2 & not g1 is identity & not g2 is identity holds
( b₄ . g1 = f1 & b₄ . g2 = f2 ) );