let G1, G2 be _Graph; :: thesis: for S being GraphSum of G1,G2 holds S .numComponents() = (G1 .numComponents()) +` (G2 .numComponents())
let S be GraphSum of G1,G2; :: thesis: S .numComponents() = (G1 .numComponents()) +` (G2 .numComponents())
S is GraphSum of <*G1,G2*> by Def28;
then consider G9 being GraphUnion of rng (canGFDistinction <*G1,G2*>) such that
A1: S is G9 -Disomorphic by Def27;
consider H being PGraphMapping of G9,S such that
A2: H is Disomorphism by A1, GLIB_010:def 24;
consider G3, G4 being _Graph such that
the_Edges_of G3 misses the_Edges_of G4 and
A3: G3 tolerates G4 and
A4: the_Vertices_of G3 misses the_Vertices_of G4 and
A5: G9 is GraphUnion of G3,G4 and
A6: ( G3 is G1 -Disomorphic & G4 is G2 -Disomorphic ) by Lm6;
consider H1 being PGraphMapping of G1,G3 such that
A7: H1 is Disomorphism by A6, GLIB_010:def 24;
consider H2 being PGraphMapping of G2,G4 such that
A8: H2 is Disomorphism by A6, GLIB_010:def 24;
thus S .numComponents() = G9 .numComponents() by A2, GLIBPRE1:83
.= (G3 .numComponents()) +` (G4 .numComponents()) by A3, A4, A5, GLIBPRE1:126
.= (G1 .numComponents()) +` (G4 .numComponents()) by A7, GLIBPRE1:83
.= (G1 .numComponents()) +` (G2 .numComponents()) by A8, GLIBPRE1:83 ; :: thesis: verum