for G1, G2, G3 being _Graph
for F1 being PGraphMapping of G1,G2
for F2 being PGraphMapping of G2,G3
for H being Subgraph of G3 holds (H |` F2) * F1 = H |` (F2 * F1)