let F be non empty Graph-yielding Function; :: thesis: for z being Element of dom F holds F, canGFDistinction (F,z) are_Disomorphic
let z be Element of dom F; :: thesis: F, canGFDistinction (F,z) are_Disomorphic
A1: dom F = dom (canGFDistinction F) by Def25
.= dom (canGFDistinction (F,z)) by FUNCT_7:30 ;
for x 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 by Th104;
hence F, canGFDistinction (F,z) are_Disomorphic by A1, Th38; :: thesis: verum