for T being non empty TopSpace
for FS1 being Functional_Sequence of the carrier of T,REAL st ( for n being Nat ex f being RealMap of T st
( FS1 . n = f & f is continuous & ( for p being Point of T holds f . p >= 0 ) ) ) & ex seq being Real_Sequence st
( seq is summable & ( for n being Nat
for p being Point of T holds (FS1 # p) . n <= seq . n ) ) holds
for f being RealMap of T st ( for p being Point of T holds f . p = Sum (FS1 # p) ) holds
f is continuous