theorem Th3: :: GLIB_015:3

for G being _Graph
for E being one-to-one ManySortedSet of the_Edges_of G holds
( the_Vertices_of (replaceEdges E) = the_Vertices_of G & the_Edges_of (replaceEdges E) = rng E & the_Source_of (replaceEdges E) = (the_Source_of G) * (E ") & the_Target_of (replaceEdges E) = (the_Target_of G) * (E ") )