let G1, G2 be non-Dmulti _Graph; :: thesis: for f being directed PVertexMapping of G1,G2 st f is one-to-one holds
DPVM2PGM f is one-to-one
let f be directed PVertexMapping of G1,G2; :: thesis: ( f is one-to-one implies DPVM2PGM f is one-to-one )
assume A1: f is one-to-one ; :: thesis: DPVM2PGM f is one-to-one
then A2: (DPVM2PGM f) _V is one-to-one ;
set g = (DPVM2PGM f) _E ;
for x1, x2 being object st x1 in dom ((DPVM2PGM f) _E) & x2 in dom ((DPVM2PGM f) _E) & ((DPVM2PGM f) _E) . x1 = ((DPVM2PGM f) _E) . x2 holds
x1 = x2

proof

let x1, x2 be object ; :: thesis: ( x1 in dom ((DPVM2PGM f) _E) & x2 in dom ((DPVM2PGM f) _E) & ((DPVM2PGM f) _E) . x1 = ((DPVM2PGM f) _E) . x2 implies x1 = x2 )
set v1 = (the_Source_of G1) . x1;
set w1 = (the_Target_of G1) . x1;
set v2 = (the_Source_of G1) . x2;
set w2 = (the_Target_of G1) . x2;
assume A3: ( x1 in dom ((DPVM2PGM f) _E) & x2 in dom ((DPVM2PGM f) _E) & ((DPVM2PGM f) _E) . x1 = ((DPVM2PGM f) _E) . x2 ) ; :: thesis: x1 = x2
then x1 in G1 .edgesBetween (dom f) by Def11;
then A4: ( x1 in the_Edges_of G1 & (the_Source_of G1) . x1 in dom f & (the_Target_of G1) . x1 in dom f ) by GLIB_000:31;
then A5: x1 DJoins (the_Source_of G1) . x1,(the_Target_of G1) . x1,G1 by GLIB_000:def 14;
then ((DPVM2PGM f) _E) . x1 DJoins ((DPVM2PGM f) _V) . ((the_Source_of G1) . x1),((DPVM2PGM f) _V) . ((the_Target_of G1) . x1),G2 by A3, A4, GLIB_010:def 14;
then A6: ((DPVM2PGM f) _E) . x1 DJoins f . ((the_Source_of G1) . x1),f . ((the_Target_of G1) . x1),G2 ;
x2 in G1 .edgesBetween (dom f) by A3, Def11;
then A7: ( x2 in the_Edges_of G1 & (the_Source_of G1) . x2 in dom f & (the_Target_of G1) . x2 in dom f ) by GLIB_000:31;
then A8: x2 DJoins (the_Source_of G1) . x2,(the_Target_of G1) . x2,G1 by GLIB_000:def 14;
then ((DPVM2PGM f) _E) . x2 DJoins ((DPVM2PGM f) _V) . ((the_Source_of G1) . x2),((DPVM2PGM f) _V) . ((the_Target_of G1) . x2),G2 by A3, A7, GLIB_010:def 14;
then ( f . ((the_Source_of G1) . x1) = f . ((the_Source_of G1) . x2) & f . ((the_Target_of G1) . x1) = f . ((the_Target_of G1) . x2) ) by A3, A6, GLIB_000:125;
then ( (the_Source_of G1) . x1 = (the_Source_of G1) . x2 & (the_Target_of G1) . x1 = (the_Target_of G1) . x2 ) by A1, A4, A7, FUNCT_1:def 4;
hence x1 = x2 by A5, A8, GLIB_000:def 21; :: thesis: verum

end;

then (DPVM2PGM f) _E is one-to-one by FUNCT_1:def 4;
hence DPVM2PGM f is one-to-one by A2, GLIB_010:def 13; :: thesis: verum