let G1, G2 be _Graph; for f being PartFunc of (the_Vertices_of G1),(the_Vertices_of G2) holds
( f is PVertexMapping of G1,G2 iff for v, w, e being object st v in dom f & w in dom f & e Joins v,w,G1 holds
ex e9 being object st e9 Joins f . v,f . w,G2 )
let f be PartFunc of (the_Vertices_of G1),(the_Vertices_of G2); ( f is PVertexMapping of G1,G2 iff for v, w, e being object st v in dom f & w in dom f & e Joins v,w,G1 holds
ex e9 being object st e9 Joins f . v,f . w,G2 )
hereby ( ( for v, w, e being object st v in dom f & w in dom f & e Joins v,w,G1 holds
ex e9 being object st e9 Joins f . v,f . w,G2 ) implies f is PVertexMapping of G1,G2 )
assume A1:
f is
PVertexMapping of
G1,
G2
;
for v, w, e being object st v in dom f & w in dom f & e Joins v,w,G1 holds
ex e9 being object st e9 Joins f . v,f . w,G2let v,
w,
e be
object ;
( v in dom f & w in dom f & e Joins v,w,G1 implies ex e9 being object st e9 Joins f . v,f . w,G2 )assume A2:
(
v in dom f &
w in dom f &
e Joins v,
w,
G1 )
;
ex e9 being object st e9 Joins f . v,f . w,G2then reconsider v0 =
v,
w0 =
w as
Vertex of
G1 ;
v0,
w0 are_adjacent
by A2, CHORD:def 3;
then consider e9 being
object such that A3:
e9 Joins f /. v0,
f /. w0,
G2
by A1, A2, Def1, CHORD:def 3;
take e9 =
e9;
e9 Joins f . v,f . w,G2
(
f /. v0 = f . v &
f /. w0 = f . w )
by A2, PARTFUN1:def 6;
hence
e9 Joins f . v,
f . w,
G2
by A3;
verum
end;
assume A4:
for v, w, e being object st v in dom f & w in dom f & e Joins v,w,G1 holds
ex e9 being object st e9 Joins f . v,f . w,G2
; f is PVertexMapping of G1,G2
let v, w be Vertex of G1; GLIB_011:def 1 ( v in dom f & w in dom f & v,w are_adjacent implies f /. v,f /. w are_adjacent )
assume A5:
( v in dom f & w in dom f )
; ( not v,w are_adjacent or f /. v,f /. w are_adjacent )
assume
v,w are_adjacent
; f /. v,f /. w are_adjacent
then consider e being object such that
A6:
e Joins v,w,G1
by CHORD:def 3;
consider e9 being object such that
A7:
e9 Joins f . v,f . w,G2
by A4, A5, A6;
( f /. v = f . v & f /. w = f . w )
by A5, PARTFUN1:def 6;
hence
f /. v,f /. w are_adjacent
by A7, CHORD:def 3; verum