reconsider x0 = x as Element of dom (the_Vertices_of F) by Def4;
not renameElementsDistinctlyFunc ((the_Vertices_of F),x0) is empty ;
hence not renameElementsDistinctlyFunc ((the_Vertices_of F),x) is empty ; :: thesis: renameElementsDistinctlyFunc ((the_Vertices_of F),x) is the_Vertices_of (F . x) -defined
(the_Vertices_of F) . x = the_Vertices_of (F . x) by Def8;
hence renameElementsDistinctlyFunc ((the_Vertices_of F),x) is the_Vertices_of (F . x) -defined ; :: thesis: verum