for F being non empty Graph-yielding Function
for z being Element of dom F holds (the_Vertices_of (canGFDistinction (F,z))) . z = (the_Vertices_of F) . z