:: deftheorem Def36 defines * FUNCTOR0:def 36 :
for C1 being non empty AltGraph
for C2, C3 being non empty reflexive AltGraph
for F being feasible FunctorStr over C1,C2
for G being FunctorStr over C2,C3
for b₆ being strict FunctorStr over C1,C3 holds
( b₆ = G * F iff ( the ObjectMap of b₆ = the ObjectMap of G * the ObjectMap of F & the MorphMap of b₆ = ( the MorphMap of G * the ObjectMap of F) ** the MorphMap of F ) );