let G1, G2 be non-multi _Graph; :: thesis: for f being PVertexMapping of G1,G2 st f is isomorphism holds
PVM2PGM f is isomorphism
let f be PVertexMapping of G1,G2; :: thesis: ( f is isomorphism implies PVM2PGM f is isomorphism )
assume f is isomorphism ; :: thesis: PVM2PGM f is isomorphism
then ( PVM2PGM f is total & PVM2PGM f is one-to-one & PVM2PGM f is onto ) by Th32, Th34, Th36;
hence PVM2PGM f is isomorphism ; :: thesis: verum