theorem Th100: :: GLIB_015:100

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