let S be vertex-disjoint GraphUnionSet; :: thesis:
let G be GraphUnion of S; :: thesis:
assume A1: G is connected ; :: thesis:
set v = the Vertex of G;
the_Vertices_of G = union (the_Vertices_of S) by GLIB_014:def 25;
then consider X being set such that
A2: ( the Vertex of G in X & X in the_Vertices_of S ) by TARSKI:def 4;
consider H being _Graph such that
A3: ( H in S & X = the_Vertices_of H ) by A2, GLIB_014:def 14;
take H ; :: thesis:

now :: thesis:

let x be object ; :: thesis:
assume x in the_Vertices_of G ; :: thesis:
then reconsider w = x as Vertex of G ;
consider W being Walk of G such that
A4: W is_Walk_from the Vertex of G,w by A1, GLIB_002:def 1;
consider H9 being Element of S such that
A5: W is Walk of H9 by Th58;
reconsider W9 = W as Walk of H9 by A5;
W9 is_Walk_from the Vertex of G,w by A4, GLIB_001:19;
then A6: ( the Vertex of G is Vertex of H9 & w is Vertex of H9 ) by GLIB_001:18;
then the_Vertices_of H meets the_Vertices_of H9 by A2, A3, XBOOLE_0:3;
then H = H9 by A3, Def18;
hence x in the_Vertices_of H by A6; :: thesis:

end;

then A7: the_Vertices_of G c= the_Vertices_of H by TARSKI:def 3;

now :: thesis:

let Y be object ; :: thesis:
assume Y in S ; :: thesis:
then reconsider H9 = Y as Element of S ;
set w = the Vertex of H9;
H9 is Subgraph of G by GLIB_014:21;
then the_Vertices_of H9 c= the_Vertices_of G by GLIB_000:def 32;
then the Vertex of H9 in the_Vertices_of G by TARSKI:def 3;
then the_Vertices_of H meets the_Vertices_of H9 by A7, XBOOLE_0:3;
then Y = H by A3, Def18;
hence Y in {H} by TARSKI:def 1; :: thesis:

end;

hence S = {H} by TARSKI:def 3, ZFMISC_1:33; :: thesis: