theorem :: GLIB_015:127

for F being non empty Graph-yielding connected Function
for S being GraphSum of F holds card F = S .numComponents()