let G1, G2 be _Graph; :: thesis: for F being one-to-one PGraphMapping of G1,G2 holds (F ") " = F
let F be one-to-one PGraphMapping of G1,G2; :: thesis: (F ") " = F
thus (F ") " = [(F _V),(((F _E) ") ")] by FUNCT_1:43
.= [(F _V),(F _E)] by FUNCT_1:43
.= F ; :: thesis: verum