for X being non empty set
for F being Functional_Sequence of X,ExtREAL
for x being Element of X
for D being set st F is additive & F is with_the_same_dom & D c= dom (F . 0) & x in D holds
( ( Partial_Sums (F # x) is convergent_to_finite_number implies (Partial_Sums F) # x is convergent_to_finite_number ) & ( (Partial_Sums F) # x is convergent_to_finite_number implies Partial_Sums (F # x) is convergent_to_finite_number ) & ( Partial_Sums (F # x) is convergent_to_+infty implies (Partial_Sums F) # x is convergent_to_+infty ) & ( (Partial_Sums F) # x is convergent_to_+infty implies Partial_Sums (F # x) is convergent_to_+infty ) & ( Partial_Sums (F # x) is convergent_to_-infty implies (Partial_Sums F) # x is convergent_to_-infty ) & ( (Partial_Sums F) # x is convergent_to_-infty implies Partial_Sums (F # x) is convergent_to_-infty ) & ( Partial_Sums (F # x) is convergent implies (Partial_Sums F) # x is convergent ) & ( (Partial_Sums F) # x is convergent implies Partial_Sums (F # x) is convergent ) )