let G be _Graph; :: thesis: 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 ") )
let E be one-to-one ManySortedSet of the_Edges_of G; :: thesis: ( 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 ") )
rng (id (the_Vertices_of G)) = the_Vertices_of G ;
hence the_Vertices_of (replaceEdges E) = the_Vertices_of G by Th1; :: thesis: ( 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 ") )
thus the_Edges_of (replaceEdges E) = rng E by Th1; :: thesis: ( the_Source_of (replaceEdges E) = (the_Source_of G) * (E ") & the_Target_of (replaceEdges E) = (the_Target_of G) * (E ") )
rng ((the_Source_of G) * (E ")) c= the_Vertices_of G ;
then (the_Source_of G) * (E ") = (id (the_Vertices_of G)) * ((the_Source_of G) * (E ")) by RELAT_1:53
.= ((id (the_Vertices_of G)) * (the_Source_of G)) * (E ") by RELAT_1:36 ;
hence the_Source_of (replaceEdges E) = (the_Source_of G) * (E ") by Th1; :: thesis: the_Target_of (replaceEdges E) = (the_Target_of G) * (E ")
rng ((the_Target_of G) * (E ")) c= the_Vertices_of G ;
then (the_Target_of G) * (E ") = (id (the_Vertices_of G)) * ((the_Target_of G) * (E ")) by RELAT_1:53
.= ((id (the_Vertices_of G)) * (the_Target_of G)) * (E ") by RELAT_1:36 ;
hence the_Target_of (replaceEdges E) = (the_Target_of G) * (E ") by Th1; :: thesis: verum