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