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 G3 holds (H |` F2) * F1 = H |` (F2 * F1)

let F1 be PGraphMapping of G1,G2; :: thesis: for F2 being PGraphMapping of G2,G3

for H being Subgraph of G3 holds (H |` F2) * F1 = H |` (F2 * F1)

let F2 be PGraphMapping of G2,G3; :: thesis: for H being Subgraph of G3 holds (H |` F2) * F1 = H |` (F2 * F1)

let H be Subgraph of G3; :: thesis: (H |` F2) * F1 = H |` (F2 * F1)

thus (H |` F2) * F1 = [((the_Vertices_of H) |` ((F2 _V) * (F1 _V))),(((the_Edges_of H) |` (F2 _E)) * (F1 _E))] by RELAT_1:108

.= H |` (F2 * F1) by RELAT_1:108 ; :: thesis: verum

for F2 being PGraphMapping of G2,G3

for H being Subgraph of G3 holds (H |` F2) * F1 = H |` (F2 * F1)

let F1 be PGraphMapping of G1,G2; :: thesis: for F2 being PGraphMapping of G2,G3

for H being Subgraph of G3 holds (H |` F2) * F1 = H |` (F2 * F1)

let F2 be PGraphMapping of G2,G3; :: thesis: for H being Subgraph of G3 holds (H |` F2) * F1 = H |` (F2 * F1)

let H be Subgraph of G3; :: thesis: (H |` F2) * F1 = H |` (F2 * F1)

thus (H |` F2) * F1 = [((the_Vertices_of H) |` ((F2 _V) * (F1 _V))),(((the_Edges_of H) |` (F2 _E)) * (F1 _E))] by RELAT_1:108

.= H |` (F2 * F1) by RELAT_1:108 ; :: thesis: verum