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

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