theorem Th13: :: MESFUN9C:13

for X being non empty set
for F being Functional_Sequence of X,REAL
for x being Element of X
for D being set st F is with_the_same_dom & D c= dom (F . 0) & x in D holds
( Partial_Sums (F # x) is convergent iff (Partial_Sums F) # x is convergent )