let F be non empty Graph-yielding Function; :: thesis:
let x, z be Element of dom F; :: thesis:
let x9 be Element of dom (canGFDistinction (F,z)); :: thesis:
assume A1: x = x9 ; :: thesis:

suppose x = z ; :: thesis:

then (canGFDistinction (F,z)) . x = (F . x) | _GraphSelectors by Th96;
hence (canGFDistinction (F,z)) . x9 is F . x -Disomorphic by A1, GLIB_009:9, GLIBPRE0:78; :: thesis:

end;

suppose x <> z ; :: thesis:

then consider G being PGraphMapping of F . x,(canGFDistinction (F,z)) . x9 such that
( G _V = renameElementsDistinctlyFunc ((the_Vertices_of F),x) & G _E = renameElementsDistinctlyFunc ((the_Edges_of F),x) ) and
A2: G is Disomorphism by A1, Th103;
thus (canGFDistinction (F,z)) . x9 is F . x -Disomorphic by A2, GLIB_010:def 24; :: thesis:

end;

end;