(the_Vertices_of F) . x = the_Vertices_of (F . x) by Def8;
hence for b₁ being the_Vertices_of (F . x) -defined Function st b₁ = renameElementsDistinctlyFunc ((the_Vertices_of F),x) holds
b₁ is total ; :: thesis: verum