theorem Th96: :: GLIB_015:96

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