for G1, G2 being _Graph
for F being PGraphMapping of G1,G2
for H1 being Subgraph of G1
for H2 being Subgraph of G2 holds (H2 |` F) | H1 = H2 |` (F | H1)