let G be _Graph; :: thesis: for V being non empty one-to-one ManySortedSet of the_Vertices_of G holds
( the_Vertices_of (replaceVertices V) = rng V & the_Edges_of (replaceVertices V) = the_Edges_of G & the_Source_of (replaceVertices V) = V * (the_Source_of G) & the_Target_of (replaceVertices V) = V * (the_Target_of G) )
let V be non empty one-to-one ManySortedSet of the_Vertices_of G; :: thesis: ( the_Vertices_of (replaceVertices V) = rng V & the_Edges_of (replaceVertices V) = the_Edges_of G & the_Source_of (replaceVertices V) = V * (the_Source_of G) & the_Target_of (replaceVertices V) = V * (the_Target_of G) )
thus the_Vertices_of (replaceVertices V) = rng V by Th1; :: thesis: ( the_Edges_of (replaceVertices V) = the_Edges_of G & the_Source_of (replaceVertices V) = V * (the_Source_of G) & the_Target_of (replaceVertices V) = V * (the_Target_of G) )
rng (id (the_Edges_of G)) = the_Edges_of G ;
hence the_Edges_of (replaceVertices V) = the_Edges_of G by Th1; :: thesis: ( the_Source_of (replaceVertices V) = V * (the_Source_of G) & the_Target_of (replaceVertices V) = V * (the_Target_of G) )
A1: (id (the_Edges_of G)) " = id (the_Edges_of G) by FUNCT_1:45;
dom (V * (the_Source_of G)) c= the_Edges_of G ;
then V * (the_Source_of G) = (V * (the_Source_of G)) * ((id (the_Edges_of G)) ") by A1, RELAT_1:51;
hence the_Source_of (replaceVertices V) = V * (the_Source_of G) by Th1; :: thesis: the_Target_of (replaceVertices V) = V * (the_Target_of G)
dom (V * (the_Target_of G)) c= the_Edges_of G ;
then V * (the_Target_of G) = (V * (the_Target_of G)) * ((id (the_Edges_of G)) ") by A1, RELAT_1:51;
hence the_Target_of (replaceVertices V) = V * (the_Target_of G) by Th1; :: thesis: verum