let G1, G2 be non-Dmulti _Graph; :: thesis: for f being directed PVertexMapping of G1,G2 st f is Disomorphism holds
DPVM2PGM f is Disomorphism
let f be directed PVertexMapping of G1,G2; :: thesis: ( f is Disomorphism implies DPVM2PGM f is Disomorphism )
assume f is Disomorphism ; :: thesis: DPVM2PGM f is Disomorphism
then ( DPVM2PGM f is total & DPVM2PGM f is one-to-one & DPVM2PGM f is onto & DPVM2PGM f is Dcontinuous ) by Th33, Th35, Th37, Th41;
hence DPVM2PGM f is Disomorphism ; :: thesis: verum