let G1, G2 be _Graph; :: thesis:
let G be GraphUnion of G1,G2; :: thesis:
assume A1: ( G1 tolerates G2 & the_Vertices_of G1 misses the_Vertices_of G2 ) ; :: thesis:
then A2: ( the_Vertices_of G = (the_Vertices_of G1) \/ (the_Vertices_of G2) & G is Supergraph of G2 ) by GLIB_014:25, GLIB_014:26;

let x be object ; :: thesis:

hereby :: thesis:

assume x in G .componentSet() ; :: thesis:
then consider v being Vertex of G such that
A3: x = G .reachableFrom v by GLIB_002:def 8;

per cases by A2, XBOOLE_0:def 3;

suppose v in the_Vertices_of G1 ; :: thesis:

then reconsider v1 = v as Vertex of G1 ;
x = G1 .reachableFrom v1 by A1, A3, Th127;
hence ( x in G1 .componentSet() or x in G2 .componentSet() ) by GLIB_002:def 8; :: thesis:

end;

suppose v in the_Vertices_of G2 ; :: thesis:

then reconsider v2 = v as Vertex of G2 ;
x = G2 .reachableFrom v2 by A1, A3, Th128;
hence ( x in G1 .componentSet() or x in G2 .componentSet() ) by GLIB_002:def 8; :: thesis:

end;

end;

end;

assume ( x in G1 .componentSet() or x in G2 .componentSet() ) ; :: thesis:

suppose x in G1 .componentSet() ; :: thesis:

then consider v1 being Vertex of G1 such that
A4: x = G1 .reachableFrom v1 by GLIB_002:def 8;
reconsider v = v1 as Vertex of G by GLIB_006:68;
x = G .reachableFrom v by A1, A4, Th127;
hence x in G .componentSet() by GLIB_002:def 8; :: thesis:

end;

suppose x in G2 .componentSet() ; :: thesis:

then consider v2 being Vertex of G2 such that
A5: x = G2 .reachableFrom v2 by GLIB_002:def 8;
reconsider v = v2 as Vertex of G by A2, GLIB_006:68;
x = G .reachableFrom v by A1, A5, Th128;
hence x in G .componentSet() by GLIB_002:def 8; :: thesis:

end;

end;

end;

hence G .componentSet() = (G1 .componentSet()) \/ (G2 .componentSet()) by XBOOLE_0:def 3; :: thesis:
hence G .numComponents() = card ((G1 .componentSet()) \/ (G2 .componentSet())) by GLIB_002:def 9
.= (card (G1 .componentSet())) +` (card (G2 .componentSet())) by A1, Lm5, CARD_2:35
.= (card (G1 .componentSet())) +` (G2 .numComponents()) by GLIB_002:def 9
.= (G1 .numComponents()) +` (G2 .numComponents()) by GLIB_002:def 9 ;
:: thesis: