:: HEINE semantic presentation begin theorem Th1: :: HEINE:1 for x, y being real number for A being SubSpace of RealSpace for p, q being Point of A st x = p & y = q holds dist (p,q) = abs (x - y) proof let x, y be real number ; ::_thesis: for A being SubSpace of RealSpace for p, q being Point of A st x = p & y = q holds dist (p,q) = abs (x - y) let A be SubSpace of RealSpace ; ::_thesis: for p, q being Point of A st x = p & y = q holds dist (p,q) = abs (x - y) let p, q be Point of A; ::_thesis: ( x = p & y = q implies dist (p,q) = abs (x - y) ) assume A1: ( x = p & y = q ) ; ::_thesis: dist (p,q) = abs (x - y) A2: ( x is Real & y is Real ) by XREAL_0:def_1; thus dist (p,q) = the distance of A . (p,q) by METRIC_1:def_1 .= real_dist . (x,y) by A1, METRIC_1:def_13, TOPMETR:def_1 .= abs (x - y) by A2, METRIC_1:def_12 ; ::_thesis: verum end; theorem Th2: :: HEINE:2 for n being Element of NAT for seq being Real_Sequence st seq is V40() & rng seq c= NAT holds n <= seq . n proof let n be Element of NAT ; ::_thesis: for seq being Real_Sequence st seq is V40() & rng seq c= NAT holds n <= seq . n let seq be Real_Sequence; ::_thesis: ( seq is V40() & rng seq c= NAT implies n <= seq . n ) defpred S1[ Element of NAT ] means $1 <= seq . $1; assume that A1: seq is V40() and A2: rng seq c= NAT ; ::_thesis: n <= seq . n A3: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A4: k <= seq . k ; ::_thesis: S1[k + 1] k + 1 in NAT ; then k + 1 in dom seq by FUNCT_2:def_1; then seq . (k + 1) in rng seq by FUNCT_1:def_3; then reconsider k9 = seq . (k + 1) as Element of NAT by A2; seq . k < seq . (k + 1) by A1, SEQM_3:def_6; then k < k9 by A4, XXREAL_0:2; hence S1[k + 1] by NAT_1:13; ::_thesis: verum end; 0 in NAT ; then 0 in dom seq by FUNCT_2:def_1; then seq . 0 in rng seq by FUNCT_1:def_3; then A5: S1[ 0 ] by A2, NAT_1:2; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A5, A3); hence n <= seq . n ; ::_thesis: verum end; definition let seq be Real_Sequence; let k be Element of NAT ; funck to_power seq -> Real_Sequence means :Def1: :: HEINE:def 1 for n being Element of NAT holds it . n = k to_power (seq . n); existence ex b1 being Real_Sequence st for n being Element of NAT holds b1 . n = k to_power (seq . n) proof deffunc H1( Element of NAT ) -> Element of REAL = k to_power (seq . $1); thus ex s being Real_Sequence st for n being Element of NAT holds s . n = H1(n) from SEQ_1:sch_1(); ::_thesis: verum end; uniqueness for b1, b2 being Real_Sequence st ( for n being Element of NAT holds b1 . n = k to_power (seq . n) ) & ( for n being Element of NAT holds b2 . n = k to_power (seq . n) ) holds b1 = b2 proof let s1, s2 be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s1 . n = k to_power (seq . n) ) & ( for n being Element of NAT holds s2 . n = k to_power (seq . n) ) implies s1 = s2 ) assume that A1: for n being Element of NAT holds s1 . n = k to_power (seq . n) and A2: for n being Element of NAT holds s2 . n = k to_power (seq . n) ; ::_thesis: s1 = s2 let n be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: K77(s1,n) = K77(s2,n) thus s1 . n = k to_power (seq . n) by A1 .= s2 . n by A2 ; ::_thesis: verum end; end; :: deftheorem Def1 defines to_power HEINE:def_1_:_ for seq being Real_Sequence for k being Element of NAT for b3 being Real_Sequence holds ( b3 = k to_power seq iff for n being Element of NAT holds b3 . n = k to_power (seq . n) ); theorem Th3: :: HEINE:3 for seq being Real_Sequence st seq is divergent_to+infty holds 2 to_power seq is divergent_to+infty proof let seq be Real_Sequence; ::_thesis: ( seq is divergent_to+infty implies 2 to_power seq is divergent_to+infty ) assume A1: seq is divergent_to+infty ; ::_thesis: 2 to_power seq is divergent_to+infty let r be Real; :: according to LIMFUNC1:def_4 ::_thesis: ex b1 being Element of NAT st for b2 being Element of NAT holds ( not b1 <= b2 or not (2 to_power seq) . b2 <= r ) consider p being Element of NAT such that A2: p > r by SEQ_4:3; consider n being Element of NAT such that A3: for m being Element of NAT st n <= m holds p < seq . m by A1, LIMFUNC1:def_4; take n ; ::_thesis: for b1 being Element of NAT holds ( not n <= b1 or not (2 to_power seq) . b1 <= r ) let m be Element of NAT ; ::_thesis: ( not n <= m or not (2 to_power seq) . m <= r ) assume m >= n ; ::_thesis: not (2 to_power seq) . m <= r then p < seq . m by A3; then A4: 2 to_power p < 2 to_power (seq . m) by POWER:39; 2 to_power p = 2 |^ p by POWER:41; then p < 2 to_power (seq . m) by A4, NEWTON:86, XXREAL_0:2; then r < 2 to_power (seq . m) by A2, XXREAL_0:2; hence not (2 to_power seq) . m <= r by Def1; ::_thesis: verum end; theorem :: HEINE:4 for a, b being real number st a <= b holds Closed-Interval-TSpace (a,b) is compact proof let a, b be real number ; ::_thesis: ( a <= b implies Closed-Interval-TSpace (a,b) is compact ) set M = Closed-Interval-MSpace (a,b); assume A1: a <= b ; ::_thesis: Closed-Interval-TSpace (a,b) is compact reconsider a = a, b = b as Real by XREAL_0:def_1; set r = b - a; now__::_thesis:_Closed-Interval-TSpace_(a,b)_is_compact percases ( b - a = 0 or b - a > 0 ) by A1, XREAL_1:48; suppose b - a = 0 ; ::_thesis: Closed-Interval-TSpace (a,b) is compact then ( [.a,b.] = {a} & the carrier of (Closed-Interval-TSpace (a,b)) = [.a,b.] ) by TOPMETR:18, XXREAL_1:17; hence Closed-Interval-TSpace (a,b) is compact by COMPTS_1:18; ::_thesis: verum end; supposeA2: b - a > 0 ; ::_thesis: Closed-Interval-TSpace (a,b) is compact A3: TopSpaceMetr (Closed-Interval-MSpace (a,b)) = Closed-Interval-TSpace (a,b) by TOPMETR:def_7; assume not Closed-Interval-TSpace (a,b) is compact ; ::_thesis: contradiction then not Closed-Interval-MSpace (a,b) is compact by A3, TOPMETR:def_5; then consider F being Subset-Family of (Closed-Interval-MSpace (a,b)) such that A4: F is being_ball-family and A5: F is Cover of (Closed-Interval-MSpace (a,b)) and A6: for G being Subset-Family of (Closed-Interval-MSpace (a,b)) holds ( not G c= F or not G is Cover of (Closed-Interval-MSpace (a,b)) or not G is finite ) by TOPMETR:16; defpred S1[ Element of NAT , Element of REAL , Element of REAL ] means ( ( ( for G being Subset-Family of (Closed-Interval-MSpace (a,b)) holds ( not G c= F or not [.($2 - ((b - a) / (2 |^ ($1 + 1)))),$2.] c= union G or not G is finite ) ) implies $3 = $2 - ((b - a) / (2 |^ ($1 + 2))) ) & ( ex G being Subset-Family of (Closed-Interval-MSpace (a,b)) st ( G c= F & [.($2 - ((b - a) / (2 |^ ($1 + 1)))),$2.] c= union G & G is finite ) implies $3 = $2 + ((b - a) / (2 |^ ($1 + 2))) ) ); A7: for n being Element of NAT for p being Real ex w being Real st S1[n,p,w] proof let n be Element of NAT ; ::_thesis: for p being Real ex w being Real st S1[n,p,w] let p be Real; ::_thesis: ex w being Real st S1[n,p,w] now__::_thesis:_ex_y_being_Element_of_REAL_st_S1[n,p,y] percases ( for G being Subset-Family of (Closed-Interval-MSpace (a,b)) holds ( not G c= F or not [.(p - ((b - a) / (2 |^ (n + 1)))),p.] c= union G or not G is finite ) or ex G being Subset-Family of (Closed-Interval-MSpace (a,b)) st ( G c= F & [.(p - ((b - a) / (2 |^ (n + 1)))),p.] c= union G & G is finite ) ) ; supposeA8: for G being Subset-Family of (Closed-Interval-MSpace (a,b)) holds ( not G c= F or not [.(p - ((b - a) / (2 |^ (n + 1)))),p.] c= union G or not G is finite ) ; ::_thesis: ex y being Element of REAL st S1[n,p,y] take y = p - ((b - a) / (2 |^ (n + 2))); ::_thesis: S1[n,p,y] thus S1[n,p,y] by A8; ::_thesis: verum end; supposeA9: ex G being Subset-Family of (Closed-Interval-MSpace (a,b)) st ( G c= F & [.(p - ((b - a) / (2 |^ (n + 1)))),p.] c= union G & G is finite ) ; ::_thesis: ex y being Element of REAL st S1[n,p,y] take y = p + ((b - a) / (2 |^ (n + 2))); ::_thesis: S1[n,p,y] thus S1[n,p,y] by A9; ::_thesis: verum end; end; end; hence ex w being Real st S1[n,p,w] ; ::_thesis: verum end; consider f being Function of NAT,REAL such that A10: f . 0 = (a + b) / 2 and A11: for n being Element of NAT holds S1[n,f . n,f . (n + 1)] from RECDEF_1:sch_2(A7); defpred S2[ Element of NAT ] means for G being Subset-Family of (Closed-Interval-MSpace (a,b)) holds ( not G c= F or not [.((f . $1) - ((b - a) / (2 |^ ($1 + 1)))),((f . $1) + ((b - a) / (2 |^ ($1 + 1)))).] c= union G or not G is finite ); A12: (f . 0) + ((b - a) / (2 |^ (0 + 1))) = ((a + b) / 2) + ((b - a) / 2) by A10, NEWTON:5 .= b ; defpred S3[ Element of NAT ] means ( a <= (f . $1) - ((b - a) / (2 |^ ($1 + 1))) & (f . $1) + ((b - a) / (2 |^ ($1 + 1))) <= b ); A13: for n being Element of NAT holds ( f . (n + 1) = (f . n) + ((b - a) / (2 |^ (n + 2))) or f . (n + 1) = (f . n) - ((b - a) / (2 |^ (n + 2))) ) proof let n be Element of NAT ; ::_thesis: ( f . (n + 1) = (f . n) + ((b - a) / (2 |^ (n + 2))) or f . (n + 1) = (f . n) - ((b - a) / (2 |^ (n + 2))) ) S1[n,f . n,f . (n + 1)] by A11; hence ( f . (n + 1) = (f . n) + ((b - a) / (2 |^ (n + 2))) or f . (n + 1) = (f . n) - ((b - a) / (2 |^ (n + 2))) ) ; ::_thesis: verum end; A14: for k being Element of NAT st S3[k] holds S3[k + 1] proof let k be Element of NAT ; ::_thesis: ( S3[k] implies S3[k + 1] ) A15: ((b - a) / (2 * (2 |^ (k + 1)))) + ((b - a) / (2 * (2 |^ (k + 1)))) = (b - a) / (2 |^ (k + 1)) by XCMPLX_1:118; A16: ((b - a) / (2 |^ (k + 1))) - ((b - a) / (2 |^ (k + (1 + 1)))) = ((b - a) / (2 |^ (k + 1))) - ((b - a) / (2 |^ ((k + 1) + 1))) .= ((b - a) / (2 |^ (k + 1))) - ((b - a) / (2 * (2 |^ (k + 1)))) by NEWTON:6 .= (b - a) / (2 |^ ((k + 1) + 1)) by A15, NEWTON:6 .= (b - a) / (2 |^ (k + (1 + 1))) ; assume A17: S3[k] ; ::_thesis: S3[k + 1] then A18: b - (f . k) >= (b - a) / (2 |^ (k + 1)) by XREAL_1:19; A19: (f . k) - a >= (b - a) / (2 |^ (k + 1)) by A17, XREAL_1:11; now__::_thesis:_(_a_<=_(f_._(k_+_1))_-_((b_-_a)_/_(2_|^_((k_+_1)_+_1)))_&_(f_._(k_+_1))_+_((b_-_a)_/_(2_|^_((k_+_1)_+_1)))_<=_b_) percases ( f . (k + 1) = (f . k) + ((b - a) / (2 |^ (k + 2))) or f . (k + 1) = (f . k) - ((b - a) / (2 |^ (k + 2))) ) by A13; supposeA20: f . (k + 1) = (f . k) + ((b - a) / (2 |^ (k + 2))) ; ::_thesis: ( a <= (f . (k + 1)) - ((b - a) / (2 |^ ((k + 1) + 1))) & (f . (k + 1)) + ((b - a) / (2 |^ ((k + 1) + 1))) <= b ) ( 2 |^ (k + 1) > 0 & b - a >= 0 ) by A1, NEWTON:83, XREAL_1:48; then A21: (b - a) / (2 |^ (k + 1)) >= 0 ; (f . (k + 1)) - a = ((f . k) - a) + ((b - a) / (2 |^ (k + 2))) by A20; then (f . (k + 1)) - a >= (b - a) / (2 |^ (k + 2)) by A19, A21, XREAL_1:31; hence a <= (f . (k + 1)) - ((b - a) / (2 |^ ((k + 1) + 1))) by XREAL_1:11; ::_thesis: (f . (k + 1)) + ((b - a) / (2 |^ ((k + 1) + 1))) <= b b - (f . (k + 1)) = (b - (f . k)) - ((b - a) / (2 |^ (k + 2))) by A20; then b - (f . (k + 1)) >= (b - a) / (2 |^ (k + 2)) by A18, A16, XREAL_1:9; hence (f . (k + 1)) + ((b - a) / (2 |^ ((k + 1) + 1))) <= b by XREAL_1:19; ::_thesis: verum end; supposeA22: f . (k + 1) = (f . k) - ((b - a) / (2 |^ (k + 2))) ; ::_thesis: ( a <= (f . (k + 1)) - ((b - a) / (2 |^ ((k + 1) + 1))) & (f . (k + 1)) + ((b - a) / (2 |^ ((k + 1) + 1))) <= b ) then (f . (k + 1)) - a = ((f . k) - a) - ((b - a) / (2 |^ (k + 2))) ; then (f . (k + 1)) - a >= (b - a) / (2 |^ (k + 2)) by A19, A16, XREAL_1:9; hence a <= (f . (k + 1)) - ((b - a) / (2 |^ ((k + 1) + 1))) by XREAL_1:11; ::_thesis: (f . (k + 1)) + ((b - a) / (2 |^ ((k + 1) + 1))) <= b ( 2 |^ (k + 1) > 0 & b - a >= 0 ) by A1, NEWTON:83, XREAL_1:48; then A23: (b - a) / (2 |^ (k + 1)) >= 0 ; b - (f . (k + 1)) = (b - (f . k)) + ((b - a) / (2 |^ (k + 2))) by A22; then b - (f . (k + 1)) >= (b - a) / (2 |^ (k + 2)) by A18, A23, XREAL_1:31; hence (f . (k + 1)) + ((b - a) / (2 |^ ((k + 1) + 1))) <= b by XREAL_1:19; ::_thesis: verum end; end; end; hence S3[k + 1] ; ::_thesis: verum end; A24: (f . 0) - ((b - a) / (2 |^ (0 + 1))) = ((a + b) / 2) - ((b - a) / 2) by A10, NEWTON:5 .= a ; then A25: S3[ 0 ] by A12; A26: for k being Element of NAT holds S3[k] from NAT_1:sch_1(A25, A14); A27: rng f c= [.a,b.] proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in [.a,b.] ) assume y in rng f ; ::_thesis: y in [.a,b.] then consider x being set such that A28: x in dom f and A29: y = f . x by FUNCT_1:def_3; reconsider n = x as Element of NAT by A28, FUNCT_2:def_1; A30: ( 2 |^ (n + 1) > 0 & b - a >= 0 ) by A1, NEWTON:83, XREAL_1:48; (f . n) + ((b - a) / (2 |^ (n + 1))) <= b by A26; then A31: f . n <= b by A30, XREAL_1:40; a <= (f . n) - ((b - a) / (2 |^ (n + 1))) by A26; then a <= f . n by A30, XREAL_1:51; then y in { y1 where y1 is Real : ( a <= y1 & y1 <= b ) } by A29, A31; hence y in [.a,b.] by RCOMP_1:def_1; ::_thesis: verum end; A32: for k being Element of NAT st S2[k] holds S2[k + 1] proof let k be Element of NAT ; ::_thesis: ( S2[k] implies S2[k + 1] ) assume A33: S2[k] ; ::_thesis: S2[k + 1] given G being Subset-Family of (Closed-Interval-MSpace (a,b)) such that A34: G c= F and A35: [.((f . (k + 1)) - ((b - a) / (2 |^ ((k + 1) + 1)))),((f . (k + 1)) + ((b - a) / (2 |^ ((k + 1) + 1)))).] c= union G and A36: G is finite ; ::_thesis: contradiction A37: (b - a) / (2 |^ (k + (1 + 1))) = (b - a) / (2 |^ ((k + 1) + 1)) .= (b - a) / ((2 |^ (k + 1)) * 2) by NEWTON:6 .= ((b - a) / (2 |^ (k + 1))) / 2 by XCMPLX_1:78 ; now__::_thesis:_contradiction percases ( ex G being Subset-Family of (Closed-Interval-MSpace (a,b)) st ( G c= F & [.((f . k) - ((b - a) / (2 |^ (k + 1)))),(f . k).] c= union G & G is finite ) or for G being Subset-Family of (Closed-Interval-MSpace (a,b)) holds ( not G c= F or not [.((f . k) - ((b - a) / (2 |^ (k + 1)))),(f . k).] c= union G or not G is finite ) ) ; supposeA38: ex G being Subset-Family of (Closed-Interval-MSpace (a,b)) st ( G c= F & [.((f . k) - ((b - a) / (2 |^ (k + 1)))),(f . k).] c= union G & G is finite ) ; ::_thesis: contradiction ( 2 |^ (k + 1) > 0 & b - a >= 0 ) by A1, NEWTON:83, XREAL_1:48; then ( (f . k) - ((b - a) / (2 |^ (k + 1))) <= f . k & f . k <= (f . k) + ((b - a) / (2 |^ (k + 1))) ) by XREAL_1:31, XREAL_1:43; then A39: [.((f . k) - ((b - a) / (2 |^ (k + 1)))),((f . k) + ((b - a) / (2 |^ (k + 1)))).] = [.((f . k) - ((b - a) / (2 |^ (k + 1)))),(f . k).] \/ [.(f . k),((f . k) + ((b - a) / (2 |^ (k + 1)))).] by XXREAL_1:165; A40: (f . (k + 1)) - ((b - a) / (2 |^ ((k + 1) + 1))) = ((f . k) + ((b - a) / (2 |^ (k + 2)))) - ((b - a) / (2 |^ (k + (1 + 1)))) by A11, A38 .= f . k ; consider G1 being Subset-Family of (Closed-Interval-MSpace (a,b)) such that A41: G1 c= F and A42: [.((f . k) - ((b - a) / (2 |^ (k + 1)))),(f . k).] c= union G1 and A43: G1 is finite by A38; reconsider G3 = G1 \/ G as Subset-Family of (Closed-Interval-MSpace (a,b)) ; (f . (k + 1)) + ((b - a) / (2 |^ ((k + 1) + 1))) = ((f . k) + ((b - a) / (2 |^ (k + 2)))) + ((b - a) / (2 |^ (k + (1 + 1)))) by A11, A38 .= ((f . k) + (((b - a) / (2 |^ (k + 1))) / 2)) + (((b - a) / (2 |^ (k + 1))) / 2) by A37 .= (f . k) + ((b - a) / (2 |^ (k + 1))) ; then [.((f . k) - ((b - a) / (2 |^ (k + 1)))),((f . k) + ((b - a) / (2 |^ (k + 1)))).] c= (union G1) \/ (union G) by A35, A42, A40, A39, XBOOLE_1:13; then [.((f . k) - ((b - a) / (2 |^ (k + 1)))),((f . k) + ((b - a) / (2 |^ (k + 1)))).] c= union G3 by ZFMISC_1:78; hence contradiction by A33, A34, A36, A41, A43, XBOOLE_1:8; ::_thesis: verum end; supposeA44: for G being Subset-Family of (Closed-Interval-MSpace (a,b)) holds ( not G c= F or not [.((f . k) - ((b - a) / (2 |^ (k + 1)))),(f . k).] c= union G or not G is finite ) ; ::_thesis: contradiction then A45: (f . (k + 1)) + ((b - a) / (2 |^ ((k + 1) + 1))) = ((f . k) - ((b - a) / (2 |^ (k + 2)))) + ((b - a) / (2 |^ (k + (1 + 1)))) by A11 .= f . k ; (f . (k + 1)) - ((b - a) / (2 |^ ((k + 1) + 1))) = ((f . k) - ((b - a) / (2 |^ (k + 2)))) - ((b - a) / (2 |^ (k + (1 + 1)))) by A11, A44 .= ((f . k) - (((b - a) / (2 |^ (k + 1))) / 2)) - (((b - a) / (2 |^ (k + 1))) / 2) by A37 .= (f . k) - ((b - a) / (2 |^ (k + 1))) ; hence contradiction by A34, A35, A36, A44, A45; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; A46: the carrier of (Closed-Interval-MSpace (a,b)) = [.a,b.] by A1, TOPMETR:10; A47: S2[ 0 ] proof given G being Subset-Family of (Closed-Interval-MSpace (a,b)) such that A48: G c= F and A49: [.((f . 0) - ((b - a) / (2 |^ (0 + 1)))),((f . 0) + ((b - a) / (2 |^ (0 + 1)))).] c= union G and A50: G is finite ; ::_thesis: contradiction the carrier of (Closed-Interval-MSpace (a,b)) c= union G by A1, A24, A12, A49, TOPMETR:10; then G is Cover of (Closed-Interval-MSpace (a,b)) by SETFAM_1:def_11; hence contradiction by A6, A48, A50; ::_thesis: verum end; reconsider f = f as Real_Sequence ; [.a,b.] is compact by RCOMP_1:6; then consider s being Real_Sequence such that A51: s is subsequence of f and A52: s is convergent and A53: lim s in [.a,b.] by A27, RCOMP_1:def_3; reconsider ls = lim s as Point of (Closed-Interval-MSpace (a,b)) by A1, A53, TOPMETR:10; consider Nseq being V40() sequence of NAT such that A54: s = f * Nseq by A51, VALUED_0:def_17; the carrier of (Closed-Interval-MSpace (a,b)) c= union F by A5, SETFAM_1:def_11; then consider Z being set such that A55: lim s in Z and A56: Z in F by A53, A46, TARSKI:def_4; consider p being Point of (Closed-Interval-MSpace (a,b)), r0 being Real such that A57: Z = Ball (p,r0) by A4, A56, TOPMETR:def_4; set G = {(Ball (p,r0))}; {(Ball (p,r0))} c= bool the carrier of (Closed-Interval-MSpace (a,b)) proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in {(Ball (p,r0))} or a in bool the carrier of (Closed-Interval-MSpace (a,b)) ) assume a in {(Ball (p,r0))} ; ::_thesis: a in bool the carrier of (Closed-Interval-MSpace (a,b)) then a = Ball (p,r0) by TARSKI:def_1; hence a in bool the carrier of (Closed-Interval-MSpace (a,b)) ; ::_thesis: verum end; then reconsider G = {(Ball (p,r0))} as Subset-Family of (Closed-Interval-MSpace (a,b)) ; A58: G c= F by A56, A57, ZFMISC_1:31; reconsider Ns = Nseq as Real_Sequence by RELSET_1:7; not Ns is bounded_above proof let r be real number ; :: according to SEQ_2:def_3 ::_thesis: ex b1 being Element of NAT st r <= Ns . b1 consider n being Element of NAT such that A59: n > r by SEQ_4:3; rng Nseq c= NAT by VALUED_0:def_6; then n <= Ns . n by Th2; hence ex b1 being Element of NAT st r <= Ns . b1 by A59, XXREAL_0:2; ::_thesis: verum end; then A60: 2 to_power Ns is divergent_to+infty by Th3, LIMFUNC1:31; then A61: (2 to_power Ns) " is convergent by LIMFUNC1:34; consider r1 being Real such that A62: r1 > 0 and A63: Ball (ls,r1) c= Ball (p,r0) by A55, A57, PCOMPS_1:27; A64: r1 / 2 > 0 by A62, XREAL_1:139; then consider n being Element of NAT such that A65: for m being Element of NAT st m >= n holds abs ((s . m) - (lim s)) < r1 / 2 by A52, SEQ_2:def_7; A66: for m being Element of NAT for q being Point of (Closed-Interval-MSpace (a,b)) st s . m = q & m >= n holds dist (ls,q) < r1 / 2 proof let m be Element of NAT ; ::_thesis: for q being Point of (Closed-Interval-MSpace (a,b)) st s . m = q & m >= n holds dist (ls,q) < r1 / 2 let q be Point of (Closed-Interval-MSpace (a,b)); ::_thesis: ( s . m = q & m >= n implies dist (ls,q) < r1 / 2 ) assume that A67: s . m = q and A68: m >= n ; ::_thesis: dist (ls,q) < r1 / 2 abs ((s . m) - (lim s)) < r1 / 2 by A65, A68; then A69: abs (- ((s . m) - (lim s))) < r1 / 2 by COMPLEX1:52; dist (ls,q) = the distance of (Closed-Interval-MSpace (a,b)) . ((lim s),(s . m)) by A67, METRIC_1:def_1 .= the distance of RealSpace . (ls,q) by A67, TOPMETR:def_1 .= abs ((lim s) - (s . m)) by A67, METRIC_1:def_12, METRIC_1:def_13 ; hence dist (ls,q) < r1 / 2 by A69; ::_thesis: verum end; A70: for m being Element of NAT st m >= n holds (f * Nseq) . m in Ball (ls,(r1 / 2)) proof let m be Element of NAT ; ::_thesis: ( m >= n implies (f * Nseq) . m in Ball (ls,(r1 / 2)) ) assume A71: m >= n ; ::_thesis: (f * Nseq) . m in Ball (ls,(r1 / 2)) ( dom f = NAT & s . m = f . (Nseq . m) ) by A54, FUNCT_2:15, FUNCT_2:def_1; then s . m in rng f by FUNCT_1:def_3; then reconsider q = s . m as Point of (Closed-Interval-MSpace (a,b)) by A1, A27, TOPMETR:10; dist (ls,q) < r1 / 2 by A66, A71; hence (f * Nseq) . m in Ball (ls,(r1 / 2)) by A54, METRIC_1:11; ::_thesis: verum end; lim ((2 to_power Ns) ") = 0 by A60, LIMFUNC1:34; then A72: lim ((b - a) (#) ((2 to_power Ns) ")) = (b - a) * 0 by A61, SEQ_2:8 .= 0 ; (b - a) (#) ((2 to_power Ns) ") is convergent by A61, SEQ_2:7; then consider i being Element of NAT such that A73: for m being Element of NAT st i <= m holds abs ((((b - a) (#) ((2 to_power Ns) ")) . m) - 0) < r1 / 2 by A64, A72, SEQ_2:def_7; set l = (i + 1) + n; A74: (i + 1) + n = (n + 1) + i ; [.((s . ((i + 1) + n)) - ((b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) "))),((s . ((i + 1) + n)) + ((b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) "))).] c= Ball (ls,r1) proof abs ((((b - a) (#) ((2 to_power Ns) ")) . ((i + 1) + n)) - 0) < r1 / 2 by A73, A74, NAT_1:11; then abs ((b - a) * (((2 to_power Ns) ") . ((i + 1) + n))) < r1 / 2 by SEQ_1:9; then abs ((b - a) * (((2 to_power Ns) . ((i + 1) + n)) ")) < r1 / 2 by VALUED_1:10; then abs ((b - a) * ((2 to_power (Ns . ((i + 1) + n))) ")) < r1 / 2 by Def1; then A75: abs ((b - a) * ((2 |^ (Nseq . ((i + 1) + n))) ")) < r1 / 2 by POWER:41; ( 2 |^ ((Nseq . ((i + 1) + n)) + 1) = 2 * (2 |^ (Nseq . ((i + 1) + n))) & 2 |^ (Nseq . ((i + 1) + n)) > 0 ) by NEWTON:6, NEWTON:83; then 1 / (2 |^ ((Nseq . ((i + 1) + n)) + 1)) < (2 |^ (Nseq . ((i + 1) + n))) " by XREAL_1:88, XREAL_1:155; then A76: (b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) ") < (b - a) * ((2 |^ (Nseq . ((i + 1) + n))) ") by A2, XREAL_1:68; ( 2 |^ ((Nseq . ((i + 1) + n)) + 1) > 0 & b - a >= 0 ) by A1, NEWTON:83, XREAL_1:48; then abs ((b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) ")) = (b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) ") by ABSVALUE:def_1; then abs ((b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) ")) < abs ((b - a) * ((2 |^ (Nseq . ((i + 1) + n))) ")) by A76, ABSVALUE:5; then A77: abs ((b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) ")) < r1 / 2 by A75, XXREAL_0:2; ( 2 |^ ((Nseq . ((i + 1) + n)) + 1) > 0 & b - a >= 0 ) by A1, NEWTON:83, XREAL_1:48; then A78: (b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) ") < r1 / 2 by A77, ABSVALUE:def_1; A79: s . ((i + 1) + n) in Ball (ls,(r1 / 2)) by A54, A70, NAT_1:11; then reconsider sl = s . ((i + 1) + n) as Point of (Closed-Interval-MSpace (a,b)) ; dist (ls,sl) < r1 / 2 by A79, METRIC_1:11; then A80: abs ((lim s) - (s . ((i + 1) + n))) < r1 / 2 by Th1; let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in [.((s . ((i + 1) + n)) - ((b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) "))),((s . ((i + 1) + n)) + ((b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) "))).] or z in Ball (ls,r1) ) A81: the carrier of (Closed-Interval-MSpace (a,b)) = [.a,b.] by A1, TOPMETR:10; assume z in [.((s . ((i + 1) + n)) - ((b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) "))),((s . ((i + 1) + n)) + ((b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) "))).] ; ::_thesis: z in Ball (ls,r1) then z in { m where m is Real : ( (s . ((i + 1) + n)) - ((b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) ")) <= m & m <= (s . ((i + 1) + n)) + ((b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) ")) ) } by RCOMP_1:def_1; then consider x being Real such that A82: x = z and A83: (s . ((i + 1) + n)) - ((b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) ")) <= x and A84: x <= (s . ((i + 1) + n)) + ((b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) ")) ; (f . (Nseq . ((i + 1) + n))) - ((b - a) / (2 |^ ((Nseq . ((i + 1) + n)) + 1))) >= a by A26; then (s . ((i + 1) + n)) - ((b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) ")) >= a by A54, FUNCT_2:15; then A85: x >= a by A83, XXREAL_0:2; (f . (Nseq . ((i + 1) + n))) + ((b - a) / (2 |^ ((Nseq . ((i + 1) + n)) + 1))) <= b by A26; then (s . ((i + 1) + n)) + ((b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) ")) <= b by A54, FUNCT_2:15; then x <= b by A84, XXREAL_0:2; then x in { m where m is Real : ( a <= m & m <= b ) } by A85; then reconsider x9 = x as Point of (Closed-Interval-MSpace (a,b)) by A81, RCOMP_1:def_1; abs ((lim s) - x) = abs (((lim s) - (s . ((i + 1) + n))) + ((s . ((i + 1) + n)) - x)) ; then A86: abs ((lim s) - x) <= (abs ((lim s) - (s . ((i + 1) + n)))) + (abs ((s . ((i + 1) + n)) - x)) by COMPLEX1:56; x - (s . ((i + 1) + n)) <= (b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) ") by A84, XREAL_1:20; then A87: - (x - (s . ((i + 1) + n))) >= - ((b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) ")) by XREAL_1:24; s . ((i + 1) + n) <= ((b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) ")) + x by A83, XREAL_1:20; then (s . ((i + 1) + n)) - x <= (b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) ") by XREAL_1:20; then abs ((s . ((i + 1) + n)) - x) <= (b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) ") by A87, ABSVALUE:5; then abs ((s . ((i + 1) + n)) - x) < r1 / 2 by A78, XXREAL_0:2; then (abs ((lim s) - (s . ((i + 1) + n)))) + (abs ((s . ((i + 1) + n)) - x)) < (r1 / 2) + (r1 / 2) by A80, XREAL_1:8; then abs ((lim s) - x) < (r1 / 2) + (r1 / 2) by A86, XXREAL_0:2; then dist (ls,x9) < r1 by Th1; hence z in Ball (ls,r1) by A82, METRIC_1:11; ::_thesis: verum end; then [.((s . ((i + 1) + n)) - ((b - a) / (2 |^ ((Nseq . ((i + 1) + n)) + 1)))),((s . ((i + 1) + n)) + ((b - a) * ((2 |^ ((Nseq . ((i + 1) + n)) + 1)) "))).] c= Ball (p,r0) by A63, XBOOLE_1:1; then [.((f . (Nseq . ((i + 1) + n))) - ((b - a) / (2 |^ ((Nseq . ((i + 1) + n)) + 1)))),((s . ((i + 1) + n)) + ((b - a) / (2 |^ ((Nseq . ((i + 1) + n)) + 1)))).] c= Ball (p,r0) by A54, FUNCT_2:15; then [.((f . (Nseq . ((i + 1) + n))) - ((b - a) / (2 |^ ((Nseq . ((i + 1) + n)) + 1)))),((f . (Nseq . ((i + 1) + n))) + ((b - a) / (2 |^ ((Nseq . ((i + 1) + n)) + 1)))).] c= Ball (p,r0) by A54, FUNCT_2:15; then A88: [.((f . (Nseq . ((i + 1) + n))) - ((b - a) / (2 |^ ((Nseq . ((i + 1) + n)) + 1)))),((f . (Nseq . ((i + 1) + n))) + ((b - a) / (2 |^ ((Nseq . ((i + 1) + n)) + 1)))).] c= union G by ZFMISC_1:25; for k being Element of NAT holds S2[k] from NAT_1:sch_1(A47, A32); hence contradiction by A58, A88; ::_thesis: verum end; end; end; hence Closed-Interval-TSpace (a,b) is compact ; ::_thesis: verum end;