let G1, G2 be _Graph; :: thesis: for G being GraphUnion of G1,G2 st G1 tolerates G2 & the_Vertices_of G1 misses the_Vertices_of G2 holds
( G .componentSet() = (G1 .componentSet()) \/ (G2 .componentSet()) & G .numComponents() = (G1 .numComponents()) +` (G2 .numComponents()) )
let G be GraphUnion of G1,G2; :: thesis: ( G1 tolerates G2 & the_Vertices_of G1 misses the_Vertices_of G2 implies ( G .componentSet() = (G1 .componentSet()) \/ (G2 .componentSet()) & G .numComponents() = (G1 .numComponents()) +` (G2 .numComponents()) ) )
assume A1: ( G1 tolerates G2 & the_Vertices_of G1 misses the_Vertices_of G2 ) ; :: thesis: ( G .componentSet() = (G1 .componentSet()) \/ (G2 .componentSet()) & G .numComponents() = (G1 .numComponents()) +` (G2 .numComponents()) )
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;

now :: thesis: for x being object holds
( ( not x in G .componentSet() or x in G1 .componentSet() or x in G2 .componentSet() ) & ( ( x in G1 .componentSet() or x in G2 .componentSet() ) implies x in G .componentSet() ) )

let x be object ; :: thesis: ( ( not x in G .componentSet() or x in G1 .componentSet() or x in G2 .componentSet() ) & ( ( x in G1 .componentSet() or x in G2 .componentSet() ) implies b₁ in G .componentSet() ) )

hereby :: thesis: ( ( x in G1 .componentSet() or x in G2 .componentSet() ) implies b₁ in G .componentSet() )

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

per cases ( v in the_Vertices_of G1 or v in the_Vertices_of G2 ) by A2, XBOOLE_0:def 3;

suppose v in the_Vertices_of G1 ; :: thesis: ( x in G1 .componentSet() or x in G2 .componentSet() )

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: verum

end;

suppose v in the_Vertices_of G2 ; :: thesis: ( x in G1 .componentSet() or x in G2 .componentSet() )

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: verum

end;

end;

end;

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

per cases then ( x in G1 .componentSet() or x in G2 .componentSet() ) ;

suppose x in G1 .componentSet() ; :: thesis: b₁ in G .componentSet()

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: verum

end;

suppose x in G2 .componentSet() ; :: thesis: b₁ in G .componentSet()

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: verum

end;

end;

end;

hence G .componentSet() = (G1 .componentSet()) \/ (G2 .componentSet()) by XBOOLE_0:def 3; :: thesis: G .numComponents() = (G1 .numComponents()) +` (G2 .numComponents())
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: verum