let F be non empty Graph-yielding Function; :: thesis: for x, z being Element of dom F st x <> z holds
(the_Vertices_of (canGFDistinction (F,z))) . x = (the_Vertices_of (canGFDistinction F)) . x
let x, z be Element of dom F; :: thesis: ( x <> z implies (the_Vertices_of (canGFDistinction (F,z))) . x = (the_Vertices_of (canGFDistinction F)) . x )
assume A1: x <> z ; :: thesis: (the_Vertices_of (canGFDistinction (F,z))) . x = (the_Vertices_of (canGFDistinction F)) . x
reconsider x1 = x as Element of dom (canGFDistinction F) by Def25;
reconsider x2 = x as Element of dom (canGFDistinction (F,z)) by Th95;
thus (the_Vertices_of (canGFDistinction (F,z))) . x = the_Vertices_of ((canGFDistinction (F,z)) . x2) by Def8
.= the_Vertices_of ((canGFDistinction F) . x1) by A1, FUNCT_7:32
.= (the_Vertices_of (canGFDistinction F)) . x by Def8 ; :: thesis: verum