theorem :: GLIB_015:107

for F1, F2 being non empty Graph-yielding Function
for z1 being Element of dom F1
for z2 being Element of dom F2 st F1,F2 are_Disomorphic holds
canGFDistinction (F1,z1), canGFDistinction (F2,z2) are_Disomorphic