let F be non empty Graph-yielding Function; :: thesis: for x being Element of dom F holds (the_Edges_of (canGFDistinction F)) . x = [:{[(the_Edges_of F),x]},((the_Edges_of F) . x):]
let x be Element of dom F; :: thesis: (the_Edges_of (canGFDistinction F)) . x = [:{[(the_Edges_of F),x]},((the_Edges_of F) . x):]
reconsider x9 = x as Element of dom (canGFDistinction F) by Def25;
thus (the_Edges_of (canGFDistinction F)) . x = the_Edges_of ((canGFDistinction F) . x9) by Def9
.= the_Edges_of (replaceVerticesEdges ((renameElementsDistinctlyFunc ((the_Vertices_of F),x)),(renameElementsDistinctlyFunc ((the_Edges_of F),x)))) by Def25
.= rng (renameElementsDistinctlyFunc ((the_Edges_of F),x)) by Th1
.= [:{[(the_Edges_of F),x]},((the_Edges_of F) . x):] by Th80 ; :: thesis: verum