(the_Edges_of F) . x = the_Edges_of (F . x) by Def9;
hence renameElementsDistinctlyFunc ((the_Edges_of F),x) is the_Edges_of (F . x) -defined ; :: thesis: verum