let F be non empty Graph-yielding Function; :: thesis: for z being Element of dom F holds (the_Edges_of (canGFDistinction (F,z))) . z = (the_Edges_of F) . z
let z be Element of dom F; :: thesis: (the_Edges_of (canGFDistinction (F,z))) . z = (the_Edges_of F) . z
A1: F . z == (F . z) | _GraphSelectors by GLIB_000:128;
reconsider z9 = z as Element of dom (canGFDistinction (F,z)) by Th94;
thus (the_Edges_of (canGFDistinction (F,z))) . z = the_Edges_of ((canGFDistinction (F,z)) . z9) by Def9
.= the_Edges_of ((F . z) | _GraphSelectors) by Th96
.= the_Edges_of (F . z) by A1, GLIB_000:def 34
.= (the_Edges_of F) . z by Def9 ; :: thesis: verum