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