theorem Th95: :: GLIB_015:95

for F being 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))) ) ) )