let x be object ; :: thesis: for G being _Graph
for S being GraphSum of x .--> G holds S is G -Disomorphic
let G be _Graph; :: thesis: for S being GraphSum of x .--> G holds S is G -Disomorphic
let S be GraphSum of x .--> G; :: thesis: S is G -Disomorphic
x in {x} by TARSKI:def 1;
then x in dom {[x,G]} by RELAT_1:9;
then reconsider x0 = x as Element of dom (x .--> G) by FUNCT_4:82;
set H = replaceVerticesEdges ((renameElementsDistinctlyFunc ((the_Vertices_of (x .--> G)),x0)),(renameElementsDistinctlyFunc ((the_Edges_of (x .--> G)),x0)));
A1: (canGFDistinction (x .--> G)) . x = replaceVerticesEdges ((renameElementsDistinctlyFunc ((the_Vertices_of (x .--> G)),x0)),(renameElementsDistinctlyFunc ((the_Edges_of (x .--> G)),x0))) by Def25;
dom (canGFDistinction (x .--> G)) = dom (x .--> G) by Def25
.= dom {[x,G]} by FUNCT_4:82
.= {x} by RELAT_1:9 ;
then canGFDistinction (x .--> G) = x .--> (replaceVerticesEdges ((renameElementsDistinctlyFunc ((the_Vertices_of (x .--> G)),x0)),(renameElementsDistinctlyFunc ((the_Edges_of (x .--> G)),x0)))) by A1, DICKSON:1;
then A2: rng (canGFDistinction (x .--> G)) = {(replaceVerticesEdges ((renameElementsDistinctlyFunc ((the_Vertices_of (x .--> G)),x0)),(renameElementsDistinctlyFunc ((the_Edges_of (x .--> G)),x0))))} by FUNCOP_1:88;
consider G9 being GraphUnion of rng (canGFDistinction (x .--> G)) such that
A3: S is G9 -Disomorphic by Def27;
( replaceVerticesEdges ((renameElementsDistinctlyFunc ((the_Vertices_of (x .--> G)),x0)),(renameElementsDistinctlyFunc ((the_Edges_of (x .--> G)),x0))) is (x .--> G) . x0 -Disomorphic & (x .--> G) . x = G ) by Th17, FUNCOP_1:72;
then A4: replaceVerticesEdges ((renameElementsDistinctlyFunc ((the_Vertices_of (x .--> G)),x0)),(renameElementsDistinctlyFunc ((the_Edges_of (x .--> G)),x0))) is G -Disomorphic ;
G9 == replaceVerticesEdges ((renameElementsDistinctlyFunc ((the_Vertices_of (x .--> G)),x0)),(renameElementsDistinctlyFunc ((the_Edges_of (x .--> G)),x0))) by A2, GLIB_014:24;
then G9 is replaceVerticesEdges ((renameElementsDistinctlyFunc ((the_Vertices_of (x .--> G)),x0)),(renameElementsDistinctlyFunc ((the_Edges_of (x .--> G)),x0))) -Disomorphic by GLIBPRE0:76;
then G9 is G -Disomorphic by A4;
hence S is G -Disomorphic by A3; :: thesis: verum