let G1, G2 be _Graph; :: thesis: for F being one-to-one PGraphMapping of G1,G2 st F is total & F is Dcontinuous holds
F " is Dcontinuous
let F be one-to-one PGraphMapping of G1,G2; :: thesis: ( F is total & F is Dcontinuous implies F " is Dcontinuous )
assume A1: ( F is total & F is Dcontinuous ) ; :: thesis: F " is Dcontinuous
then F " is onto by FUNCT_1:33;
hence F " is Dcontinuous by A1; :: thesis: verum