let F be non empty Graph-yielding Function; :: thesis: for z being Element of dom F
for G being Graph-yielding Function holds
( G = canGFDistinction (F,z) iff ( dom G = dom F & G . z = (F . z) | _GraphSelectors & ( 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))) ) ) )
let z be Element of dom F; :: thesis: for G being Graph-yielding Function holds
( G = canGFDistinction (F,z) iff ( dom G = dom F & G . z = (F . z) | _GraphSelectors & ( 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))) ) ) )
let G be Graph-yielding Function; :: thesis: ( G = canGFDistinction (F,z) iff ( dom G = dom F & G . z = (F . z) | _GraphSelectors & ( 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))) ) ) )
z in dom F ;
then A1: z in dom (canGFDistinction F) by Def25;

hereby :: thesis: ( dom G = dom F & G . z = (F . z) | _GraphSelectors & ( 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))) ) implies G = canGFDistinction (F,z) )

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

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: G = canGFDistinction (F,z)
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

proof

let x be object ; :: thesis: ( x in dom G implies G . x = (canGFDistinction (F,z)) . x )
assume A7: x in dom G ; :: thesis: G . x = (canGFDistinction (F,z)) . x

per cases ( x = z or x <> z ) ;

suppose x = z ; :: thesis: G . x = (canGFDistinction (F,z)) . x

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

end;

suppose A8: x <> z ; :: thesis: G . x = (canGFDistinction (F,z)) . x

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: verum

end;

end;

end;

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