let G1, G2 be non-multi _Graph; :: thesis: for f being PVertexMapping of G1,G2 st f is onto & f is continuous holds
PVM2PGM f is onto
let f be PVertexMapping of G1,G2; :: thesis: ( f is onto & f is continuous implies PVM2PGM f is onto )
assume A1: ( f is onto & f is continuous ) ; :: thesis: PVM2PGM f is onto
then A2: rng ((PVM2PGM f) _V) = the_Vertices_of G2 by FUNCT_2:def 3;
set g = (PVM2PGM f) _E ;
for e being object st e in the_Edges_of G2 holds
e in rng ((PVM2PGM f) _E)

proof

let e be object ; :: thesis: ( e in the_Edges_of G2 implies e in rng ((PVM2PGM f) _E) )
set v2 = (the_Source_of G2) . e;
set w2 = (the_Target_of G2) . e;
assume e in the_Edges_of G2 ; :: thesis: e in rng ((PVM2PGM f) _E)
then e in G2 .edgesBetween (the_Vertices_of G2) by GLIB_000:34;
then e in G2 .edgesBetween (rng f) by A1, FUNCT_2:def 3;
then A3: ( e in the_Edges_of G2 & (the_Source_of G2) . e in rng f & (the_Target_of G2) . e in rng f ) by GLIB_000:31;
consider v1 being object such that
A4: ( v1 in dom f & f . v1 = (the_Source_of G2) . e ) by A3, FUNCT_1:def 3;
consider w1 being object such that
A5: ( w1 in dom f & f . w1 = (the_Target_of G2) . e ) by A3, FUNCT_1:def 3;
A6: e Joins f . v1,f . w1,G2 by A3, A4, A5, GLIB_000:def 13;
then consider e0 being object such that
A7: e0 Joins v1,w1,G1 by A1, A4, A5, Th2;
e0 in G1 .edgesBetween (dom f) by A4, A5, A7, GLIB_000:32;
then A8: e0 in dom ((PVM2PGM f) _E) by Def10;
then ((PVM2PGM f) _E) . e0 Joins ((PVM2PGM f) _V) . v1,((PVM2PGM f) _V) . w1,G2 by A4, A5, A7, GLIB_010:4;
then ((PVM2PGM f) _E) . e0 = e by A6, GLIB_000:def 20;
hence e in rng ((PVM2PGM f) _E) by A8, FUNCT_1:def 3; :: thesis: verum

end;

then the_Edges_of G2 c= rng ((PVM2PGM f) _E) by TARSKI:def 3;
then rng ((PVM2PGM f) _E) = the_Edges_of G2 by XBOOLE_0:def 10;
hence PVM2PGM f is onto by A2, GLIB_010:def 12; :: thesis: verum