theorem Th1: :: GLIB_015:1

for G being _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 holds
( the_Vertices_of (replaceVerticesEdges (V,E)) = rng V & the_Edges_of (replaceVerticesEdges (V,E)) = rng E & the_Source_of (replaceVerticesEdges (V,E)) = (V * (the_Source_of G)) * (E ") & the_Target_of (replaceVerticesEdges (V,E)) = (V * (the_Target_of G)) * (E ") )