let T be non empty TopSpace; :: thesis: 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

let FS1 be Functional_Sequence of the carrier of T,REAL; :: thesis: ( ( 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 ) ) implies for f being RealMap of T st ( for p being Point of T holds f . p = Sum (FS1 # p) ) holds
f is continuous )

assume that
A1: 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 ) ) and
A2: 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 ) ) ; :: thesis: for f being RealMap of T st ( for p being Point of T holds f . p = Sum (FS1 # p) ) holds
f is continuous

let f be RealMap of T; :: thesis: ( ( for p being Point of T holds f . p = Sum (FS1 # p) ) implies f is continuous )
assume A3: for p being Point of T holds f . p = Sum (FS1 # p) ; :: thesis: f is continuous
reconsider fR = f as Function of T,R^1 by TOPMETR:17;
now :: thesis: for p being Point of T holds fR is_continuous_at p
let p be Point of T; :: thesis:
for R being Subset of R^1 st R is open & fR . p in R holds
ex U being Subset of T st
( U is open & p in U & fR .: U c= R )
proof
reconsider fRp = fR . p as Point of RealSpace by ;
let R be Subset of R^1; :: thesis: ( R is open & fR . p in R implies ex U being Subset of T st
( U is open & p in U & fR .: U c= R ) )

assume ( R is open & fR . p in R ) ; :: thesis: ex U being Subset of T st
( U is open & p in U & fR .: U c= R )

then consider rn being Real such that
A4: rn > 0 and
A5: Ball (fRp,rn) c= R by ;
set r2 = rn / 2;
set r4 = rn / 4;
reconsider r2 = rn / 2, r4 = rn / 4 as Real ;
A6: r4 > 0 by ;
consider seq being Real_Sequence such that
A7: seq is summable and
A8: for n being Nat
for q being Point of T holds (FS1 # q) . n <= seq . n by A2;
Partial_Sums seq is convergent by ;
then consider n being Nat such that
A9: for m being Nat st n <= m holds
|.(((Partial_Sums seq) . m) - (lim (Partial_Sums seq))).| < r4 by ;
defpred S1[ object , object ] means ex SS being Subset of T st
( SS = \$2 & SS is open & p in SS & ( for f1 being RealMap of T st FS1 . \$1 = f1 holds
for f1p being Point of RealSpace st f1p = f1 . p holds
f1 .: SS c= Ball (f1p,(r2 / (n + 1))) ) );
A10: for k being object st k in \/ (Seg n) holds
ex U being object st
( U in bool the carrier of T & S1[k,U] )
proof
let k be object ; :: thesis: ( k in \/ (Seg n) implies ex U being object st
( U in bool the carrier of T & S1[k,U] ) )

assume k in \/ (Seg n) ; :: thesis: ex U being object st
( U in bool the carrier of T & S1[k,U] )

then ( k in Seg n or k in ) by XBOOLE_0:def 3;
then reconsider k = k as Element of NAT by TARSKI:def 1;
consider f1 being RealMap of T such that
A11: FS1 . k = f1 and
A12: f1 is continuous and
for p being Point of T holds f1 . p >= 0 by A1;
reconsider f19 = f1 as Function of T,R^1 by TOPMETR:17;
reconsider f1p = f19 . p as Point of RealSpace by ;
set B = Ball (f1p,(r2 / (n + 1)));
reconsider B = Ball (f1p,(r2 / (n + 1))) as Subset of R^1 by ;
( dist (f1p,f1p) = 0 & r2 > 0 ) by ;
then dist (f1p,f1p) < r2 / (n + 1) by XREAL_1:139;
then A13: f1p in B by METRIC_1:11;
f19 is continuous by ;
then ( B is open & f19 is_continuous_at p ) by ;
then consider U being Subset of T such that
A14: ( U is open & p in U ) and
A15: f19 .: U c= B by ;
for f1 being RealMap of T st FS1 . k = f1 holds
for f1p being Point of RealSpace st f1p = f1 . p holds
f1 .: U c= Ball (f1p,(r2 / (n + 1))) by ;
hence ex U being object st
( U in bool the carrier of T & S1[k,U] ) by A14; :: thesis: verum
end;
consider FSn being Function of ( \/ (Seg n)),(bool the carrier of T) such that
A16: for k being object st k in \/ (Seg n) holds
S1[k,FSn . k] from A17: for k being Nat
for q being Point of T holds (FS1 # q) . k >= 0
proof
let k be Nat; :: thesis: for q being Point of T holds (FS1 # q) . k >= 0
let q be Point of T; :: thesis: (FS1 # q) . k >= 0
( ex f1 being RealMap of T st
( FS1 . k = f1 & f1 is continuous & ( for q being Point of T holds f1 . q >= 0 ) ) & (FS1 . k) . q = (FS1 # q) . k ) by ;
hence (FS1 # q) . k >= 0 ; :: thesis: verum
end;
A18: for k being Nat holds (seq ^\ (n + 1)) . k >= 0
proof
let k be Nat; :: thesis: (seq ^\ (n + 1)) . k >= 0
( 0 <= (FS1 # p) . ((n + 1) + k) & seq . ((n + 1) + k) = (seq ^\ (n + 1)) . k ) by ;
hence (seq ^\ (n + 1)) . k >= 0 by A8; :: thesis: verum
end;
reconsider RNG = rng FSn as Subset-Family of T ;
A19: RNG is open
proof
let Q be Subset of T; :: according to TOPS_2:def 1 :: thesis: ( not Q in RNG or Q is open )
assume Q in RNG ; :: thesis: Q is open
then consider x being object such that
A20: x in dom FSn and
A21: FSn . x = Q by FUNCT_1:def 3;
ex SS being Subset of T st
( SS = FSn . x & SS is open & p in SS & ( for f1 being RealMap of T st FS1 . x = f1 holds
for f1p being Point of RealSpace st f1p = f1 . p holds
f1 .: SS c= Ball (f1p,(r2 / (n + 1))) ) ) by ;
hence Q is open by A21; :: thesis: verum
end;
0 in by TARSKI:def 1;
then 0 in \/ (Seg n) by XBOOLE_0:def 3;
then reconsider RNG = RNG as non empty Subset-Family of T by FUNCT_2:4;
A22: ( lim (Partial_Sums seq) = Sum seq & Sum seq = ((Partial_Sums seq) . n) + (Sum (seq ^\ (n + 1))) ) by ;
|.(((Partial_Sums seq) . n) - (lim (Partial_Sums seq))).| < r4 by A9;
then |.(- (Sum (seq ^\ (n + 1)))).| < r4 by A22;
then A23: |.(Sum (seq ^\ (n + 1))).| < r4 by COMPLEX1:52;
seq ^\ (n + 1) is summable by ;
then Sum (seq ^\ (n + 1)) >= 0 by ;
then A24: Sum (seq ^\ (n + 1)) < r4 by ;
A25: for q being Point of T holds
( FS1 # q is summable & 0 <= Sum ((FS1 # q) ^\ (n + 1)) & Sum ((FS1 # q) ^\ (n + 1)) < r4 )
proof
let q be Point of T; :: thesis: ( FS1 # q is summable & 0 <= Sum ((FS1 # q) ^\ (n + 1)) & Sum ((FS1 # q) ^\ (n + 1)) < r4 )
set F = FS1 # q;
A26: now :: thesis: for k being Nat holds
( 0 <= ((FS1 # q) ^\ (n + 1)) . k & ((FS1 # q) ^\ (n + 1)) . k <= (seq ^\ (n + 1)) . k )
let k be Nat; :: thesis: ( 0 <= ((FS1 # q) ^\ (n + 1)) . k & ((FS1 # q) ^\ (n + 1)) . k <= (seq ^\ (n + 1)) . k )
A27: seq . ((n + 1) + k) = (seq ^\ (n + 1)) . k by NAT_1:def 3;
( 0 <= (FS1 # q) . ((n + 1) + k) & (FS1 # q) . ((n + 1) + k) <= seq . ((n + 1) + k) ) by ;
hence ( 0 <= ((FS1 # q) ^\ (n + 1)) . k & ((FS1 # q) ^\ (n + 1)) . k <= (seq ^\ (n + 1)) . k ) by ; :: thesis: verum
end;
A28: for k being Nat holds
( 0 <= (FS1 # q) . k & (FS1 # q) . k <= seq . k ) by ;
then FS1 # q is summable by ;
then A29: (FS1 # q) ^\ (n + 1) is summable by SERIES_1:12;
seq ^\ (n + 1) is summable by ;
then Sum ((FS1 # q) ^\ (n + 1)) <= Sum (seq ^\ (n + 1)) by ;
hence ( FS1 # q is summable & 0 <= Sum ((FS1 # q) ^\ (n + 1)) & Sum ((FS1 # q) ^\ (n + 1)) < r4 ) by ; :: thesis: verum
end;
A30: fR .: (meet RNG) c= R
proof
let fRq be object ; :: according to TARSKI:def 3 :: thesis: ( not fRq in fR .: (meet RNG) or fRq in R )
assume fRq in fR .: (meet RNG) ; :: thesis: fRq in R
then consider q being object such that
A31: q in dom fR and
A32: q in meet RNG and
A33: fRq = fR . q by FUNCT_1:def 6;
reconsider q = q as Point of T by A31;
set sp = FS1 # p;
set sq = FS1 # q;
set spn = (FS1 # p) ^\ (n + 1);
set sqn = (FS1 # q) ^\ (n + 1);
set absPSpq = Partial_Sums |.((FS1 # p) - (FS1 # q)).|;
for k being Nat st k <= n holds
|.((FS1 # p) - (FS1 # q)).| . k <= r2 / (n + 1)
proof
let k be Nat; :: thesis: ( k <= n implies |.((FS1 # p) - (FS1 # q)).| . k <= r2 / (n + 1) )
assume A34: k <= n ; :: thesis: |.((FS1 # p) - (FS1 # q)).| . k <= r2 / (n + 1)
( k = 0 or k >= 1 ) by NAT_1:14;
then ( k in or k in Seg n ) by ;
then A35: k in \/ (Seg n) by XBOOLE_0:def 3;
then FSn . k in RNG by FUNCT_2:4;
then A36: q in FSn . k by ;
A37: k in NAT by ORDINAL1:def 12;
dom ((FS1 # p) - (FS1 # q)) = NAT by FUNCT_2:def 1;
then A38: ((FS1 # p) - (FS1 # q)) . k = ((FS1 # p) . k) - ((FS1 # q) . k) by ;
consider f1 being RealMap of T such that
A39: FS1 . k = f1 and
f1 is continuous and
for p being Point of T holds f1 . p >= 0 by A1;
reconsider f1p = f1 . p, f1q = f1 . q as Point of RealSpace by METRIC_1:def 13;
ex SS being Subset of T st
( SS = FSn . k & SS is open & p in SS & ( for f1 being RealMap of T st FS1 . k = f1 holds
for f1p being Point of RealSpace st f1p = f1 . p holds
f1 .: SS c= Ball (f1p,(r2 / (n + 1))) ) ) by ;
then A40: f1 .: (FSn . k) c= Ball (f1p,(r2 / (n + 1))) by A39;
dom f1 = the carrier of T by FUNCT_2:def 1;
then f1q in f1 .: (FSn . k) by ;
then dist (f1p,f1q) < r2 / (n + 1) by ;
then A41: |.((f1 . p) - (f1 . q)).| < r2 / (n + 1) by TOPMETR:11;
f1 . p = (FS1 # p) . k by ;
then |.(((FS1 # p) . k) - ((FS1 # q) . k)).| < r2 / (n + 1) by ;
hence |.((FS1 # p) - (FS1 # q)).| . k <= r2 / (n + 1) by ; :: thesis: verum
end;
then A42: (Partial_Sums |.((FS1 # p) - (FS1 # q)).|) . n <= (r2 / (n + 1)) * (n + 1) by Th12;
A43: n in NAT by ORDINAL1:def 12;
set PSp = Partial_Sums (FS1 # p);
set PSq = Partial_Sums (FS1 # q);
set PSpq = Partial_Sums ((FS1 # p) - (FS1 # q));
( (Partial_Sums (FS1 # p)) - (Partial_Sums (FS1 # q)) = Partial_Sums ((FS1 # p) - (FS1 # q)) & dom ((Partial_Sums (FS1 # p)) - (Partial_Sums (FS1 # q))) = NAT ) by ;
then A44: |.(((Partial_Sums (FS1 # p)) . n) - ((Partial_Sums (FS1 # q)) . n)).| = |.((Partial_Sums ((FS1 # p) - (FS1 # q))) . n).| by ;
|.((Partial_Sums ((FS1 # p) - (FS1 # q))) . n).| <= (Partial_Sums |.((FS1 # p) - (FS1 # q)).|) . n by Th13;
then |.(((Partial_Sums (FS1 # p)) . n) - ((Partial_Sums (FS1 # q)) . n)).| <= (r2 / (n + 1)) * (n + 1) by ;
then A45: |.(((Partial_Sums (FS1 # p)) . n) - ((Partial_Sums (FS1 # q)) . n)).| <= r2 by XCMPLX_1:87;
0 <= Sum ((FS1 # p) ^\ (n + 1)) by A25;
then A46: |.(Sum ((FS1 # p) ^\ (n + 1))).| = Sum ((FS1 # p) ^\ (n + 1)) by ABSVALUE:def 1;
0 <= Sum ((FS1 # q) ^\ (n + 1)) by A25;
then A47: |.(Sum ((FS1 # q) ^\ (n + 1))).| = Sum ((FS1 # q) ^\ (n + 1)) by ABSVALUE:def 1;
reconsider fRq = fR . q as Point of RealSpace by ;
A48: |.((Sum ((FS1 # p) ^\ (n + 1))) - (Sum ((FS1 # q) ^\ (n + 1)))).| <= |.(Sum ((FS1 # p) ^\ (n + 1))).| + |.(Sum ((FS1 # q) ^\ (n + 1))).| by COMPLEX1:57;
A49: ( fRp = Sum (FS1 # p) & fRq = Sum (FS1 # q) ) by A3;
( Sum (FS1 # p) = ((Partial_Sums (FS1 # p)) . n) + (Sum ((FS1 # p) ^\ (n + 1))) & Sum (FS1 # q) = ((Partial_Sums (FS1 # q)) . n) + (Sum ((FS1 # q) ^\ (n + 1))) ) by ;
then |.((fR . p) - (fR . q)).| = |.((((Partial_Sums (FS1 # p)) . n) - ((Partial_Sums (FS1 # q)) . n)) + ((Sum ((FS1 # p) ^\ (n + 1))) - (Sum ((FS1 # q) ^\ (n + 1))))).| by A49;
then A50: |.((fR . p) - (fR . q)).| <= |.(((Partial_Sums (FS1 # p)) . n) - ((Partial_Sums (FS1 # q)) . n)).| + |.((Sum ((FS1 # p) ^\ (n + 1))) - (Sum ((FS1 # q) ^\ (n + 1)))).| by COMPLEX1:56;
( Sum ((FS1 # p) ^\ (n + 1)) < r4 & Sum ((FS1 # q) ^\ (n + 1)) < r4 ) by A25;
then |.(Sum ((FS1 # p) ^\ (n + 1))).| + |.(Sum ((FS1 # q) ^\ (n + 1))).| < r4 + r4 by ;
then |.((Sum ((FS1 # p) ^\ (n + 1))) - (Sum ((FS1 # q) ^\ (n + 1)))).| < r2 by ;
then |.(((Partial_Sums (FS1 # p)) . n) - ((Partial_Sums (FS1 # q)) . n)).| + |.((Sum ((FS1 # p) ^\ (n + 1))) - (Sum ((FS1 # q) ^\ (n + 1)))).| < r2 + r2 by ;
then |.((fR . p) - (fR . q)).| < rn by ;
then dist (fRp,fRq) < rn by TOPMETR:11;
then fRq in Ball (fRp,rn) by METRIC_1:11;
hence fRq in R by ; :: thesis: verum
end;
now :: thesis: for Fx being set st Fx in RNG holds
p in Fx
let Fx be set ; :: thesis: ( Fx in RNG implies p in Fx )
assume Fx in RNG ; :: thesis: p in Fx
then consider x being object such that
A51: x in dom FSn and
A52: FSn . x = Fx by FUNCT_1:def 3;
ex SS being Subset of T st
( SS = FSn . x & SS is open & p in SS & ( for f1 being RealMap of T st FS1 . x = f1 holds
for f1p being Point of RealSpace st f1p = f1 . p holds
f1 .: SS c= Ball (f1p,(r2 / (n + 1))) ) ) by ;
hence p in Fx by A52; :: thesis: verum
end;
then p in meet RNG by SETFAM_1:def 1;
hence ex U being Subset of T st
( U is open & p in U & fR .: U c= R ) by ; :: thesis: verum
end;
hence fR is_continuous_at p by TMAP_1:43; :: thesis: verum
end;
then fR is continuous by TMAP_1:50;
hence f is continuous by JORDAN5A:27; :: thesis: verum