let F be non empty Graph-yielding Function; :: thesis: F, canGFDistinction F are_Disomorphic
A1: dom F = dom (canGFDistinction F) by Def25;
for x being Element of dom F
for x9 being Element of dom (canGFDistinction F) st x = x9 holds
(canGFDistinction F) . x9 is F . x -Disomorphic by Th86;
hence F, canGFDistinction F are_Disomorphic by A1, Th38; :: thesis: verum