let F be non empty Graph-yielding Function; :: thesis: for x being Element of dom F
for S being GraphSum of F ex M being PGraphMapping of F . x,S st M is strong_SG-embedding
let x be Element of dom F; :: thesis: for S being GraphSum of F ex M being PGraphMapping of F . x,S st M is strong_SG-embedding
let S be GraphSum of F; :: thesis: ex M being PGraphMapping of F . x,S st M is strong_SG-embedding
set C = canGFDistinction F;
consider G9 being GraphUnion of rng (canGFDistinction F) such that
A1: S is G9 -Disomorphic by Def27;
consider M1 being PGraphMapping of G9,S such that
A2: M1 is Disomorphism by A1, GLIB_010:def 24;
set H = replaceVerticesEdges ((renameElementsDistinctlyFunc ((the_Vertices_of F),x)),(renameElementsDistinctlyFunc ((the_Edges_of F),x)));
set V = the_Vertices_of (replaceVerticesEdges ((renameElementsDistinctlyFunc ((the_Vertices_of F),x)),(renameElementsDistinctlyFunc ((the_Edges_of F),x))));
x in dom F ;
then ( replaceVerticesEdges ((renameElementsDistinctlyFunc ((the_Vertices_of F),x)),(renameElementsDistinctlyFunc ((the_Edges_of F),x))) = (canGFDistinction F) . x & x in dom (canGFDistinction F) ) by Def25;
then replaceVerticesEdges ((renameElementsDistinctlyFunc ((the_Vertices_of F),x)),(renameElementsDistinctlyFunc ((the_Edges_of F),x))) in rng (canGFDistinction F) by FUNCT_1:3;
then reconsider H = replaceVerticesEdges ((renameElementsDistinctlyFunc ((the_Vertices_of F),x)),(renameElementsDistinctlyFunc ((the_Edges_of F),x))) as inducedSubgraph of G9,(the_Vertices_of (replaceVerticesEdges ((renameElementsDistinctlyFunc ((the_Vertices_of F),x)),(renameElementsDistinctlyFunc ((the_Edges_of F),x))))) by Th62;
A3: M1 | H is strong_SG-embedding by A2, GLIB_010:58;
H is F . x -Disomorphic by Th17;
then consider M2 being PGraphMapping of F . x,H such that
A4: M2 is Disomorphism by GLIB_010:def 24;
take (M1 | H) * M2 ; :: thesis: (M1 | H) * M2 is strong_SG-embedding
thus (M1 | H) * M2 is strong_SG-embedding by A3, A4, GLIB_010:108; :: thesis: verum