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

proof

let x1, x2 be object ; :: thesis: ( x1 in dom ((PVM2PGM f) _E) & x2 in dom ((PVM2PGM f) _E) & ((PVM2PGM f) _E) . x1 = ((PVM2PGM 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 ((PVM2PGM f) _E) & x2 in dom ((PVM2PGM f) _E) & ((PVM2PGM f) _E) . x1 = ((PVM2PGM f) _E) . x2 ) ; :: thesis: x1 = x2
then x1 in G1 .edgesBetween (dom f) by Def10;
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 Joins (the_Source_of G1) . x1,(the_Target_of G1) . x1,G1 by GLIB_000:def 13;
then ((PVM2PGM f) _E) . x1 Joins ((PVM2PGM f) _V) . ((the_Source_of G1) . x1),((PVM2PGM f) _V) . ((the_Target_of G1) . x1),G2 by A3, A4, GLIB_010:4;
then A6: ((PVM2PGM f) _E) . x1 Joins f . ((the_Source_of G1) . x1),f . ((the_Target_of G1) . x1),G2 ;
x2 in G1 .edgesBetween (dom f) by A3, Def10;
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 Joins (the_Source_of G1) . x2,(the_Target_of G1) . x2,G1 by GLIB_000:def 13;
then ((PVM2PGM f) _E) . x2 Joins ((PVM2PGM f) _V) . ((the_Source_of G1) . x2),((PVM2PGM f) _V) . ((the_Target_of G1) . x2),G2 by A3, A7, GLIB_010:4;

per cases 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) ) or ( f . ((the_Source_of G1) . x1) = f . ((the_Target_of G1) . x2) & f . ((the_Target_of G1) . x1) = f . ((the_Source_of G1) . x2) ) ) by A3, A6, GLIB_000:15;

suppose ( f . ((the_Source_of G1) . x1) = f . ((the_Source_of G1) . x2) & f . ((the_Target_of G1) . x1) = f . ((the_Target_of G1) . x2) ) ; :: thesis: x1 = x2

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 20; :: thesis: verum

end;

suppose ( f . ((the_Source_of G1) . x1) = f . ((the_Target_of G1) . x2) & f . ((the_Target_of G1) . x1) = f . ((the_Source_of G1) . x2) ) ; :: thesis: x1 = x2

then ( (the_Source_of G1) . x1 = (the_Target_of G1) . x2 & (the_Target_of G1) . x1 = (the_Source_of G1) . x2 ) by A1, A4, A7, FUNCT_1:def 4;
then x2 Joins (the_Source_of G1) . x1,(the_Target_of G1) . x1,G1 by A8, GLIB_000:14;
hence x1 = x2 by A5, GLIB_000:def 20; :: thesis: verum

end;

end;

end;

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