:: deftheorem Def25 defines canGFDistinction GLIB_015:def 25 :
for F being non empty Graph-yielding Function
for b₂ being Graph-yielding Function holds
( b₂ = canGFDistinction F iff ( dom b₂ = dom F & ( for x being Element of dom F holds b₂ . x = replaceVerticesEdges ((renameElementsDistinctlyFunc ((the_Vertices_of F),x)),(renameElementsDistinctlyFunc ((the_Edges_of F),x))) ) ) );