let T be non empty TopSpace; :: thesis: for FS1 being Functional_Sequence of the carrier of T,REAL st ( for n being Element of 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 Element of 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 Element of 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 Element of 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 Element of 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 Element of 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:24;

now

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

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 A4: ( 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 )
reconsider fRp = fR . p as Point of RealSpace by METRIC_1:def 14;
consider rn being real number such that
A5: ( rn > 0 & Ball fRp,rn c= R ) by A4, TOPMETR:22, TOPMETR:def 7;
set r2 = rn / 2;
set r4 = rn / 4;
reconsider r2 = rn / 2, r4 = rn / 4 as Real ;
consider seq being Real_Sequence such that
A6: ( seq is summable & ( for n being Element of NAT
for q being Point of T holds (FS1 # q) . n <= seq . n ) ) by A2;
( Partial_Sums seq is convergent & r4 > 0 ) by A5, A6, SERIES_1:def 2, XREAL_1:226;
then consider n being Element of NAT such that
A7: for m being Element of NAT st n <= m holds
abs (((Partial_Sums seq) . m) - (lim (Partial_Sums seq))) < r4 by SEQ_2:def 7;
A8: for k being Element of NAT
for q being Point of T holds (FS1 # q) . k >= 0

proof

let k be Element of NAT ; :: thesis: for q being Point of T holds (FS1 # q) . k >= 0
let q be Point of T; :: thesis: (FS1 # q) . k >= 0
consider f1 being RealMap of T such that
A9: ( FS1 . k = f1 & f1 is continuous & ( for q being Point of T holds f1 . q >= 0 ) ) by A1;
(FS1 . k) . q = (FS1 # q) . k by SEQFUNC:def 11;
hence (FS1 # q) . k >= 0 by A9; :: thesis: verum

end;

A10: for k being Element of NAT holds (seq ^\ (n + 1)) . k >= 0

proof

let k be Element of NAT ; :: thesis: (seq ^\ (n + 1)) . k >= 0
for q being Point of T holds
( 0 <= (FS1 # p) . ((n + 1) + k) & (FS1 # q) . ((n + 1) + k) <= seq . ((n + 1) + k) & seq . ((n + 1) + k) = (seq ^\ (n + 1)) . k ) by A6, A8, NAT_1:def 3;
hence (seq ^\ (n + 1)) . k >= 0 ; :: thesis: verum

end;

( abs (((Partial_Sums seq) . n) - (lim (Partial_Sums seq))) < r4 & lim (Partial_Sums seq) = Sum seq & Sum seq = ((Partial_Sums seq) . n) + (Sum (seq ^\ (n + 1))) ) by A6, A7, SERIES_1:18, SERIES_1:def 3;
then ( abs (- (Sum (seq ^\ (n + 1)))) < r4 & seq ^\ (n + 1) is summable ) by A6, SERIES_1:15;
then ( abs (Sum (seq ^\ (n + 1))) < r4 & Sum (seq ^\ (n + 1)) >= 0 ) by A10, COMPLEX1:138, SERIES_1:21;
then A11: Sum (seq ^\ (n + 1)) < r4 by ABSVALUE:def 1;
A12: 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;
A13: for k being Element of NAT holds
( 0 <= (FS1 # q) . k & (FS1 # q) . k <= seq . k ) by A6, A8;
then A14: FS1 # q is summable by A6, SERIES_1:24;
( (FS1 # q) ^\ (n + 1) is summable & seq ^\ (n + 1) is summable & ( for k being Element of NAT holds
( 0 <= ((FS1 # q) ^\ (n + 1)) . k & ((FS1 # q) ^\ (n + 1)) . k <= (seq ^\ (n + 1)) . k ) ) )

proof

now

let k be Element of NAT ; :: thesis: ( 0 <= ((FS1 # q) ^\ (n + 1)) . k & ((FS1 # q) ^\ (n + 1)) . k <= (seq ^\ (n + 1)) . k )
( 0 <= (FS1 # q) . ((n + 1) + k) & (FS1 # q) . ((n + 1) + k) <= seq . ((n + 1) + k) & seq . ((n + 1) + k) = (seq ^\ (n + 1)) . k & (FS1 # q) . ((n + 1) + k) = ((FS1 # q) ^\ (n + 1)) . k ) by A6, A8, NAT_1:def 3;
hence ( 0 <= ((FS1 # q) ^\ (n + 1)) . k & ((FS1 # q) ^\ (n + 1)) . k <= (seq ^\ (n + 1)) . k ) ; :: thesis: verum

end;

hence ( (FS1 # q) ^\ (n + 1) is summable & seq ^\ (n + 1) is summable & ( for k being Element of NAT holds
( 0 <= ((FS1 # q) ^\ (n + 1)) . k & ((FS1 # q) ^\ (n + 1)) . k <= (seq ^\ (n + 1)) . k ) ) ) by A6, A14, SERIES_1:15; :: thesis: verum

end;

then ( 0 <= Sum ((FS1 # q) ^\ (n + 1)) & Sum ((FS1 # q) ^\ (n + 1)) <= Sum (seq ^\ (n + 1)) ) by SERIES_1:21, SERIES_1:24;
hence ( FS1 # q is summable & 0 <= Sum ((FS1 # q) ^\ (n + 1)) & Sum ((FS1 # q) ^\ (n + 1)) < r4 ) by A6, A11, A13, SERIES_1:24, XXREAL_0:2; :: thesis: verum

end;

defpred S₁[ set , set ] 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)) ) );
A15: for k being set st k in {0 } \/ (Seg n) holds
ex U being set st
( U in bool the carrier of T & S₁[k,U] )

proof

let k be set ; :: thesis: ( k in {0 } \/ (Seg n) implies ex U being set st
( U in bool the carrier of T & S₁[k,U] ) )
assume k in {0 } \/ (Seg n) ; :: thesis: ex U being set 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
A16: ( FS1 . k = f1 & f1 is continuous & ( for p being Point of T holds f1 . p >= 0 ) ) by A1;
reconsider f1' = f1 as Function of T,R^1 by TOPMETR:24;
reconsider f1p = f1' . p as Point of RealSpace by METRIC_1:def 14;
set B = Ball f1p,(r2 / (n + 1));
reconsider B = Ball f1p,(r2 / (n + 1)) as Subset of R^1 by METRIC_1:def 14, TOPMETR:24;
( dist f1p,f1p = 0 & r2 > 0 & n + 1 <> 0 & n + 1 >= 0 ) by A5, METRIC_1:1, XREAL_1:217;
then ( dist f1p,f1p < r2 / (n + 1) & f1' is continuous ) by A16, TOPREAL6:83, XREAL_1:141;
then ( f1p in B & B is open & f1' is_continuous_at p ) by METRIC_1:12, TMAP_1:55, TOPMETR:21, TOPMETR:def 7;
then consider U being Subset of T such that
A17: ( U is open & p in U & f1' .: U c= B ) by TMAP_1:48;
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 A16, A17;
hence ex U being set st
( U in bool the carrier of T & S₁[k,U] ) by A17; :: thesis: verum

end;

consider FSn being Function of ({0 } \/ (Seg n)),(bool the carrier of T) such that
A18: for k being set st k in {0 } \/ (Seg n) holds
S₁[k,FSn . k] from FUNCT_2:sch 1(A15);
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 set such that
A20: ( x in dom FSn & FSn . x = Q ) by FUNCT_1:def 5;
consider SS being Subset of T such that
A21: ( 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 A18, A20;
thus Q is open by A20, 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:6;
A22: p in meet RNG

proof

now

let Fx be set ; :: thesis: ( Fx in RNG implies p in Fx )
assume Fx in RNG ; :: thesis: p in Fx
then consider x being set such that
A23: ( x in dom FSn & FSn . x = Fx ) by FUNCT_1:def 5;
consider SS being Subset of T such that
A24: ( 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 A18, A23;
thus p in Fx by A23, A24; :: thesis: verum

end;

hence p in meet RNG by SETFAM_1:def 1; :: thesis: verum

end;

fR .: (meet RNG) c= R

proof

let fRq be set ; :: 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 set such that
A25: ( q in dom fR & q in meet RNG & fRq = fR . q ) by FUNCT_1:def 12;
reconsider q = q as Point of T by A25;
reconsider fRq = fR . q as Point of RealSpace by METRIC_1:def 14;
set sp = FS1 # p;
set sq = FS1 # q;
set spn = (FS1 # p) ^\ (n + 1);
set sqn = (FS1 # q) ^\ (n + 1);
set PSp = Partial_Sums (FS1 # p);
set PSq = Partial_Sums (FS1 # q);
set PSpq = Partial_Sums ((FS1 # p) - (FS1 # q));
set absPSpq = Partial_Sums (abs ((FS1 # p) - (FS1 # q)));
( 0 <= Sum ((FS1 # p) ^\ (n + 1)) & 0 <= Sum ((FS1 # q) ^\ (n + 1)) ) by A12;
then ( abs (Sum ((FS1 # p) ^\ (n + 1))) = Sum ((FS1 # p) ^\ (n + 1)) & abs (Sum ((FS1 # q) ^\ (n + 1))) = Sum ((FS1 # q) ^\ (n + 1)) & Sum ((FS1 # p) ^\ (n + 1)) < r4 & Sum ((FS1 # q) ^\ (n + 1)) < r4 ) by A12, ABSVALUE:def 1;
then A26: (abs (Sum ((FS1 # p) ^\ (n + 1)))) + (abs (Sum ((FS1 # q) ^\ (n + 1)))) < r4 + r4 by XREAL_1:10;
A27: for k being Element of NAT st k <= n holds
(abs ((FS1 # p) - (FS1 # q))) . k <= r2 / (n + 1)

proof

let k be Element of NAT ; :: thesis: ( k <= n implies (abs ((FS1 # p) - (FS1 # q))) . k <= r2 / (n + 1) )
assume A28: k <= n ; :: thesis: (abs ((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 A28, FINSEQ_1:3, TARSKI:def 1;
then A29: k in {0 } \/ (Seg n) by XBOOLE_0:def 3;
consider f1 being RealMap of T such that
A30: ( FS1 . k = f1 & f1 is continuous & ( 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 14;
( FSn . k in RNG & q in meet RNG ) by A25, A29, FUNCT_2:6;
then ( q in FSn . k & dom f1 = the carrier of T ) by FUNCT_2:def 1, SETFAM_1:def 1;
then A31: f1q in f1 .: (FSn . k) by FUNCT_1:def 12;
consider SS being Subset of T such that
A32: ( 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 A18, A29;
f1 .: (FSn . k) c= Ball f1p,(r2 / (n + 1)) by A30, A32;
then dist f1p,f1q < r2 / (n + 1) by A31, METRIC_1:12;
then ( abs ((f1 . p) - (f1 . q)) < r2 / (n + 1) & f1 . p = (FS1 # p) . k & f1 . q = (FS1 # q) . k & dom ((FS1 # p) - (FS1 # q)) = NAT ) by A30, FUNCT_2:def 1, SEQFUNC:def 11, TOPMETR:15;
then ( abs (((FS1 # p) . k) - ((FS1 # q) . k)) < r2 / (n + 1) & ((FS1 # p) - (FS1 # q)) . k = ((FS1 # p) . k) - ((FS1 # q) . k) ) by VALUED_1:13;
hence (abs ((FS1 # p) - (FS1 # q))) . k <= r2 / (n + 1) by SEQ_1:16; :: thesis: verum

end;

( (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:3, SERIES_1:9;
then ( abs (((Partial_Sums (FS1 # p)) . n) - ((Partial_Sums (FS1 # q)) . n)) = abs ((Partial_Sums ((FS1 # p) - (FS1 # q))) . n) & abs ((Partial_Sums ((FS1 # p) - (FS1 # q))) . n) <= (Partial_Sums (abs ((FS1 # p) - (FS1 # q)))) . n & (Partial_Sums (abs ((FS1 # p) - (FS1 # q)))) . n <= (r2 / (n + 1)) * (n + 1) ) by A27, Th12, Th13, VALUED_1:13;
then abs (((Partial_Sums (FS1 # p)) . n) - ((Partial_Sums (FS1 # q)) . n)) <= (r2 / (n + 1)) * (n + 1) by XXREAL_0:2;
then A33: abs (((Partial_Sums (FS1 # p)) . n) - ((Partial_Sums (FS1 # q)) . n)) <= r2 by XCMPLX_1:88;
( FS1 # p is summable & FS1 # q is summable ) by A12;
then ( 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))) & fRp = Sum (FS1 # p) & fRq = Sum (FS1 # q) ) by A3, SERIES_1:18;
then abs ((fR . p) - (fR . q)) = abs ((((Partial_Sums (FS1 # p)) . n) - ((Partial_Sums (FS1 # q)) . n)) + ((Sum ((FS1 # p) ^\ (n + 1))) - (Sum ((FS1 # q) ^\ (n + 1))))) ;
then A34: ( abs ((fR . p) - (fR . q)) <= (abs (((Partial_Sums (FS1 # p)) . n) - ((Partial_Sums (FS1 # q)) . n))) + (abs ((Sum ((FS1 # p) ^\ (n + 1))) - (Sum ((FS1 # q) ^\ (n + 1))))) & abs ((Sum ((FS1 # p) ^\ (n + 1))) - (Sum ((FS1 # q) ^\ (n + 1)))) <= (abs (Sum ((FS1 # p) ^\ (n + 1)))) + (abs (Sum ((FS1 # q) ^\ (n + 1)))) ) by COMPLEX1:142, COMPLEX1:143;
then abs ((Sum ((FS1 # p) ^\ (n + 1))) - (Sum ((FS1 # q) ^\ (n + 1)))) < r2 by A26, XXREAL_0:2;
then (abs (((Partial_Sums (FS1 # p)) . n) - ((Partial_Sums (FS1 # q)) . n))) + (abs ((Sum ((FS1 # p) ^\ (n + 1))) - (Sum ((FS1 # q) ^\ (n + 1))))) < r2 + r2 by A33, XREAL_1:10;
then abs ((fR . p) - (fR . q)) < rn by A34, XXREAL_0:2;
then dist fRp,fRq < rn by TOPMETR:15;
then fRq in Ball fRp,rn by METRIC_1:12;
hence fRq in R by A5, A25; :: thesis: verum

end;

hence ex U being Subset of T st
( U is open & p in U & fR .: U c= R ) by A19, A22, TOPS_2:27; :: thesis: verum

end;

hence fR is_continuous_at p by TMAP_1:48; :: thesis: verum

end;

then fR is continuous by TMAP_1:55;
hence f is continuous by TOPREAL6:83; :: thesis: verum