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;

hence f is continuous by JORDAN5A:27; :: thesis: verum

( 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

then
fR is continuous
by TMAP_1:50;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 )

end;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

hence
fR is_continuous_at p
by TMAP_1:43; :: thesis: verum
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_{1}[ 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_{1}[k,U] )

A16: for k being object st k in {0} \/ (Seg n) holds

S_{1}[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

A19: RNG is open

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 )

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;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

( 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

proof

consider FSn being Function of ({0} \/ (Seg n)),(bool the carrier of T) such that
let k be object ; :: thesis: ( k in {0} \/ (Seg n) implies ex U being object st

( U in bool the carrier of T & S_{1}[k,U] ) )

assume k in {0} \/ (Seg n) ; :: thesis: ex U being object st

( U in bool the carrier of T & S_{1}[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_{1}[k,U] )
by A14; :: thesis: verum

end;( U in bool the carrier of T & S

assume k in {0} \/ (Seg n) ; :: thesis: ex U being object st

( U in bool the carrier of T & S

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

A16: for k being object st k in {0} \/ (Seg n) holds

S

A17: for k being Nat

for q being Point of T holds (FS1 # q) . k >= 0

proof

A18:
for k being Nat holds (seq ^\ (n + 1)) . k >= 0
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;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

proof

reconsider RNG = rng FSn as Subset-Family of T ;
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;( 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

A19: RNG is open

proof

0 in {0}
by TARSKI:def 1;
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;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

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

A30:
fR .: (meet RNG) c= R
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;

( 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;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 )

A28:
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;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

( 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

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)

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;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

then A42:
(Partial_Sums |.((FS1 # p) - (FS1 # q)).|) . n <= (r2 / (n + 1)) * (n + 1)
by Th12;
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;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

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

now :: thesis: for Fx being set st Fx in RNG holds

p in Fx

then
p in meet RNG
by SETFAM_1:def 1;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;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

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

hence f is continuous by JORDAN5A:27; :: thesis: verum