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

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