theorem Th98: :: GLIB_015:98

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