let G1, G2 be _Graph; :: thesis: 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)

let F be PGraphMapping of G1,G2; :: thesis: for H1 being Subgraph of G1

for H2 being Subgraph of G2 holds (H2 |` F) | H1 = H2 |` (F | H1)

let H1 be Subgraph of G1; :: thesis: for H2 being Subgraph of G2 holds (H2 |` F) | H1 = H2 |` (F | H1)

let H2 be Subgraph of G2; :: thesis: (H2 |` F) | H1 = H2 |` (F | H1)

thus (H2 |` F) | H1 = [((the_Vertices_of H2) |` ((F _V) | (the_Vertices_of H1))),(((the_Edges_of H2) |` (F _E)) | (the_Edges_of H1))] by RELAT_1:109

.= H2 |` (F | H1) by RELAT_1:109 ; :: thesis: verum

for H1 being Subgraph of G1

for H2 being Subgraph of G2 holds (H2 |` F) | H1 = H2 |` (F | H1)

let F be PGraphMapping of G1,G2; :: thesis: for H1 being Subgraph of G1

for H2 being Subgraph of G2 holds (H2 |` F) | H1 = H2 |` (F | H1)

let H1 be Subgraph of G1; :: thesis: for H2 being Subgraph of G2 holds (H2 |` F) | H1 = H2 |` (F | H1)

let H2 be Subgraph of G2; :: thesis: (H2 |` F) | H1 = H2 |` (F | H1)

thus (H2 |` F) | H1 = [((the_Vertices_of H2) |` ((F _V) | (the_Vertices_of H1))),(((the_Edges_of H2) |` (F _E)) | (the_Edges_of H1))] by RELAT_1:109

.= H2 |` (F | H1) by RELAT_1:109 ; :: thesis: verum