theorem :: GLIB_015:99

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