let S be vertex-disjoint GraphUnionSet; :: thesis: for G being GraphUnion of S st S is connected holds
card S = G .numComponents()
let G be GraphUnion of S; :: thesis: ( S is connected implies card S = G .numComponents() )
assume A1: S is connected ; :: thesis: card S = G .numComponents()
thus card S = card { (H .componentSet()) where H is Element of S : verum } by Lm2
.= card (SmallestPartition (the_Vertices_of S)) by A1, Th67
.= card (the_Vertices_of S) by TOPGEN_2:12
.= card (union (SmallestPartition (the_Vertices_of S))) by EQREL_1:def 4
.= card (union { (H .componentSet()) where H is Element of S : verum } ) by A1, Th67
.= card (G .componentSet()) by Th65
.= G .numComponents() by GLIB_002:def 9 ; :: thesis: verum