theorem :: GLIB_015:126

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