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

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