for X being non empty set
for S being SigmaField of X
for n being Nat
for F being Functional_Sequence of X,COMPLEX st ( for m being Nat holds F . m is_simple_func_in S ) holds
(Partial_Sums F) . n is_simple_func_in S