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 <> z & x = x9 holds
ex G being PGraphMapping of F . x,(canGFDistinction (F,z)) . x9 st
( G _V = renameElementsDistinctlyFunc ((the_Vertices_of F),x) & G _E = renameElementsDistinctlyFunc ((the_Edges_of F),x) & G is Disomorphism )
let x, z be Element of dom F; :: thesis: for x9 being Element of dom (canGFDistinction (F,z)) st x <> z & x = x9 holds
ex G being PGraphMapping of F . x,(canGFDistinction (F,z)) . 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,z)); :: thesis: ( x <> z & x = x9 implies ex G being PGraphMapping of F . x,(canGFDistinction (F,z)) . x9 st
( G _V = renameElementsDistinctlyFunc ((the_Vertices_of F),x) & G _E = renameElementsDistinctlyFunc ((the_Edges_of F),x) & G is Disomorphism ) )
assume A1: ( x <> z & x = x9 ) ; :: thesis: ex G being PGraphMapping of F . x,(canGFDistinction (F,z)) . x9 st
( G _V = renameElementsDistinctlyFunc ((the_Vertices_of F),x) & G _E = renameElementsDistinctlyFunc ((the_Edges_of F),x) & G is Disomorphism )
reconsider x8 = x9 as Element of dom (canGFDistinction F) by FUNCT_7:30;
consider G0 being PGraphMapping of F . x,(canGFDistinction F) . x8 such that
A2: ( G0 _V = renameElementsDistinctlyFunc ((the_Vertices_of F),x) & G0 _E = renameElementsDistinctlyFunc ((the_Edges_of F),x) ) and
A3: G0 is Disomorphism by A1, Th85;
A4: (canGFDistinction F) . x8 = (canGFDistinction (F,z)) . x9 by A1, FUNCT_7:32;
then reconsider G = G0 as PGraphMapping of F . x,(canGFDistinction (F,z)) . x9 ;
take G ; :: thesis: ( G _V = renameElementsDistinctlyFunc ((the_Vertices_of F),x) & G _E = renameElementsDistinctlyFunc ((the_Edges_of F),x) & G is Disomorphism )
thus ( G _V = renameElementsDistinctlyFunc ((the_Vertices_of F),x) & G _E = renameElementsDistinctlyFunc ((the_Edges_of F),x) & G is Disomorphism ) by A2, A3, A4; :: thesis: verum