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

proof

let e be object ; :: thesis: ( e in the_Edges_of G2 implies e in rng ((DPVM2PGM 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 ((DPVM2PGM 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;
e DJoins (the_Source_of G2) . e,(the_Target_of G2) . e,G2 by A3, GLIB_000:def 14;
then A6: e DJoins f . v1,f . w1,G2 by A4, A5;
then consider e0 being object such that
A7: e0 DJoins v1,w1,G1 by A1, A4, A5;
e0 Joins v1,w1,G1 by A7, GLIB_000:16;
then e0 in G1 .edgesBetween (dom f) by A4, A5, GLIB_000:32;
then A8: e0 in dom ((DPVM2PGM f) _E) by Def11;
then ((DPVM2PGM f) _E) . e0 DJoins ((DPVM2PGM f) _V) . v1,((DPVM2PGM f) _V) . w1,G2 by A4, A5, A7, GLIB_010:def 14;
then ((DPVM2PGM f) _E) . e0 = e by A6, GLIB_000:def 21;
hence e in rng ((DPVM2PGM f) _E) by A8, FUNCT_1:def 3; :: thesis: verum

end;

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