let F1, F2 be non empty Graph-yielding Function; :: thesis: 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
let z1 be Element of dom F1; :: thesis: for z2 being Element of dom F2 st F1,F2 are_Disomorphic holds
canGFDistinction (F1,z1), canGFDistinction (F2,z2) are_Disomorphic
let z2 be Element of dom F2; :: thesis: ( F1,F2 are_Disomorphic implies canGFDistinction (F1,z1), canGFDistinction (F2,z2) are_Disomorphic )
assume A1: F1,F2 are_Disomorphic ; :: thesis: canGFDistinction (F1,z1), canGFDistinction (F2,z2) are_Disomorphic
canGFDistinction (F1,z1),F1 are_Disomorphic by Th105;
then A2: canGFDistinction (F1,z1),F2 are_Disomorphic by A1, Th40;
F2, canGFDistinction (F2,z2) are_Disomorphic by Th105;
hence canGFDistinction (F1,z1), canGFDistinction (F2,z2) are_Disomorphic by A2, Th40; :: thesis: verum