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

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