let G1, G2 be _Graph; :: thesis: for F being one-to-one PGraphMapping of G1,G2

for H being Subgraph of G1 holds (F | H) " = H |` (F ")

let F be one-to-one PGraphMapping of G1,G2; :: thesis: for H being Subgraph of G1 holds (F | H) " = H |` (F ")

let H be Subgraph of G1; :: thesis: (F | H) " = H |` (F ")

reconsider f = F _V , g = F _E as one-to-one Function ;

thus (F | H) " = [((the_Vertices_of H) |` (f ")),((g | (the_Edges_of H)) ")] by GLIB_009:5

.= H |` (F ") by GLIB_009:5 ; :: thesis: verum

for H being Subgraph of G1 holds (F | H) " = H |` (F ")

let F be one-to-one PGraphMapping of G1,G2; :: thesis: for H being Subgraph of G1 holds (F | H) " = H |` (F ")

let H be Subgraph of G1; :: thesis: (F | H) " = H |` (F ")

reconsider f = F _V , g = F _E as one-to-one Function ;

thus (F | H) " = [((the_Vertices_of H) |` (f ")),((g | (the_Edges_of H)) ")] by GLIB_009:5

.= H |` (F ") by GLIB_009:5 ; :: thesis: verum