let F be non empty Graph-yielding Function; :: thesis:
let z be Element of dom F; :: thesis:
let G be Graph-yielding Function; :: thesis:
z in dom F ;
then A1: z in dom (canGFDistinction F) by Def25;

hereby :: thesis:

assume A2: G = canGFDistinction (F,z) ; :: thesis:
hence dom G = dom (canGFDistinction F) by FUNCT_7:30
.= dom F by Def25 ;
:: thesis:
thus G . z = (F . z) | _GraphSelectors by A1, A2, FUNCT_7:31; :: thesis:
let x be Element of dom F; :: thesis:
assume A3: x <> z ; :: thesis:
thus G . x = (canGFDistinction F) . x by A2, A3, FUNCT_7:32
.= replaceVerticesEdges ((renameElementsDistinctlyFunc ((the_Vertices_of F),x)),(renameElementsDistinctlyFunc ((the_Edges_of F),x))) by Def25 ; :: thesis:

end;

assume that
A4: ( dom G = dom F & G . z = (F . z) | _GraphSelectors ) and
A5: for x being Element of dom F st x <> z holds
G . x = replaceVerticesEdges ((renameElementsDistinctlyFunc ((the_Vertices_of F),x)),(renameElementsDistinctlyFunc ((the_Edges_of F),x))) ; :: thesis:
A6: dom G = dom (canGFDistinction F) by A4, Def25
.= dom (canGFDistinction (F,z)) by FUNCT_7:30 ;
for x being object st x in dom G holds
G . x = (canGFDistinction (F,z)) . x

let x be object ; :: thesis:
assume A7: x in dom G ; :: thesis:

suppose x = z ; :: thesis:

hence G . x = (canGFDistinction (F,z)) . x by A1, A4, FUNCT_7:31; :: thesis:

end;

suppose A8: x <> z ; :: thesis:

reconsider x0 = x as Element of dom F by A4, A7;
thus G . x = replaceVerticesEdges ((renameElementsDistinctlyFunc ((the_Vertices_of F),x0)),(renameElementsDistinctlyFunc ((the_Edges_of F),x0))) by A5, A8
.= (canGFDistinction F) . x by Def25
.= (canGFDistinction (F,z)) . x by A8, FUNCT_7:32 ; :: thesis:

end;

end;

end;

hence G = canGFDistinction (F,z) by A6, FUNCT_1:2; :: thesis: