theorem Th104: :: GLIB_015:104

for F being non empty Graph-yielding Function
for x, z being Element of dom F
for x9 being Element of dom (canGFDistinction (F,z)) st x = x9 holds
(canGFDistinction (F,z)) . x9 is F . x -Disomorphic