let F be non empty Graph-yielding Function; :: thesis: for z being Element of dom F holds canGFDistinction F, canGFDistinction (F,z) are_Disomorphic
let z be Element of dom F; :: thesis: canGFDistinction F, canGFDistinction (F,z) are_Disomorphic
A1: canGFDistinction F,F are_Disomorphic by Th87;
F, canGFDistinction (F,z) are_Disomorphic by Th105;
hence canGFDistinction F, canGFDistinction (F,z) are_Disomorphic by A1, Th40; :: thesis: verum