let F be non empty Graph-yielding Function; :: thesis: for x being Element of dom F
for x9 being Element of dom (canGFDistinction F)
for v, e, w being object st x = x9 & e DJoins v,w,F . x holds
[(the_Edges_of F),x,e] DJoins [(the_Vertices_of F),x,v],[(the_Vertices_of F),x,w],(canGFDistinction F) . x9
let x be Element of dom F; :: thesis: for x9 being Element of dom (canGFDistinction F)
for v, e, w being object st x = x9 & e DJoins v,w,F . x holds
[(the_Edges_of F),x,e] DJoins [(the_Vertices_of F),x,v],[(the_Vertices_of F),x,w],(canGFDistinction F) . x9
let x9 be Element of dom (canGFDistinction F); :: thesis: for v, e, w being object st x = x9 & e DJoins v,w,F . x holds
[(the_Edges_of F),x,e] DJoins [(the_Vertices_of F),x,v],[(the_Vertices_of F),x,w],(canGFDistinction F) . x9
let v, e, w be object ; :: thesis: ( x = x9 & e DJoins v,w,F . x implies [(the_Edges_of F),x,e] DJoins [(the_Vertices_of F),x,v],[(the_Vertices_of F),x,w],(canGFDistinction F) . x9 )
assume x = x9 ; :: thesis: ( not e DJoins v,w,F . x or [(the_Edges_of F),x,e] DJoins [(the_Vertices_of F),x,v],[(the_Vertices_of F),x,w],(canGFDistinction F) . x9 )
then consider G being PGraphMapping of F . x,(canGFDistinction F) . x9 such that
A1: G _V = renameElementsDistinctlyFunc ((the_Vertices_of F),x) and
A2: G _E = renameElementsDistinctlyFunc ((the_Edges_of F),x) and
A3: G is Disomorphism by Th85;
assume A4: e DJoins v,w,F . x ; :: thesis: [(the_Edges_of F),x,e] DJoins [(the_Vertices_of F),x,v],[(the_Vertices_of F),x,w],(canGFDistinction F) . x9
then e Joins v,w,F . x by GLIB_000:16;
then A5: ( e in the_Edges_of (F . x) & v is Vertex of (F . x) & w is Vertex of (F . x) ) by GLIB_000:13, GLIB_000:def 13;
( dom (G _V) = the_Vertices_of (F . x) & dom (G _E) = the_Edges_of (F . x) ) by A3, GLIB_010:def 11;
then A6: (G _E) . e DJoins (G _V) . v,(G _V) . w,(canGFDistinction F) . x9 by A3, A4, A5, GLIB_010:def 14;
( dom F = dom (the_Vertices_of F) & dom F = dom (the_Edges_of F) ) by Def4, Def5;
then A7: ( x in dom (the_Vertices_of F) & x in dom (the_Edges_of F) ) ;
(the_Vertices_of F) . x = the_Vertices_of (F . x) by Def8;
then A8: ( v in (the_Vertices_of F) . x & w in (the_Vertices_of F) . x ) by A5;
e in (the_Edges_of F) . x by A5, Def9;
then [(the_Edges_of F),x,e] DJoins (G _V) . v,(G _V) . w,(canGFDistinction F) . x9 by A2, A6, A7, Th78;
then [(the_Edges_of F),x,e] DJoins [(the_Vertices_of F),x,v],(G _V) . w,(canGFDistinction F) . x9 by A1, A7, A8, Th78;
hence [(the_Edges_of F),x,e] DJoins [(the_Vertices_of F),x,v],[(the_Vertices_of F),x,w],(canGFDistinction F) . x9 by A1, A7, A8, Th78; :: thesis: verum