theorem :: GLIB_015:131

for G1, G2 being _Graph
for S being GraphSum of G1,G2 holds S .numComponents() = (G1 .numComponents()) +` (G2 .numComponents())