for A, B, C being non empty reflexive AltGraph
for F1, F2 being feasible FunctorStr over A,B
for G1, G2 being FunctorStr over B,C st FunctorStr(# the ObjectMap of F1, the MorphMap of F1 #) = FunctorStr(# the ObjectMap of F2, the MorphMap of F2 #) & FunctorStr(# the ObjectMap of G1, the MorphMap of G1 #) = FunctorStr(# the ObjectMap of G2, the MorphMap of G2 #) holds
G1 * F1 = G2 * F2