let F be non empty Graph-yielding Function; :: thesis: for z being Element of dom F holds (canGFDistinction (F,z)) . z = (F . z) | _GraphSelectors
let z be Element of dom F; :: thesis: (canGFDistinction (F,z)) . z = (F . z) | _GraphSelectors
dom F = dom (canGFDistinction F) by Def25;
hence (canGFDistinction (F,z)) . z = (F . z) | _GraphSelectors by FUNCT_7:31; :: thesis: verum