for G1, G2, G3, G4 being _Graph
for F1 being PGraphMapping of G1,G2
for F2 being PGraphMapping of G2,G3
for F3 being PGraphMapping of G3,G4 holds F3 * (F2 * F1) = (F3 * F2) * F1