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