:: deftheorem defines | FUNCTOR0:def 37 :
for A, C being non empty reflexive AltCatStr
for B being non empty SubCatStr of A
for F being FunctorStr over A,C holds F | B = F * (incl B);