theorem Th101: :: GLIB_015:101

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