for F being non empty Graph-yielding Function
for S being GraphSum of F st S is connected holds
ex x being object ex G being connected _Graph st F = x .--> G