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
(canGFDistinction F) . x9 is F . x -Disomorphic
let x be Element of dom F; :: thesis: for x9 being Element of dom (canGFDistinction F) st x = x9 holds
(canGFDistinction F) . x9 is F . x -Disomorphic
let x9 be Element of dom (canGFDistinction F); :: thesis: ( x = x9 implies (canGFDistinction F) . x9 is F . x -Disomorphic )
assume x = x9 ; :: thesis: (canGFDistinction F) . x9 is F . x -Disomorphic
then consider G being PGraphMapping of F . x,(canGFDistinction F) . x9 such that
( G _V = renameElementsDistinctlyFunc ((the_Vertices_of F),x) & G _E = renameElementsDistinctlyFunc ((the_Edges_of F),x) ) and
A1: G is Disomorphism by Th85;
thus (canGFDistinction F) . x9 is F . x -Disomorphic by A1, GLIB_010:def 24; :: thesis: verum