for A, I being non empty reflexive AltCatStr
for B being non empty reflexive SubCatStr of A
for C being non empty SubCatStr of A
for D being non empty SubCatStr of B st C = D holds
for F being FunctorStr over A,I holds F | C = (F | B) | D