let G be _Graph; for V being non empty one-to-one ManySortedSet of the_Vertices_of G
for E being one-to-one ManySortedSet of the_Edges_of G
for e, v, w being object st e in dom E & v in dom V & w in dom V & E . e DJoins V . v,V . w, replaceVerticesEdges (V,E) holds
e DJoins v,w,G
let V be non empty one-to-one ManySortedSet of the_Vertices_of G; for E being one-to-one ManySortedSet of the_Edges_of G
for e, v, w being object st e in dom E & v in dom V & w in dom V & E . e DJoins V . v,V . w, replaceVerticesEdges (V,E) holds
e DJoins v,w,G
let E be one-to-one ManySortedSet of the_Edges_of G; for e, v, w being object st e in dom E & v in dom V & w in dom V & E . e DJoins V . v,V . w, replaceVerticesEdges (V,E) holds
e DJoins v,w,G
let e, v, w be object ; ( e in dom E & v in dom V & w in dom V & E . e DJoins V . v,V . w, replaceVerticesEdges (V,E) implies e DJoins v,w,G )
assume A1:
( e in dom E & v in dom V & w in dom V )
; ( not E . e DJoins V . v,V . w, replaceVerticesEdges (V,E) or e DJoins v,w,G )
then A2:
e in the_Edges_of G
;
assume A3:
E . e DJoins V . v,V . w, replaceVerticesEdges (V,E)
; e DJoins v,w,G
E . e in rng E
by A1, FUNCT_1:3;
then A4:
E . e in dom (E ")
by FUNCT_1:33;
A5:
( e in dom (the_Source_of G) & e in dom (the_Target_of G) )
by A2, FUNCT_2:def 1;
( (the_Source_of G) . e in the_Vertices_of G & (the_Target_of G) . e in the_Vertices_of G )
by A1, FUNCT_2:5;
then A6:
( (the_Source_of G) . e in dom V & (the_Target_of G) . e in dom V )
by PARTFUN1:def 2;
V . v =
(the_Source_of (replaceVerticesEdges (V,E))) . (E . e)
by A3, GLIB_000:def 14
.=
((V * (the_Source_of G)) * (E ")) . (E . e)
by Th1
.=
(V * (the_Source_of G)) . ((E ") . (E . e))
by A4, FUNCT_1:13
.=
(V * (the_Source_of G)) . e
by A1, FUNCT_1:34
.=
V . ((the_Source_of G) . e)
by A5, FUNCT_1:13
;
then A7:
v = (the_Source_of G) . e
by A1, A6, FUNCT_1:def 4;
V . w =
(the_Target_of (replaceVerticesEdges (V,E))) . (E . e)
by A3, GLIB_000:def 14
.=
((V * (the_Target_of G)) * (E ")) . (E . e)
by Th1
.=
(V * (the_Target_of G)) . ((E ") . (E . e))
by A4, FUNCT_1:13
.=
(V * (the_Target_of G)) . e
by A1, FUNCT_1:34
.=
V . ((the_Target_of G) . e)
by A5, FUNCT_1:13
;
then
w = (the_Target_of G) . e
by A1, A6, FUNCT_1:def 4;
hence
e DJoins v,w,G
by A1, A7, GLIB_000:def 14; verum