theorem :: MESFUN9C:36

for X being non empty set
for x being Element of X
for F being Functional_Sequence of X,COMPLEX
for f being PartFunc of X,COMPLEX st F is with_the_same_dom & dom f c= dom (F . 0) & x in dom f & F # x is summable & f . x = Sum (F # x) holds
f . x = lim ((Partial_Sums F) # x)