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