let F be non empty Graph-yielding Function; :: thesis: for x being Element of dom F
for x9 being Element of dom (canGFDistinction F) st x = x9 holds
ex G being PGraphMapping of F . x,(canGFDistinction F) . x9 st
( G _V = renameElementsDistinctlyFunc ((the_Vertices_of F),x) & G _E = renameElementsDistinctlyFunc ((the_Edges_of F),x) & G is Disomorphism )
let x be Element of dom F; :: thesis: for x9 being Element of dom (canGFDistinction F) st x = x9 holds
ex G being PGraphMapping of F . x,(canGFDistinction F) . x9 st
( G _V = renameElementsDistinctlyFunc ((the_Vertices_of F),x) & G _E = renameElementsDistinctlyFunc ((the_Edges_of F),x) & G is Disomorphism )
let x9 be Element of dom (canGFDistinction F); :: thesis: ( x = x9 implies ex G being PGraphMapping of F . x,(canGFDistinction F) . x9 st
( G _V = renameElementsDistinctlyFunc ((the_Vertices_of F),x) & G _E = renameElementsDistinctlyFunc ((the_Edges_of F),x) & G is Disomorphism ) )
assume x = x9 ; :: thesis: ex G being PGraphMapping of F . x,(canGFDistinction F) . x9 st
( G _V = renameElementsDistinctlyFunc ((the_Vertices_of F),x) & G _E = renameElementsDistinctlyFunc ((the_Edges_of F),x) & G is Disomorphism )
then (canGFDistinction F) . x9 = replaceVerticesEdges ((renameElementsDistinctlyFunc ((the_Vertices_of F),x)),(renameElementsDistinctlyFunc ((the_Edges_of F),x))) by Def25;
hence ex G being PGraphMapping of F . x,(canGFDistinction F) . x9 st
( G _V = renameElementsDistinctlyFunc ((the_Vertices_of F),x) & G _E = renameElementsDistinctlyFunc ((the_Edges_of F),x) & G is Disomorphism ) by Th16; :: thesis: verum