theorem Th14: :: MESFUN9C:14

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