let G1, G2 be _Graph; :: thesis: for F being directed PGraphMapping of G1,G2 st F _V is one-to-one & rng (F _E) = the_Edges_of G2 holds

F is Dcontinuous

let F be directed PGraphMapping of G1,G2; :: thesis: ( F _V is one-to-one & rng (F _E) = the_Edges_of G2 implies F is Dcontinuous )

assume A1: ( F _V is one-to-one & rng (F _E) = the_Edges_of G2 ) ; :: thesis: F is Dcontinuous

then F is semi-Dcontinuous by Th18;

hence F is Dcontinuous by A1, Th20; :: thesis: verum

F is Dcontinuous

let F be directed PGraphMapping of G1,G2; :: thesis: ( F _V is one-to-one & rng (F _E) = the_Edges_of G2 implies F is Dcontinuous )

assume A1: ( F _V is one-to-one & rng (F _E) = the_Edges_of G2 ) ; :: thesis: F is Dcontinuous

then F is semi-Dcontinuous by Th18;

hence F is Dcontinuous by A1, Th20; :: thesis: verum