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