let S be vertex-disjoint GraphUnionSet; :: thesis: for G being GraphUnion of S holds G .componentSet() = union { (H .componentSet()) where H is Element of S : verum }
let G be GraphUnion of S; :: thesis: G .componentSet() = union { (H .componentSet()) where H is Element of S : verum }

now :: thesis: for x being object holds
( ( x in G .componentSet() implies x in union { (H .componentSet()) where H is Element of S : verum } ) & ( x in union { (H .componentSet()) where H is Element of S : verum } implies x in G .componentSet() ) )

let x be object ; :: thesis: ( ( x in G .componentSet() implies x in union { (H .componentSet()) where H is Element of S : verum } ) & ( x in union { (H .componentSet()) where H is Element of S : verum } implies x in G .componentSet() ) )

hereby :: thesis: ( x in union { (H .componentSet()) where H is Element of S : verum } implies x in G .componentSet() )

assume x in G .componentSet() ; :: thesis: x in union { (H .componentSet()) where H is Element of S : verum }
then consider v being Vertex of G such that
A1: x = G .reachableFrom v by GLIB_002:def 8;
the_Vertices_of G = union (the_Vertices_of S) by GLIB_014:def 25;
then consider X being set such that
A2: ( v in X & X in the_Vertices_of S ) by TARSKI:def 4;
consider H9 being _Graph such that
A3: ( H9 in S & X = the_Vertices_of H9 ) by A2, GLIB_014:def 14;
reconsider w = v as Vertex of H9 by A2, A3;
H9 .reachableFrom w = x by A1, A3, Th64;
then A4: x in H9 .componentSet() by GLIB_002:def 8;
H9 .componentSet() in { (H .componentSet()) where H is Element of S : verum } by A3;
hence x in union { (H .componentSet()) where H is Element of S : verum } by A4, TARSKI:def 4; :: thesis: verum

end;

assume x in union { (H .componentSet()) where H is Element of S : verum } ; :: thesis: x in G .componentSet()
then consider X being set such that
A5: ( x in X & X in { (H .componentSet()) where H is Element of S : verum } ) by TARSKI:def 4;
consider H being Element of S such that
A6: X = H .componentSet() by A5;
consider w being Vertex of H such that
A7: x = H .reachableFrom w by A5, A6, GLIB_002:def 8;
H is Subgraph of G by GLIB_014:21;
then the_Vertices_of H c= the_Vertices_of G by GLIB_000:def 32;
then reconsider v = w as Vertex of G by TARSKI:def 3;
x = G .reachableFrom v by A7, Th64;
hence x in G .componentSet() by GLIB_002:def 8; :: thesis: verum

end;

hence G .componentSet() = union { (H .componentSet()) where H is Element of S : verum } by TARSKI:2; :: thesis: verum