let G1, G2 be non-Dmulti _Graph; 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; ( f is one-to-one implies DPVM2PGM f is one-to-one )
assume A1:
f is one-to-one
; 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 ;
( 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 )
;
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_009:6;
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;
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; verum