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: fR is_continuous_at p
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 METRIC_1:def 13, XREAL_0:def 1;
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 TOPMETR:15, TOPMETR:def 6;
set r2 = rn / 2;
set r4 = rn / 4;
reconsider r2 = rn / 2, r4 = rn / 4 as Real ;
A6: r4 > 0 by A4, XREAL_1:224;
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 A7, SERIES_1:def 2;
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 A6, SEQ_2:def 7;
defpred S₁[ 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 {0} \/ (Seg n) holds
ex U being object st
( U in bool the carrier of T & S₁[k,U] )

proof

let k be object ; :: thesis: ( k in {0} \/ (Seg n) implies ex U being object st
( U in bool the carrier of T & S₁[k,U] ) )
assume k in {0} \/ (Seg n) ; :: thesis: ex U being object st
( U in bool the carrier of T & S₁[k,U] )
then ( k in Seg n or k in {0} ) 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 METRIC_1:def 13, XREAL_0:def 1;
set B = Ball (f1p,(r2 / (n + 1)));
reconsider B = Ball (f1p,(r2 / (n + 1))) as Subset of R^1 by METRIC_1:def 13, TOPMETR:17;
( dist (f1p,f1p) = 0 & r2 > 0 ) by A4, METRIC_1:1, XREAL_1:215;
then dist (f1p,f1p) < r2 / (n + 1) by XREAL_1:139;
then A13: f1p in B by METRIC_1:11;
f19 is continuous by A12, JORDAN5A:27;
then ( B is open & f19 is_continuous_at p ) by TMAP_1:50, TOPMETR:14, TOPMETR:def 6;
then consider U being Subset of T such that
A14: ( U is open & p in U ) and
A15: f19 .: U c= B by A13, TMAP_1:43;
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 A11, A15;
hence ex U being object st
( U in bool the carrier of T & S₁[k,U] ) by A14; :: thesis: verum

end;

consider FSn being Function of ({0} \/ (Seg n)),(bool the carrier of T) such that
A16: for k being object st k in {0} \/ (Seg n) holds
S₁[k,FSn . k] from FUNCT_2:sch 1(A10);
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 A1, SEQFUNC:def 10;
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 A17, NAT_1:def 3;
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 A16, A20;
hence Q is open by A21; :: thesis: verum

end;

0 in {0} by TARSKI:def 1;
then 0 in {0} \/ (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 A7, SERIES_1:15, SERIES_1:def 3;
|.(((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 A7, SERIES_1:12;
then Sum (seq ^\ (n + 1)) >= 0 by A18, SERIES_1:18;
then A24: Sum (seq ^\ (n + 1)) < r4 by A23, ABSVALUE:def 1;
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 A8, A17;
hence ( 0 <= ((FS1 # q) ^\ (n + 1)) . k & ((FS1 # q) ^\ (n + 1)) . k <= (seq ^\ (n + 1)) . k ) by A27, NAT_1:def 3; :: thesis: verum

end;

A28: for k being Nat holds
( 0 <= (FS1 # q) . k & (FS1 # q) . k <= seq . k ) by A8, A17;
then FS1 # q is summable by A7, SERIES_1:20;
then A29: (FS1 # q) ^\ (n + 1) is summable by SERIES_1:12;
seq ^\ (n + 1) is summable by A7, SERIES_1:12;
then Sum ((FS1 # q) ^\ (n + 1)) <= Sum (seq ^\ (n + 1)) by A26, SERIES_1:20;
hence ( FS1 # q is summable & 0 <= Sum ((FS1 # q) ^\ (n + 1)) & Sum ((FS1 # q) ^\ (n + 1)) < r4 ) by A7, A24, A28, A26, A29, SERIES_1:18, SERIES_1:20, XXREAL_0:2; :: 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 {0} or k in Seg n ) by A34, FINSEQ_1:1, TARSKI:def 1;
then A35: k in {0} \/ (Seg n) by XBOOLE_0:def 3;
then FSn . k in RNG by FUNCT_2:4;
then A36: q in FSn . k by A32, SETFAM_1:def 1;
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 VALUED_1:13, A37;
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 A16, A35;
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 A36, FUNCT_1:def 6;
then dist (f1p,f1q) < r2 / (n + 1) by A40, METRIC_1:11;
then A41: |.((f1 . p) - (f1 . q)).| < r2 / (n + 1) by TOPMETR:11;
f1 . p = (FS1 # p) . k by A39, SEQFUNC:def 10;
then |.(((FS1 # p) . k) - ((FS1 # q) . k)).| < r2 / (n + 1) by A39, A41, SEQFUNC:def 10;
hence |.((FS1 # p) - (FS1 # q)).| . k <= r2 / (n + 1) by A38, SEQ_1:12; :: 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 SEQ_1:1, SERIES_1:6;
then A44: |.(((Partial_Sums (FS1 # p)) . n) - ((Partial_Sums (FS1 # q)) . n)).| = |.((Partial_Sums ((FS1 # p) - (FS1 # q))) . n).| by VALUED_1:13, A43;
|.((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 A44, A42, XXREAL_0:2;
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 METRIC_1:def 13, XREAL_0:def 1;
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 A25, SERIES_1:15;
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 A46, A47, XREAL_1:8;
then |.((Sum ((FS1 # p) ^\ (n + 1))) - (Sum ((FS1 # q) ^\ (n + 1)))).| < r2 by A48, XXREAL_0:2;
then |.(((Partial_Sums (FS1 # p)) . n) - ((Partial_Sums (FS1 # q)) . n)).| + |.((Sum ((FS1 # p) ^\ (n + 1))) - (Sum ((FS1 # q) ^\ (n + 1)))).| < r2 + r2 by A45, XREAL_1:8;
then |.((fR . p) - (fR . q)).| < rn by A50, XXREAL_0:2;
then dist (fRp,fRq) < rn by TOPMETR:11;
then fRq in Ball (fRp,rn) by METRIC_1:11;
hence fRq in R by A5, A33; :: 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 A16, A51;
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 A19, A30, TOPS_2:20; :: 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