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

F is continuous

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

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

then F is semi-continuous by Th17;

hence F is continuous by A1, Th19; :: thesis: verum

F is continuous

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

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

then F is semi-continuous by Th17;

hence F is continuous by A1, Th19; :: thesis: verum