let F be non empty Graph-yielding Function; :: thesis: for x, z being Element of dom F
for x9 being Element of dom (canGFDistinction (F,z)) st x = x9 holds
(canGFDistinction (F,z)) . x9 is F . x -Disomorphic
let x, z be Element of dom F; :: thesis: for x9 being Element of dom (canGFDistinction (F,z)) st x = x9 holds
(canGFDistinction (F,z)) . x9 is F . x -Disomorphic
let x9 be Element of dom (canGFDistinction (F,z)); :: thesis: ( x = x9 implies (canGFDistinction (F,z)) . x9 is F . x -Disomorphic )
assume A1: x = x9 ; :: thesis: (canGFDistinction (F,z)) . x9 is F . x -Disomorphic

per cases ( x = z or x <> z ) ;

suppose x = z ; :: thesis: (canGFDistinction (F,z)) . x9 is F . x -Disomorphic

then (canGFDistinction (F,z)) . x = (F . x) | _GraphSelectors by Th96;
hence (canGFDistinction (F,z)) . x9 is F . x -Disomorphic by A1, GLIB_000:128, GLIBPRE0:76; :: thesis: verum

end;

suppose x <> z ; :: thesis: (canGFDistinction (F,z)) . x9 is F . x -Disomorphic

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: verum

end;

end;