let F be non empty Graph-yielding Function; :: thesis: for z being Element of dom F holds (the_Vertices_of (canGFDistinction (F,z))) . z = (the_Vertices_of F) . z
let z be Element of dom F; :: thesis: (the_Vertices_of (canGFDistinction (F,z))) . z = (the_Vertices_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_Vertices_of (canGFDistinction (F,z))) . z = the_Vertices_of ((canGFDistinction (F,z)) . z9) by Def8
.= the_Vertices_of ((F . z) | _GraphSelectors) by Th96
.= the_Vertices_of (F . z) by A1, GLIB_000:def 34
.= (the_Vertices_of F) . z by Def8 ; :: thesis: verum