let G be _Graph; :: thesis: 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 ") )
let V be non empty one-to-one ManySortedSet of the_Vertices_of G; :: thesis: 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 ") )
let E be one-to-one ManySortedSet of the_Edges_of G; :: thesis: ( 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 ") )
consider S, T being Function of (rng E),(rng V) such that
A1: ( S = (V * (the_Source_of G)) * (E ") & T = (V * (the_Target_of G)) * (E ") ) and
A2: replaceVerticesEdges (V,E) = createGraph ((rng V),(rng E),S,T) by Def1;
thus ( 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 ") ) by A1, A2; :: thesis: verum