let G1, G2 be _Graph; :: thesis: for G9 being GraphUnion of rng (canGFDistinction <*G1,G2*>) ex G3, G4 being _Graph st
( the_Edges_of G3 misses the_Edges_of G4 & G3 tolerates G4 & the_Vertices_of G3 misses the_Vertices_of G4 & G9 is GraphUnion of G3,G4 & G3 is G1 -Disomorphic & G4 is G2 -Disomorphic )
set F = <*G1,G2*>;
reconsider x = 1, y = 2 as Element of dom <*G1,G2*> by CALCUL_1:14;
set R = rng (canGFDistinction <*G1,G2*>);
let G9 be GraphUnion of rng (canGFDistinction <*G1,G2*>); :: thesis: ex G3, G4 being _Graph st
( the_Edges_of G3 misses the_Edges_of G4 & G3 tolerates G4 & the_Vertices_of G3 misses the_Vertices_of G4 & G9 is GraphUnion of G3,G4 & G3 is G1 -Disomorphic & G4 is G2 -Disomorphic )
A1: dom (canGFDistinction <*G1,G2*>) = dom <*G1,G2*> by Def25
.= {x,y} by FINSEQ_1:92 ;
then A2: ( x in dom (canGFDistinction <*G1,G2*>) & y in dom (canGFDistinction <*G1,G2*>) ) by TARSKI:def 2;
then reconsider G3 = (canGFDistinction <*G1,G2*>) . x, G4 = (canGFDistinction <*G1,G2*>) . y as _Graph ;
take G3 ; :: thesis: ex G4 being _Graph st
( the_Edges_of G3 misses the_Edges_of G4 & G3 tolerates G4 & the_Vertices_of G3 misses the_Vertices_of G4 & G9 is GraphUnion of G3,G4 & G3 is G1 -Disomorphic & G4 is G2 -Disomorphic )
take G4 ; :: thesis: ( the_Edges_of G3 misses the_Edges_of G4 & G3 tolerates G4 & the_Vertices_of G3 misses the_Vertices_of G4 & G9 is GraphUnion of G3,G4 & G3 is G1 -Disomorphic & G4 is G2 -Disomorphic )
thus the_Edges_of G3 misses the_Edges_of G4 by A2, Def23; :: thesis: ( G3 tolerates G4 & the_Vertices_of G3 misses the_Vertices_of G4 & G9 is GraphUnion of G3,G4 & G3 is G1 -Disomorphic & G4 is G2 -Disomorphic )
hence A3: G3 tolerates G4 by GLIB_014:12; :: thesis: ( the_Vertices_of G3 misses the_Vertices_of G4 & G9 is GraphUnion of G3,G4 & G3 is G1 -Disomorphic & G4 is G2 -Disomorphic )
thus the_Vertices_of G3 misses the_Vertices_of G4 by A2, Def22; :: thesis: ( G9 is GraphUnion of G3,G4 & G3 is G1 -Disomorphic & G4 is G2 -Disomorphic )
A4: dom (canGFDistinction <*G1,G2*>) = Seg 2 by A1, FINSEQ_1:2;
then reconsider p = canGFDistinction <*G1,G2*> as FinSequence by FINSEQ_1:def 2;
len p = 2 by A4, FINSEQ_1:def 3;
then p = <*G3,G4*> by FINSEQ_1:44;
then A5: rng p = {G3,G4} by FINSEQ_2:127;
then G3 in rng p by TARSKI:def 2;
then G3 is Subgraph of G9 by GLIB_014:21;
then G9 is Supergraph of G3 by GLIB_006:57;
hence G9 is GraphUnion of G3,G4 by A3, A5, GLIB_014:def 26; :: thesis: ( G3 is G1 -Disomorphic & G4 is G2 -Disomorphic )
A6: ( <*G1,G2*> . x = G1 & <*G1,G2*> . y = G2 ) ;
hence G3 is G1 -Disomorphic by A2, Th86; :: thesis: G4 is G2 -Disomorphic
thus G4 is G2 -Disomorphic by A2, A6, Th86; :: thesis: verum