let G1, G2, G3 be _Graph; :: thesis: for F1 being PGraphMapping of G1,G2
for F2 being PGraphMapping of G2,G3
for H being Subgraph of G1 holds F2 * (F1 | H) = (F2 * F1) | H
let F1 be PGraphMapping of G1,G2; :: thesis: for F2 being PGraphMapping of G2,G3
for H being Subgraph of G1 holds F2 * (F1 | H) = (F2 * F1) | H
let F2 be PGraphMapping of G2,G3; :: thesis: for H being Subgraph of G1 holds F2 * (F1 | H) = (F2 * F1) | H
let H be Subgraph of G1; :: thesis: F2 * (F1 | H) = (F2 * F1) | H
thus F2 * (F1 | H) = [(((F2 _V) * (F1 _V)) | (the_Vertices_of H)),((F2 _E) * ((F1 _E) | (the_Edges_of H)))] by RELAT_1:83
.= (F2 * F1) | H by RELAT_1:83 ; :: thesis: verum