let G1, G2 be _Graph; :: thesis: for F being one-to-one PGraphMapping of G1,G2
for H being Subgraph of G2 holds (H |` F) " = (F ") | H
let F be one-to-one PGraphMapping of G1,G2; :: thesis: for H being Subgraph of G2 holds (H |` F) " = (F ") | H
let H be Subgraph of G2; :: thesis: (H |` F) " = (F ") | H
((F ") | H) " = H |` ((F ") ") by Th82;
then (((F ") | H) ") " = (H |` F) " by Th70;
hence (H |` F) " = (F ") | H by Th70; :: thesis: verum