for F being non empty Graph-yielding Function
for x being Element of dom F holds (the_Vertices_of (canGFDistinction F)) . x = [:{[(the_Vertices_of F),x]},((the_Vertices_of F) . x):]