let F be non empty Graph-yielding Function; 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; 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; ( 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 ( 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)
;
( 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
;
( 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;
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;
( x <> z implies G . x = replaceVerticesEdges ((renameElementsDistinctlyFunc ((the_Vertices_of F),x)),(renameElementsDistinctlyFunc ((the_Edges_of F),x))) )assume A3:
x <> z
;
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
;
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)))
; 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
hence
G = canGFDistinction (F,z)
by A6, FUNCT_1:2; verum