:: SEQ_2 semantic presentation

begin


theorem Th1: :: SEQ_2:1
for g, r being real number holds
( ( - g < r & r < g ) iff abs r < g )
proof
let g, r be real number ; ::_thesis: ( ( - g < r & r < g ) iff abs r < g )
thus  ( - g < r & r < g implies abs r < g ) ::_thesis: ( abs r < g implies ( - g < r & r < g ) )
proof
assume that
A1: - g < r and
A2: r < g ; ::_thesis: abs r < g
A3: abs r <= g by A1, A2, ABSVALUE:5;
now__::_thesis:_not_abs_r_=_g
assume A4: abs r = g ; ::_thesis: contradiction
now__::_thesis:_not_r_<_0
assume  r < 0 ; ::_thesis: contradiction
then  g = - r by A4, ABSVALUE:def_1;
hence  contradiction by A1; ::_thesis: verum
end;
hence  contradiction by A2, A4, ABSVALUE:def_1; ::_thesis: verum
end;
hence  abs r < g by A3, XXREAL_0:1; ::_thesis: verum
end;
assume A5: abs r < g ; ::_thesis: ( - g < r & r < g )
then A6: - g <= r by ABSVALUE:5;
A7: 0 <= abs r by COMPLEX1:46;
A8: 0 < g by A5, COMPLEX1:46;
A9: - g < - 0 by A5, A7;
now__::_thesis:_not_r_=_-_g
assume  r = - g ; ::_thesis: contradiction
then  abs r = - (- g) by A9, ABSVALUE:def_1
.= g ;
hence  contradiction by A5; ::_thesis: verum
end;
hence  - g < r by A6, XXREAL_0:1; ::_thesis: r < g
thus  r < g by A5, A8, ABSVALUE:def_1; ::_thesis: verum
end;

theorem Th2: :: SEQ_2:2
for g, r being real number st g <> 0 & r <> 0 holds
abs ((g ") - (r ")) = (abs (g - r)) / ((abs g) * (abs r))
proof
let g, r be real number ; ::_thesis: ( g <> 0 & r <> 0 implies abs ((g ") - (r ")) = (abs (g - r)) / ((abs g) * (abs r)) )
assume that
A1: g <> 0 and
A2: r <> 0 ; ::_thesis: abs ((g ") - (r ")) = (abs (g - r)) / ((abs g) * (abs r))
thus  abs ((g ") - (r ")) = abs ((1 / g) - (r ")) by XCMPLX_1:215
.= abs ((1 / g) - (1 / r)) by XCMPLX_1:215
.= abs (((1 * r) - (1 * g)) / (g * r)) by A1, A2, XCMPLX_1:130
.= (abs (r - g)) / (abs (g * r)) by COMPLEX1:67
.= (abs (- (g - r))) / ((abs g) * (abs r)) by COMPLEX1:65
.= (abs (g - r)) / ((abs g) * (abs r)) by COMPLEX1:52 ; ::_thesis: verum
end;

definition
let f be real-valued Function;
attrf is bounded_above  means :Def1: :: SEQ_2:def 1
 ex r being real number st
for y being set st y in dom f holds
f . y < r;
attrf is bounded_below  means :Def2: :: SEQ_2:def 2
 ex r being real number st
for y being set st y in dom f holds
r < f . y;
end;

:: deftheorem Def1 defines bounded_above SEQ_2:def_1_:_
 for f being real-valued Function holds
( f is bounded_above iff ex r being real number st
for y being set st y in dom f holds
f . y < r );

:: deftheorem Def2 defines bounded_below SEQ_2:def_2_:_
 for f being real-valued Function holds
( f is bounded_below iff ex r being real number st
for y being set st y in dom f holds
r < f . y );

definition
let seq be Real_Sequence;
A1: dom seq = NAT by SEQ_1:1;
redefine attr seq is bounded_above  means :Def3: :: SEQ_2:def 3
 ex r being real number st
for n being Element of NAT holds seq . n < r;
compatibility
 ( seq is bounded_above iff ex r being real number st
for n being Element of NAT holds seq . n < r )
proof
thus  ( seq is bounded_above implies ex r being real number st
for n being Element of NAT holds seq . n < r ) ::_thesis: ( ex r being real number st
for n being Element of NAT holds seq . n < r implies seq is bounded_above )
proof
given r being real number  such that A2: for y being set st y in dom seq holds
seq . y < r ; :: according to SEQ_2:def_1 ::_thesis: ex r being real number st
for n being Element of NAT holds seq . n < r
take  r ; ::_thesis: for n being Element of NAT holds seq . n < r
let n be Element of NAT ; ::_thesis: seq . n < r
thus  seq . n < r by A1, A2; ::_thesis: verum
end;
given r being real number  such that A3: for n being Element of NAT holds seq . n < r ; ::_thesis: seq is bounded_above
take  r ; :: according to SEQ_2:def_1 ::_thesis: for y being set st y in dom seq holds
seq . y < r
let y be set ; ::_thesis: ( y in dom seq implies seq . y < r )
assume  y in dom seq ; ::_thesis: seq . y < r
hence  seq . y < r by A1, A3; ::_thesis: verum
end;
redefine attr seq is bounded_below  means :Def4: :: SEQ_2:def 4
 ex r being real number st
for n being Element of NAT holds r < seq . n;
compatibility
 ( seq is bounded_below iff ex r being real number st
for n being Element of NAT holds r < seq . n )
proof
thus  ( seq is bounded_below implies ex r being real number st
for n being Element of NAT holds r < seq . n ) ::_thesis: ( ex r being real number st
for n being Element of NAT holds r < seq . n implies seq is bounded_below )
proof
given r being real number  such that A4: for y being set st y in dom seq holds
r < seq . y ; :: according to SEQ_2:def_2 ::_thesis: ex r being real number st
for n being Element of NAT holds r < seq . n
take  r ; ::_thesis: for n being Element of NAT holds r < seq . n
let n be Element of NAT ; ::_thesis: r < seq . n
thus  r < seq . n by A1, A4; ::_thesis: verum
end;
given r being real number  such that A5: for n being Element of NAT holds r < seq . n ; ::_thesis: seq is bounded_below
take  r ; :: according to SEQ_2:def_2 ::_thesis: for y being set st y in dom seq holds
r < seq . y
let y be set ; ::_thesis: ( y in dom seq implies r < seq . y )
assume  y in dom seq ; ::_thesis: r < seq . y
hence  r < seq . y by A1, A5; ::_thesis: verum
end;
end;

:: deftheorem Def3 defines bounded_above SEQ_2:def_3_:_
 for seq being Real_Sequence holds
( seq is bounded_above iff ex r being real number st
for n being Element of NAT holds seq . n < r );

:: deftheorem Def4 defines bounded_below SEQ_2:def_4_:_
 for seq being Real_Sequence holds
( seq is bounded_below iff ex r being real number st
for n being Element of NAT holds r < seq . n );

registration
cluster Relation-like Function-like real-valued bounded  ->  real-valued bounded_above bounded_below for set ;
coherence
 for b1 being real-valued Function st b1 is bounded holds
( b1 is bounded_above & b1 is bounded_below )
proof
let f be real-valued Function; ::_thesis: ( f is bounded implies ( f is bounded_above & f is bounded_below ) )
given r being real number  such that A1: for y being set st y in dom f holds
abs (f . y) < r ; :: according to COMSEQ_2:def_3 ::_thesis: ( f is bounded_above & f is bounded_below )
thus  f is bounded_above ::_thesis: f is bounded_below
proof
take  r ; :: according to SEQ_2:def_1 ::_thesis: for y being set st y in dom f holds
f . y < r
let y be set ; ::_thesis: ( y in dom f implies f . y < r )
A2: f . y <= abs (f . y) by ABSVALUE:4;
assume  y in dom f ; ::_thesis: f . y < r
hence  f . y < r by A1, A2, XXREAL_0:2; ::_thesis: verum
end;
take  - (abs r) ; :: according to SEQ_2:def_2 ::_thesis: for y being set st y in dom f holds
- (abs r) < f . y
let y be set ; ::_thesis: ( y in dom f implies - (abs r) < f . y )
A3: - (abs (f . y)) <= f . y by ABSVALUE:4;
 r <= abs r by ABSVALUE:4;
then A4: - (abs r) <= - r by XREAL_1:24;
assume  y in dom f ; ::_thesis: - (abs r) < f . y
then  abs (f . y) < r by A1;
then  - r < - (abs (f . y)) by XREAL_1:24;
then  - (abs r) < - (abs (f . y)) by A4, XXREAL_0:2;
hence  - (abs r) < f . y by A3, XXREAL_0:2; ::_thesis: verum
end;
cluster Relation-like Function-like real-valued bounded_above bounded_below  ->  real-valued bounded for set ;
coherence
 for b1 being real-valued Function st b1 is bounded_above & b1 is bounded_below holds
b1 is bounded
proof
let f be real-valued Function; ::_thesis: ( f is bounded_above & f is bounded_below implies f is bounded )
assume  f is bounded_above ; ::_thesis: ( not f is bounded_below or f is bounded )
then consider r1 being real number  such that
A5: for y being set st y in dom f holds
f . y < r1 by Def1;
assume  f is bounded_below ; ::_thesis: f is bounded
then consider r2 being real number  such that
A6: for y being set st y in dom f holds
r2 < f . y by Def2;
take g = ((abs r1) + (abs r2)) + 1; :: according to COMSEQ_2:def_3 ::_thesis: for b1 being set holds
( not b1 in dom f or not g <= abs (f . b1) )
A7: 0 <= abs r1 by COMPLEX1:46;
let y be set ; ::_thesis: ( not y in dom f or not g <= abs (f . y) )
assume A8: y in dom f ; ::_thesis: not g <= abs (f . y)
 r1 <= abs r1 by ABSVALUE:4;
then  f . y < abs r1 by A5, A8, XXREAL_0:2;
then  (f . y) + 0 < (abs r1) + (abs r2) by COMPLEX1:46, XREAL_1:8;
then A9: f . y < g by XREAL_1:8;
 - (abs r2) <= r2 by ABSVALUE:4;
then  - (abs r2) < f . y by A6, A8, XXREAL_0:2;
then  (- (abs r1)) + (- (abs r2)) < 0 + (f . y) by A7, XREAL_1:8;
then A10: ((- (abs r1)) - (abs r2)) + (- 1) < (f . y) + 0 by XREAL_1:8;
 ((- (abs r1)) - (abs r2)) - 1 = - g ;
hence  abs (f . y) < g by A9, A10, Th1; ::_thesis: verum
end;
end;

theorem Th3: :: SEQ_2:3
for seq being Real_Sequence holds
( seq is bounded iff ex r being real number st
( 0 < r & ( for n being Element of NAT holds abs (seq . n) < r ) ) )
proof
let seq be Real_Sequence; ::_thesis: ( seq is bounded iff ex r being real number st
( 0 < r & ( for n being Element of NAT holds abs (seq . n) < r ) ) )
thus  ( seq is bounded implies ex r being real number st
( 0 < r & ( for n being Element of NAT holds abs (seq . n) < r ) ) ) ::_thesis: ( ex r being real number st
( 0 < r & ( for n being Element of NAT holds abs (seq . n) < r ) ) implies seq is bounded )
proof
assume A1: seq is bounded ; ::_thesis: ex r being real number st
( 0 < r & ( for n being Element of NAT holds abs (seq . n) < r ) )
then consider r1 being real number  such that
A2: for n being Element of NAT holds seq . n < r1 by Def3;
consider r2 being real number  such that
A3: for n being Element of NAT holds r2 < seq . n by A1, Def4;
take g = ((abs r1) + (abs r2)) + 1; ::_thesis: ( 0 < g & ( for n being Element of NAT holds abs (seq . n) < g ) )
A4: 0 <= abs r1 by COMPLEX1:46;
 0 <= abs r2 by COMPLEX1:46;
hence  0 < g by A4; ::_thesis: for n being Element of NAT holds abs (seq . n) < g
let n be Element of NAT ; ::_thesis: abs (seq . n) < g
 r1 <= abs r1 by ABSVALUE:4;
then  seq . n < abs r1 by A2, XXREAL_0:2;
then  (seq . n) + 0 < (abs r1) + (abs r2) by COMPLEX1:46, XREAL_1:8;
then A5: seq . n < g by XREAL_1:8;
 - (abs r2) <= r2 by ABSVALUE:4;
then  - (abs r2) < seq . n by A3, XXREAL_0:2;
then  (- (abs r1)) + (- (abs r2)) < 0 + (seq . n) by A4, XREAL_1:8;
then A6: ((- (abs r1)) - (abs r2)) + (- 1) < (seq . n) + 0 by XREAL_1:8;
 ((- (abs r1)) - (abs r2)) - 1 = - g ;
hence  abs (seq . n) < g by A5, A6, Th1; ::_thesis: verum
end;
given r being real number  such that  0 < r and
A7: for n being Element of NAT holds abs (seq . n) < r ; ::_thesis: seq is bounded
take  r ; :: according to COMSEQ_2:def_3 ::_thesis: for b1 being set holds
( not b1 in dom seq or not r <= abs (seq . b1) )
let y be set ; ::_thesis: ( not y in dom seq or not r <= abs (seq . y) )
assume  y in dom seq ; ::_thesis: not r <= abs (seq . y)
then  y is Element of NAT by FUNCT_2:def_1;
hence  not r <= abs (seq . y) by A7; ::_thesis: verum
end;

theorem Th4: :: SEQ_2:4
for seq being Real_Sequence
for n being Element of NAT ex r being real number st
( 0 < r & ( for m being Element of NAT st m <= n holds
abs (seq . m) < r ) )
proof
let seq be Real_Sequence; ::_thesis: for n being Element of NAT ex r being real number st
( 0 < r & ( for m being Element of NAT st m <= n holds
abs (seq . m) < r ) )
defpred S1[ Nat] means  ex r1 being real number st
( 0 < r1 & ( for m being Element of NAT st m <= $1 holds
abs (seq . m) < r1 ) );
A1: S1[ 0 ]
proof
reconsider r = (abs (seq . 0)) + 1 as real number ;
take  r ; ::_thesis: ( 0 < r & ( for m being Element of NAT st m <= 0 holds
abs (seq . m) < r ) )
 0 + 0 < (abs (seq . 0)) + 1 by COMPLEX1:46, XREAL_1:8;
hence  0 < r ; ::_thesis: for m being Element of NAT st m <= 0 holds
abs (seq . m) < r
let m be Element of NAT ; ::_thesis: ( m <= 0 implies abs (seq . m) < r )
assume  m <= 0 ; ::_thesis: abs (seq . m) < r
then  0 = m by NAT_1:2;
then  (abs (seq . m)) + 0 < r by XREAL_1:8;
hence  abs (seq . m) < r ; ::_thesis: verum
end;
A2: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
given r1 being real number  such that A3: 0 < r1 and
A4: for m being Element of NAT st m <= n holds
abs (seq . m) < r1 ; ::_thesis: S1[n + 1]
A5: now__::_thesis:_(_abs_(seq_._(n_+_1))_<=_r1_implies_ex_r_being_Element_of_REAL_st_
(_0_<_r_&_(_for_m_being_Element_of_NAT_st_m_<=_n_+_1_holds_
abs_(seq_._m)_<_r_)_)_)
assume A6: abs (seq . (n + 1)) <= r1 ; ::_thesis: ex r being Element of REAL st
( 0 < r & ( for m being Element of NAT st m <= n + 1 holds
abs (seq . m) < r ) )
take r = r1 + 1; ::_thesis: ( 0 < r & ( for m being Element of NAT st m <= n + 1 holds
abs (seq . m) < r ) )
thus  0 < r by A3; ::_thesis: for m being Element of NAT st m <= n + 1 holds
abs (seq . m) < r
let m be Element of NAT ; ::_thesis: ( m <= n + 1 implies abs (seq . m) < r )
assume A7: m <= n + 1 ; ::_thesis: abs (seq . m) < r
A8: now__::_thesis:_(_m_<=_n_implies_abs_(seq_._m)_<_r_)
assume  m <= n ; ::_thesis: abs (seq . m) < r
then A9: abs (seq . m) < r1 by A4;
 r1 + 0 < r by XREAL_1:8;
hence  abs (seq . m) < r by A9, XXREAL_0:2; ::_thesis: verum
end;
now__::_thesis:_(_m_=_n_+_1_implies_abs_(seq_._m)_<_r_)
assume A10: m = n + 1 ; ::_thesis: abs (seq . m) < r
 r1 + 0 < r by XREAL_1:8;
hence  abs (seq . m) < r by A6, A10, XXREAL_0:2; ::_thesis: verum
end;
hence  abs (seq . m) < r by A7, A8, NAT_1:8; ::_thesis: verum
end;
now__::_thesis:_(_r1_<=_abs_(seq_._(n_+_1))_implies_ex_r_being_Element_of_REAL_st_
(_0_<_r_&_(_for_m_being_Element_of_NAT_st_m_<=_n_+_1_holds_
abs_(seq_._m)_<_r_)_)_)
assume A11: r1 <= abs (seq . (n + 1)) ; ::_thesis: ex r being Element of REAL st
( 0 < r & ( for m being Element of NAT st m <= n + 1 holds
abs (seq . m) < r ) )
take r = (abs (seq . (n + 1))) + 1; ::_thesis: ( 0 < r & ( for m being Element of NAT st m <= n + 1 holds
abs (seq . m) < r ) )
 0 + 0 < r by COMPLEX1:46, XREAL_1:8;
hence  0 < r ; ::_thesis: for m being Element of NAT st m <= n + 1 holds
abs (seq . m) < r
let m be Element of NAT ; ::_thesis: ( m <= n + 1 implies abs (seq . m) < r )
assume A12: m <= n + 1 ; ::_thesis: abs (seq . m) < r
A13: now__::_thesis:_(_m_<=_n_implies_abs_(seq_._m)_<_r_)
assume  m <= n ; ::_thesis: abs (seq . m) < r
then  abs (seq . m) < r1 by A4;
then  abs (seq . m) < abs (seq . (n + 1)) by A11, XXREAL_0:2;
then  (abs (seq . m)) + 0 < r by XREAL_1:8;
hence  abs (seq . m) < r ; ::_thesis: verum
end;
now__::_thesis:_(_m_=_n_+_1_implies_abs_(seq_._m)_<_r_)
assume  m = n + 1 ; ::_thesis: abs (seq . m) < r
then  (abs (seq . m)) + 0 < r by XREAL_1:8;
hence  abs (seq . m) < r ; ::_thesis: verum
end;
hence  abs (seq . m) < r by A12, A13, NAT_1:8; ::_thesis: verum
end;
hence  S1[n + 1] by A5; ::_thesis: verum
end;
thus  for n being Element of NAT holds S1[n] from NAT_1:sch_1(A1, A2); ::_thesis: verum
end;

definition
canceled;
let seq be Real_Sequence;
redefine attr seq is convergent  means :Def6: :: SEQ_2:def 6
 ex g being real number st
for p being real number st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - g) < p;
compatibility
 ( seq is convergent iff ex g being real number st
for p being real number st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - g) < p )
proof
thus  ( seq is convergent implies ex g being real number st
for p being real number st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - g) < p ) ::_thesis: ( ex g being real number st
for p being real number st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - g) < p implies seq is convergent )
proof
assume  seq is convergent ; ::_thesis: ex g being real number st
for p being real number st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - g) < p
then consider g being Element of COMPLEX  such that
A1: for p being Real st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((seq . m) - g).| < p by COMSEQ_2:def_5;
A2: (Re g) + ((Im g) * <i>) = g by COMPLEX1:13;
now__::_thesis:_g_is_real
assume A3: not g is real ; ::_thesis: contradiction
A4: Im g <> 0 by A2, A3;
set p = abs (Im g);
A5: abs (Im g) > 0 by A4, COMPLEX1:47;
 for n being Element of NAT ex m being Element of NAT st
( n <= m & not |.((seq . m) - g).| < abs (Im g) )
proof
let n be Element of NAT ; ::_thesis: ex m being Element of NAT st
( n <= m & not |.((seq . m) - g).| < abs (Im g) )
take  n ; ::_thesis: ( n <= n & not |.((seq . n) - g).| < abs (Im g) )
thus  n <= n ; ::_thesis: not |.((seq . n) - g).| < abs (Im g)
A6: Im (seq . n) = 0 by COMPLEX1:def_2;
A7: Im ((seq . n) - g) = (Im (seq . n)) - (Im g) by COMPLEX1:19;
A8: |.((seq . n) - g).| = sqrt (((Re ((seq . n) - g)) ^2) + ((Im g) ^2)) by A7, A6;
 (Re ((seq . n) - g)) ^2 >= 0 by XREAL_1:63;
then  sqrt (((Re ((seq . n) - g)) ^2) + (|.(Im g).| ^2)) >= |.(Im g).| by SQUARE_1:58;
hence  |.((seq . n) - g).| >= |.(Im g).| by A8, COMPLEX1:75; ::_thesis: verum
end;
hence  contradiction by A1, A5; ::_thesis: verum
end;
then reconsider g = g as real number ;
take  g ; ::_thesis: for p being real number st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - g) < p
let p be real number ; ::_thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - g) < p )
reconsider p = p as Real by XREAL_0:def_1;
 ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - g) < p ) by A1;
hence  ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - g) < p ) ; ::_thesis: verum
end;
given g being real number  such that A9: for p being real number st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - g) < p ; ::_thesis: seq is convergent
 g in REAL by XREAL_0:def_1;
then reconsider g = g as Element of COMPLEX by NUMBERS:11;
take  g ; :: according to COMSEQ_2:def_5 ::_thesis: for b1 being Element of REAL holds
( b1 <= 0 or ex b2 being Element of NAT st
for b3 being Element of NAT holds
( not b2 <= b3 or not b1 <= |.((seq . b3) - g).| ) )
thus  for b1 being Element of REAL holds
( b1 <= 0 or ex b2 being Element of NAT st
for b3 being Element of NAT holds
( not b2 <= b3 or not b1 <= |.((seq . b3) - g).| ) ) by A9; ::_thesis: verum
end;
end;

:: deftheorem  SEQ_2:def_5_:_
canceled;

:: deftheorem Def6 defines convergent SEQ_2:def_6_:_
 for seq being Real_Sequence holds
( seq is convergent iff ex g being real number st
for p being real number st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - g) < p );

definition
let seq be Real_Sequence;
assume A1: seq is convergent ;
func lim seq ->  real number  means :Def7: :: SEQ_2:def 7
 for p being real number st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - it) < p;
existence
 ex b1 being real number st
for p being real number st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - b1) < p by A1, Def6;
uniqueness
 for b1, b2 being real number st ( for p being real number st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - b1) < p ) & ( for p being real number st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - b2) < p ) holds
b1 = b2
proof
given g1, g2 being real number  such that A2: for p being real number st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - g1) < p and
A3: for p being real number st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - g2) < p and
A4: g1 <> g2 ; ::_thesis: contradiction
A5: now__::_thesis:_not_abs_(g1_-_g2)_=_0
assume  abs (g1 - g2) = 0 ; ::_thesis: contradiction
then  0 + g2 = (g1 - g2) + g2 by ABSVALUE:2;
hence  contradiction by A4; ::_thesis: verum
end;
A6: 0 <= abs (g1 - g2) by COMPLEX1:46;
then consider n1 being Element of NAT  such that
A7: for m being Element of NAT st n1 <= m holds
abs ((seq . m) - g1) < (abs (g1 - g2)) / 4 by A2, A5;
consider n2 being Element of NAT  such that
A8: for m being Element of NAT st n2 <= m holds
abs ((seq . m) - g2) < (abs (g1 - g2)) / 4 by A3, A5, A6;
A9: abs ((seq . (n1 + n2)) - g1) < (abs (g1 - g2)) / 4 by A7, NAT_1:12;
 abs ((seq . (n1 + n2)) - g2) < (abs (g1 - g2)) / 4 by A8, NAT_1:12;
then A10: (abs ((seq . (n1 + n2)) - g2)) + (abs ((seq . (n1 + n2)) - g1)) < ((abs (g1 - g2)) / 4) + ((abs (g1 - g2)) / 4) by A9, XREAL_1:8;
 abs (g1 - g2) = abs ((- ((seq . (n1 + n2)) - g1)) + ((seq . (n1 + n2)) - g2)) ;
then  abs (g1 - g2) <= (abs (- ((seq . (n1 + n2)) - g1))) + (abs ((seq . (n1 + n2)) - g2)) by COMPLEX1:56;
then A11: abs (g1 - g2) <= (abs ((seq . (n1 + n2)) - g1)) + (abs ((seq . (n1 + n2)) - g2)) by COMPLEX1:52;
 (abs (g1 - g2)) / 2 < abs (g1 - g2) by A5, A6, XREAL_1:216;
hence  contradiction by A10, A11, XXREAL_0:2; ::_thesis: verum
end;
end;

:: deftheorem Def7 defines lim SEQ_2:def_7_:_
 for seq being Real_Sequence st seq is convergent holds
for b2 being real number holds
( b2 = lim seq iff for p being real number st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - b2) < p );

definition
let f be real-valued Function;
redefine attr f is bounded  means :: SEQ_2:def 8
( f is bounded_above & f is bounded_below );
compatibility
 ( f is bounded iff ( f is bounded_above & f is bounded_below ) ) ;
end;

:: deftheorem  defines bounded SEQ_2:def_8_:_
 for f being real-valued Function holds
( f is bounded iff ( f is bounded_above & f is bounded_below ) );

definition
let seq be Real_Sequence;
:: original: lim
redefine func lim seq ->  Real;
coherence
 lim seq is Real by XREAL_0:def_1;
end;

registration
cluster Function-like constant V30( NAT , REAL )  ->  convergent for Element of K11(K12(NAT,REAL));
coherence
 for b1 being Real_Sequence st b1 is constant holds
b1 is convergent
proof
let seq be Real_Sequence; ::_thesis: ( seq is constant implies seq is convergent )
assume  seq is constant ; ::_thesis: seq is convergent
then consider r being Real such that
A1: for n being Nat holds seq . n = r by VALUED_0:def_18;
take g = r; :: according to SEQ_2:def_6 ::_thesis: for p being real number st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - g) < p
let p be real number ; ::_thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - g) < p )
assume A2: 0 < p ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - g) < p
take n = 0 ; ::_thesis: for m being Element of NAT st n <= m holds
abs ((seq . m) - g) < p
let m be Element of NAT ; ::_thesis: ( n <= m implies abs ((seq . m) - g) < p )
assume  n <= m ; ::_thesis: abs ((seq . m) - g) < p
abs ((seq . m) - g) = abs (r - g) by A1
.= 0 by ABSVALUE:2 ;
hence  abs ((seq . m) - g) < p by A2; ::_thesis: verum
end;
end;

registration
cluster non zero Relation-like NAT -defined REAL -valued Function-like constant V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued for Element of K11(K12(NAT,REAL));
existence
 ex b1 being Real_Sequence st b1 is constant
proof
reconsider cs = NAT --> 0 as Real_Sequence by FUNCOP_1:45;
take  cs ; ::_thesis: cs is constant
thus  cs is constant ; ::_thesis: verum
end;
end;

theorem Th5: :: SEQ_2:5
for seq, seq9 being Real_Sequence st seq is convergent & seq9 is convergent holds
seq + seq9 is convergent
proof
let seq, seq9 be Real_Sequence; ::_thesis: ( seq is convergent & seq9 is convergent implies seq + seq9 is convergent )
assume that
A1: seq is convergent and
A2: seq9 is convergent ; ::_thesis: seq + seq9 is convergent
consider g1 being real number  such that
A3: for p being real number st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - g1) < p by A1, Def6;
consider g2 being real number  such that
A4: for p being real number st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq9 . m) - g2) < p by A2, Def6;
take g = g1 + g2; :: according to SEQ_2:def_6 ::_thesis: for p being real number st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((seq + seq9) . m) - g) < p
let p be real number ; ::_thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((seq + seq9) . m) - g) < p )
assume A5: 0 < p ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((seq + seq9) . m) - g) < p
then consider n1 being Element of NAT  such that
A6: for m being Element of NAT st n1 <= m holds
abs ((seq . m) - g1) < p / 2 by A3;
consider n2 being Element of NAT  such that
A7: for m being Element of NAT st n2 <= m holds
abs ((seq9 . m) - g2) < p / 2 by A4, A5;
take k = n1 + n2; ::_thesis: for m being Element of NAT st k <= m holds
abs (((seq + seq9) . m) - g) < p
let m be Element of NAT ; ::_thesis: ( k <= m implies abs (((seq + seq9) . m) - g) < p )
assume A8: k <= m ; ::_thesis: abs (((seq + seq9) . m) - g) < p
 n1 <= n1 + n2 by NAT_1:12;
then  n1 <= m by A8, XXREAL_0:2;
then A9: abs ((seq . m) - g1) < p / 2 by A6;
 n2 <= k by NAT_1:12;
then  n2 <= m by A8, XXREAL_0:2;
then  abs ((seq9 . m) - g2) < p / 2 by A7;
then A10: (abs ((seq . m) - g1)) + (abs ((seq9 . m) - g2)) < (p / 2) + (p / 2) by A9, XREAL_1:8;
A11: abs (((seq + seq9) . m) - g) = abs (((seq . m) + (seq9 . m)) - (g1 + g2)) by SEQ_1:7
.= abs (((seq . m) - g1) + ((seq9 . m) - g2)) ;
 abs (((seq . m) - g1) + ((seq9 . m) - g2)) <= (abs ((seq . m) - g1)) + (abs ((seq9 . m) - g2)) by COMPLEX1:56;
hence  abs (((seq + seq9) . m) - g) < p by A10, A11, XXREAL_0:2; ::_thesis: verum
end;

registration
let seq1, seq2 be convergent Real_Sequence;
clusterseq1 + seq2 ->  convergent for Real_Sequence;
coherence
 for b1 being Real_Sequence st b1 = seq1 + seq2 holds
b1 is convergent by Th5;
end;

theorem Th6: :: SEQ_2:6
for seq, seq9 being Real_Sequence st seq is convergent & seq9 is convergent holds
lim (seq + seq9) = (lim seq) + (lim seq9)
proof
let seq, seq9 be Real_Sequence; ::_thesis: ( seq is convergent & seq9 is convergent implies lim (seq + seq9) = (lim seq) + (lim seq9) )
assume that
A1: seq is convergent and
A2: seq9 is convergent ; ::_thesis: lim (seq + seq9) = (lim seq) + (lim seq9)
now__::_thesis:_for_p_being_real_number_st_0_<_p_holds_
ex_k_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_k_<=_m_holds_
abs_(((seq_+_seq9)_._m)_-_((lim_seq)_+_(lim_seq9)))_<_p
let p be real number ; ::_thesis: ( 0 < p implies ex k being Element of NAT st
for m being Element of NAT st k <= m holds
abs (((seq + seq9) . m) - ((lim seq) + (lim seq9))) < p )
assume  0 < p ; ::_thesis: ex k being Element of NAT st
for m being Element of NAT st k <= m holds
abs (((seq + seq9) . m) - ((lim seq) + (lim seq9))) < p
then A3: 0 < p / 2 ;
then consider n1 being Element of NAT  such that
A4: for m being Element of NAT st n1 <= m holds
abs ((seq . m) - (lim seq)) < p / 2 by A1, Def7;
consider n2 being Element of NAT  such that
A5: for m being Element of NAT st n2 <= m holds
abs ((seq9 . m) - (lim seq9)) < p / 2 by A2, A3, Def7;
take k = n1 + n2; ::_thesis: for m being Element of NAT st k <= m holds
abs (((seq + seq9) . m) - ((lim seq) + (lim seq9))) < p
let m be Element of NAT ; ::_thesis: ( k <= m implies abs (((seq + seq9) . m) - ((lim seq) + (lim seq9))) < p )
assume A6: k <= m ; ::_thesis: abs (((seq + seq9) . m) - ((lim seq) + (lim seq9))) < p
 n1 <= n1 + n2 by NAT_1:12;
then  n1 <= m by A6, XXREAL_0:2;
then A7: abs ((seq . m) - (lim seq)) < p / 2 by A4;
 n2 <= k by NAT_1:12;
then  n2 <= m by A6, XXREAL_0:2;
then  abs ((seq9 . m) - (lim seq9)) < p / 2 by A5;
then A8: (abs ((seq . m) - (lim seq))) + (abs ((seq9 . m) - (lim seq9))) < (p / 2) + (p / 2) by A7, XREAL_1:8;
A9: abs (((seq + seq9) . m) - ((lim seq) + (lim seq9))) = abs (((seq . m) + (seq9 . m)) - ((lim seq) + (lim seq9))) by SEQ_1:7
.= abs (((seq . m) - (lim seq)) + ((seq9 . m) - (lim seq9))) ;
 abs (((seq . m) - (lim seq)) + ((seq9 . m) - (lim seq9))) <= (abs ((seq . m) - (lim seq))) + (abs ((seq9 . m) - (lim seq9))) by COMPLEX1:56;
hence  abs (((seq + seq9) . m) - ((lim seq) + (lim seq9))) < p by A8, A9, XXREAL_0:2; ::_thesis: verum
end;
hence  lim (seq + seq9) = (lim seq) + (lim seq9) by A1, A2, Def7; ::_thesis: verum
end;

theorem Th7: :: SEQ_2:7
for r being real number
for seq being Real_Sequence st seq is convergent holds
r (#) seq is convergent
proof
let r be real number ; ::_thesis: for seq being Real_Sequence st seq is convergent holds
r (#) seq is convergent
let seq be Real_Sequence; ::_thesis: ( seq is convergent implies r (#) seq is convergent )
assume  seq is convergent ; ::_thesis: r (#) seq is convergent
then consider g1 being real number  such that
A1: for p being real number st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - g1) < p by Def6;
take g = r * g1; :: according to SEQ_2:def_6 ::_thesis: for p being real number st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((r (#) seq) . m) - g) < p
A2: now__::_thesis:_(_r_=_0_implies_for_p_being_real_number_st_0_<_p_holds_
ex_k_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_k_<=_m_holds_
abs_(((r_(#)_seq)_._m)_-_g)_<_p_)
assume A3: r = 0 ; ::_thesis: for p being real number st 0 < p holds
ex k being Element of NAT st
for m being Element of NAT st k <= m holds
abs (((r (#) seq) . m) - g) < p
let p be real number ; ::_thesis: ( 0 < p implies ex k being Element of NAT st
for m being Element of NAT st k <= m holds
abs (((r (#) seq) . m) - g) < p )
assume A4: 0 < p ; ::_thesis: ex k being Element of NAT st
for m being Element of NAT st k <= m holds
abs (((r (#) seq) . m) - g) < p
take k = 0 ; ::_thesis: for m being Element of NAT st k <= m holds
abs (((r (#) seq) . m) - g) < p
let m be Element of NAT ; ::_thesis: ( k <= m implies abs (((r (#) seq) . m) - g) < p )
assume  k <= m ; ::_thesis: abs (((r (#) seq) . m) - g) < p
abs (((r (#) seq) . m) - g) = abs ((0 * (seq . m)) - 0) by A3, SEQ_1:9
.= 0 by ABSVALUE:2 ;
hence  abs (((r (#) seq) . m) - g) < p by A4; ::_thesis: verum
end;
now__::_thesis:_(_r_<>_0_implies_for_p_being_real_number_st_0_<_p_holds_
ex_k_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_k_<=_m_holds_
abs_(((r_(#)_seq)_._m)_-_g)_<_p_)
assume A5: r <> 0 ; ::_thesis: for p being real number st 0 < p holds
ex k being Element of NAT st
for m being Element of NAT st k <= m holds
abs (((r (#) seq) . m) - g) < p
then A6: 0 < abs r by COMPLEX1:47;
let p be real number ; ::_thesis: ( 0 < p implies ex k being Element of NAT st
for m being Element of NAT st k <= m holds
abs (((r (#) seq) . m) - g) < p )
assume A7: 0 < p ; ::_thesis: ex k being Element of NAT st
for m being Element of NAT st k <= m holds
abs (((r (#) seq) . m) - g) < p
A8: 0 <> abs r by A5, COMPLEX1:47;
consider n1 being Element of NAT  such that
A9: for m being Element of NAT st n1 <= m holds
abs ((seq . m) - g1) < p / (abs r) by A1, A6, A7;
take k = n1; ::_thesis: for m being Element of NAT st k <= m holds
abs (((r (#) seq) . m) - g) < p
let m be Element of NAT ; ::_thesis: ( k <= m implies abs (((r (#) seq) . m) - g) < p )
assume  k <= m ; ::_thesis: abs (((r (#) seq) . m) - g) < p
then A10: abs ((seq . m) - g1) < p / (abs r) by A9;
A11: abs (((r (#) seq) . m) - g) = abs ((r * (seq . m)) - (r * g1)) by SEQ_1:9
.= abs (r * ((seq . m) - g1))
.= (abs r) * (abs ((seq . m) - g1)) by COMPLEX1:65 ;
(abs r) * (p / (abs r)) = (abs r) * (((abs r) ") * p) by XCMPLX_0:def_9
.= ((abs r) * ((abs r) ")) * p
.= 1 * p by A8, XCMPLX_0:def_7
.= p ;
hence  abs (((r (#) seq) . m) - g) < p by A6, A10, A11, XREAL_1:68; ::_thesis: verum
end;
hence  for p being real number st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((r (#) seq) . m) - g) < p by A2; ::_thesis: verum
end;

registration
let r be real number ;
let seq be convergent Real_Sequence;
clusterr (#) seq ->  convergent for Real_Sequence;
coherence
 for b1 being Real_Sequence st b1 = r (#) seq holds
b1 is convergent by Th7;
end;

theorem Th8: :: SEQ_2:8
for r being real number
for seq being Real_Sequence st seq is convergent holds
lim (r (#) seq) = r * (lim seq)
proof
let r be real number ; ::_thesis: for seq being Real_Sequence st seq is convergent holds
lim (r (#) seq) = r * (lim seq)
let seq be Real_Sequence; ::_thesis: ( seq is convergent implies lim (r (#) seq) = r * (lim seq) )
assume A1: seq is convergent ; ::_thesis: lim (r (#) seq) = r * (lim seq)
A2: now__::_thesis:_(_r_=_0_implies_for_p_being_real_number_st_0_<_p_holds_
ex_k_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_k_<=_m_holds_
abs_(((r_(#)_seq)_._m)_-_(r_*_(lim_seq)))_<_p_)
assume A3: r = 0 ; ::_thesis: for p being real number st 0 < p holds
ex k being Element of NAT st
for m being Element of NAT st k <= m holds
abs (((r (#) seq) . m) - (r * (lim seq))) < p
let p be real number ; ::_thesis: ( 0 < p implies ex k being Element of NAT st
for m being Element of NAT st k <= m holds
abs (((r (#) seq) . m) - (r * (lim seq))) < p )
assume A4: 0 < p ; ::_thesis: ex k being Element of NAT st
for m being Element of NAT st k <= m holds
abs (((r (#) seq) . m) - (r * (lim seq))) < p
take k = 0 ; ::_thesis: for m being Element of NAT st k <= m holds
abs (((r (#) seq) . m) - (r * (lim seq))) < p
let m be Element of NAT ; ::_thesis: ( k <= m implies abs (((r (#) seq) . m) - (r * (lim seq))) < p )
assume  k <= m ; ::_thesis: abs (((r (#) seq) . m) - (r * (lim seq))) < p
abs (((r (#) seq) . m) - (r * (lim seq))) = abs ((0 * (seq . m)) - 0) by A3, SEQ_1:9
.= 0 by ABSVALUE:2 ;
hence  abs (((r (#) seq) . m) - (r * (lim seq))) < p by A4; ::_thesis: verum
end;
now__::_thesis:_(_r_<>_0_implies_for_p_being_real_number_st_0_<_p_holds_
ex_k_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_k_<=_m_holds_
abs_(((r_(#)_seq)_._m)_-_(r_*_(lim_seq)))_<_p_)
assume A5: r <> 0 ; ::_thesis: for p being real number st 0 < p holds
ex k being Element of NAT st
for m being Element of NAT st k <= m holds
abs (((r (#) seq) . m) - (r * (lim seq))) < p
then A6: 0 < abs r by COMPLEX1:47;
let p be real number ; ::_thesis: ( 0 < p implies ex k being Element of NAT st
for m being Element of NAT st k <= m holds
abs (((r (#) seq) . m) - (r * (lim seq))) < p )
assume A7: 0 < p ; ::_thesis: ex k being Element of NAT st
for m being Element of NAT st k <= m holds
abs (((r (#) seq) . m) - (r * (lim seq))) < p
A8: 0 <> abs r by A5, COMPLEX1:47;
 0 < p / (abs r) by A6, A7;
then consider n1 being Element of NAT  such that
A9: for m being Element of NAT st n1 <= m holds
abs ((seq . m) - (lim seq)) < p / (abs r) by A1, Def7;
take k = n1; ::_thesis: for m being Element of NAT st k <= m holds
abs (((r (#) seq) . m) - (r * (lim seq))) < p
let m be Element of NAT ; ::_thesis: ( k <= m implies abs (((r (#) seq) . m) - (r * (lim seq))) < p )
assume  k <= m ; ::_thesis: abs (((r (#) seq) . m) - (r * (lim seq))) < p
then A10: abs ((seq . m) - (lim seq)) < p / (abs r) by A9;
A11: abs (((r (#) seq) . m) - (r * (lim seq))) = abs ((r * (seq . m)) - (r * (lim seq))) by SEQ_1:9
.= abs (r * ((seq . m) - (lim seq)))
.= (abs r) * (abs ((seq . m) - (lim seq))) by COMPLEX1:65 ;
(abs r) * (p / (abs r)) = (abs r) * (((abs r) ") * p) by XCMPLX_0:def_9
.= ((abs r) * ((abs r) ")) * p
.= 1 * p by A8, XCMPLX_0:def_7
.= p ;
hence  abs (((r (#) seq) . m) - (r * (lim seq))) < p by A6, A10, A11, XREAL_1:68; ::_thesis: verum
end;
hence  lim (r (#) seq) = r * (lim seq) by A1, A2, Def7; ::_thesis: verum
end;

theorem :: SEQ_2:9
for seq being Real_Sequence st seq is convergent holds
- seq is convergent ;

registration
let seq be convergent Real_Sequence;
cluster - seq ->  convergent for Real_Sequence;
coherence
 for b1 being Real_Sequence st b1 = - seq holds
b1 is convergent ;
end;

theorem Th10: :: SEQ_2:10
for seq being Real_Sequence st seq is convergent holds
lim (- seq) = - (lim seq)
proof
let seq be Real_Sequence; ::_thesis: ( seq is convergent implies lim (- seq) = - (lim seq) )
assume  seq is convergent ; ::_thesis: lim (- seq) = - (lim seq)
then  lim ((- 1) (#) seq) = (- 1) * (lim seq) by Th8;
hence  lim (- seq) = - (lim seq) ; ::_thesis: verum
end;

theorem Th11: :: SEQ_2:11
for seq, seq9 being Real_Sequence st seq is convergent & seq9 is convergent holds
seq - seq9 is convergent
proof
let seq, seq9 be Real_Sequence; ::_thesis: ( seq is convergent & seq9 is convergent implies seq - seq9 is convergent )
assume that
A1: seq is convergent and
A2: seq9 is convergent ; ::_thesis: seq - seq9 is convergent
 - seq9 is convergent by A2;
hence  seq - seq9 is convergent by A1; ::_thesis: verum
end;

registration
let seq1, seq2 be convergent Real_Sequence;
clusterseq1 - seq2 ->  convergent for Real_Sequence;
coherence
 for b1 being Real_Sequence st b1 = seq1 - seq2 holds
b1 is convergent by Th11;
end;

theorem Th12: :: SEQ_2:12
for seq, seq9 being Real_Sequence st seq is convergent & seq9 is convergent holds
lim (seq - seq9) = (lim seq) - (lim seq9)
proof
let seq, seq9 be Real_Sequence; ::_thesis: ( seq is convergent & seq9 is convergent implies lim (seq - seq9) = (lim seq) - (lim seq9) )
assume that
A1: seq is convergent and
A2: seq9 is convergent ; ::_thesis: lim (seq - seq9) = (lim seq) - (lim seq9)
thus  lim (seq - seq9) = (lim seq) + (lim (- seq9)) by A1, A2, Th6
.= (lim seq) + (- (lim seq9)) by A2, Th10
.= (lim seq) - (lim seq9) ; ::_thesis: verum
end;

theorem Th13: :: SEQ_2:13
for seq being Real_Sequence st seq is convergent holds
seq is bounded
proof
let seq be Real_Sequence; ::_thesis: ( seq is convergent implies seq is bounded )
assume  seq is convergent ; ::_thesis: seq is bounded
then consider g being real number  such that
A1: for p being real number st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - g) < p by Def6;
consider n1 being Element of NAT  such that
A2: for m being Element of NAT st n1 <= m holds
abs ((seq . m) - g) < 1 by A1;
A3: now__::_thesis:_ex_r_being_Element_of_REAL_st_
(_0_<_r_&_(_for_m_being_Element_of_NAT_st_n1_<=_m_holds_
abs_(seq_._m)_<_r_)_)
take r = (abs g) + 1; ::_thesis: ( 0 < r & ( for m being Element of NAT st n1 <= m holds
abs (seq . m) < r ) )
 0 + 0 < r by COMPLEX1:46, XREAL_1:8;
hence  0 < r ; ::_thesis: for m being Element of NAT st n1 <= m holds
abs (seq . m) < r
let m be Element of NAT ; ::_thesis: ( n1 <= m implies abs (seq . m) < r )
assume  n1 <= m ; ::_thesis: abs (seq . m) < r
then A4: abs ((seq . m) - g) < 1 by A2;
 (abs (seq . m)) - (abs g) <= abs ((seq . m) - g) by COMPLEX1:59;
then A5: (abs (seq . m)) - (abs g) < 1 by A4, XXREAL_0:2;
 ((abs (seq . m)) - (abs g)) + (abs g) = abs (seq . m) ;
hence  abs (seq . m) < r by A5, XREAL_1:6; ::_thesis: verum
end;
now__::_thesis:_ex_r_being_set_st_
(_0_<_r_&_(_for_m_being_Element_of_NAT_holds_abs_(seq_._m)_<_r_)_)
consider r1 being real number  such that
A6: 0 < r1 and
A7: for m being Element of NAT st n1 <= m holds
abs (seq . m) < r1 by A3;
consider r2 being real number  such that
A8: 0 < r2 and
A9: for m being Element of NAT st m <= n1 holds
abs (seq . m) < r2 by Th4;
take r = r1 + r2; ::_thesis: ( 0 < r & ( for m being Element of NAT holds abs (seq . m) < r ) )
thus  0 < r by A6, A8; ::_thesis: for m being Element of NAT holds abs (seq . m) < r
A10: r1 + 0 < r by A8, XREAL_1:8;
A11: 0 + r2 < r by A6, XREAL_1:8;
let m be Element of NAT ; ::_thesis: abs (seq . m) < r
A12: now__::_thesis:_(_n1_<=_m_implies_abs_(seq_._m)_<_r_)
assume  n1 <= m ; ::_thesis: abs (seq . m) < r
then  abs (seq . m) < r1 by A7;
hence  abs (seq . m) < r by A10, XXREAL_0:2; ::_thesis: verum
end;
now__::_thesis:_(_m_<=_n1_implies_abs_(seq_._m)_<_r_)
assume  m <= n1 ; ::_thesis: abs (seq . m) < r
then  abs (seq . m) < r2 by A9;
hence  abs (seq . m) < r by A11, XXREAL_0:2; ::_thesis: verum
end;
hence  abs (seq . m) < r by A12; ::_thesis: verum
end;
hence  seq is bounded by Th3; ::_thesis: verum
end;

registration
cluster Function-like V30( NAT , REAL ) convergent  ->  bounded for Element of K11(K12(NAT,REAL));
coherence
 for b1 being Real_Sequence st b1 is convergent holds
b1 is bounded by Th13;
end;

theorem Th14: :: SEQ_2:14
for seq, seq9 being Real_Sequence st seq is convergent & seq9 is convergent holds
seq (#) seq9 is convergent
proof
let seq, seq9 be Real_Sequence; ::_thesis: ( seq is convergent & seq9 is convergent implies seq (#) seq9 is convergent )
assume that
A1: seq is convergent and
A2: seq9 is convergent ; ::_thesis: seq (#) seq9 is convergent
consider g1 being real number  such that
A3: for p being real number st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - g1) < p by A1, Def6;
consider g2 being real number  such that
A4: for p being real number st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq9 . m) - g2) < p by A2, Def6;
take g = g1 * g2; :: according to SEQ_2:def_6 ::_thesis: for p being real number st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((seq (#) seq9) . m) - g) < p
consider r being real number  such that
A5: 0 < r and
A6: for n being Element of NAT holds abs (seq . n) < r by A1, Th3;
A7: 0 <= abs g2 by COMPLEX1:46;
A8: 0 + 0 < (abs g2) + r by A5, COMPLEX1:46, XREAL_1:8;
let p be real number ; ::_thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((seq (#) seq9) . m) - g) < p )
assume A9: 0 < p ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((seq (#) seq9) . m) - g) < p
then consider n1 being Element of NAT  such that
A10: for m being Element of NAT st n1 <= m holds
abs ((seq . m) - g1) < p / ((abs g2) + r) by A3, A8;
consider n2 being Element of NAT  such that
A11: for m being Element of NAT st n2 <= m holds
abs ((seq9 . m) - g2) < p / ((abs g2) + r) by A4, A8, A9;
take n = n1 + n2; ::_thesis: for m being Element of NAT st n <= m holds
abs (((seq (#) seq9) . m) - g) < p
let m be Element of NAT ; ::_thesis: ( n <= m implies abs (((seq (#) seq9) . m) - g) < p )
assume A12: n <= m ; ::_thesis: abs (((seq (#) seq9) . m) - g) < p
A13: 0 <= abs (seq . m) by COMPLEX1:46;
A14: 0 <= abs ((seq9 . m) - g2) by COMPLEX1:46;
 n2 <= n by NAT_1:12;
then  n2 <= m by A12, XXREAL_0:2;
then A15: abs ((seq9 . m) - g2) < p / ((abs g2) + r) by A11;
 n1 <= n1 + n2 by NAT_1:12;
then  n1 <= m by A12, XXREAL_0:2;
then A16: abs ((seq . m) - g1) <= p / ((abs g2) + r) by A10;
abs (((seq (#) seq9) . m) - g) = abs ((((seq . m) * (seq9 . m)) - (((seq . m) * g2) - ((seq . m) * g2))) - (g1 * g2)) by SEQ_1:8
.= abs (((seq . m) * ((seq9 . m) - g2)) + (((seq . m) - g1) * g2)) ;
then A17: abs (((seq (#) seq9) . m) - g) <= (abs ((seq . m) * ((seq9 . m) - g2))) + (abs (((seq . m) - g1) * g2)) by COMPLEX1:56;
 abs (seq . m) < r by A6;
then  (abs (seq . m)) * (abs ((seq9 . m) - g2)) < r * (p / ((abs g2) + r)) by A13, A14, A15, XREAL_1:96;
then A18: abs ((seq . m) * ((seq9 . m) - g2)) < r * (p / ((abs g2) + r)) by COMPLEX1:65;
 abs (((seq . m) - g1) * g2) = (abs g2) * (abs ((seq . m) - g1)) by COMPLEX1:65;
then A19: abs (((seq . m) - g1) * g2) <= (abs g2) * (p / ((abs g2) + r)) by A7, A16, XREAL_1:64;
(r * (p / ((abs g2) + r))) + ((abs g2) * (p / ((abs g2) + r))) = (p / ((abs g2) + r)) * ((abs g2) + r)
.= p by A8, XCMPLX_1:87 ;
then  (abs ((seq . m) * ((seq9 . m) - g2))) + (abs (((seq . m) - g1) * g2)) < p by A18, A19, XREAL_1:8;
hence  abs (((seq (#) seq9) . m) - g) < p by A17, XXREAL_0:2; ::_thesis: verum
end;

registration
let seq1, seq2 be convergent Real_Sequence;
clusterseq1 (#) seq2 ->  convergent for Real_Sequence;
coherence
 for b1 being Real_Sequence st b1 = seq1 (#) seq2 holds
b1 is convergent by Th14;
end;

theorem Th15: :: SEQ_2:15
for seq, seq9 being Real_Sequence st seq is convergent & seq9 is convergent holds
lim (seq (#) seq9) = (lim seq) * (lim seq9)
proof
let seq, seq9 be Real_Sequence; ::_thesis: ( seq is convergent & seq9 is convergent implies lim (seq (#) seq9) = (lim seq) * (lim seq9) )
assume that
A1: seq is convergent and
A2: seq9 is convergent ; ::_thesis: lim (seq (#) seq9) = (lim seq) * (lim seq9)
consider r being real number  such that
A3: 0 < r and
A4: for n being Element of NAT holds abs (seq . n) < r by A1, Th3;
A5: 0 <= abs (lim seq9) by COMPLEX1:46;
A6: 0 + 0 < (abs (lim seq9)) + r by A3, COMPLEX1:46, XREAL_1:8;
now__::_thesis:_for_p_being_real_number_st_0_<_p_holds_
ex_n_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_n_<=_m_holds_
abs_(((seq_(#)_seq9)_._m)_-_((lim_seq)_*_(lim_seq9)))_<_p
let p be real number ; ::_thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((seq (#) seq9) . m) - ((lim seq) * (lim seq9))) < p )
assume  0 < p ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((seq (#) seq9) . m) - ((lim seq) * (lim seq9))) < p
then A7: 0 < p / ((abs (lim seq9)) + r) by A6;
then consider n1 being Element of NAT  such that
A8: for m being Element of NAT st n1 <= m holds
abs ((seq . m) - (lim seq)) < p / ((abs (lim seq9)) + r) by A1, Def7;
consider n2 being Element of NAT  such that
A9: for m being Element of NAT st n2 <= m holds
abs ((seq9 . m) - (lim seq9)) < p / ((abs (lim seq9)) + r) by A2, A7, Def7;
take n = n1 + n2; ::_thesis: for m being Element of NAT st n <= m holds
abs (((seq (#) seq9) . m) - ((lim seq) * (lim seq9))) < p
let m be Element of NAT ; ::_thesis: ( n <= m implies abs (((seq (#) seq9) . m) - ((lim seq) * (lim seq9))) < p )
assume A10: n <= m ; ::_thesis: abs (((seq (#) seq9) . m) - ((lim seq) * (lim seq9))) < p
A11: 0 <= abs (seq . m) by COMPLEX1:46;
A12: 0 <= abs ((seq9 . m) - (lim seq9)) by COMPLEX1:46;
 n2 <= n by NAT_1:12;
then  n2 <= m by A10, XXREAL_0:2;
then A13: abs ((seq9 . m) - (lim seq9)) < p / ((abs (lim seq9)) + r) by A9;
 n1 <= n1 + n2 by NAT_1:12;
then  n1 <= m by A10, XXREAL_0:2;
then A14: abs ((seq . m) - (lim seq)) <= p / ((abs (lim seq9)) + r) by A8;
abs (((seq (#) seq9) . m) - ((lim seq) * (lim seq9))) = abs ((((seq . m) * (seq9 . m)) - (((seq . m) * (lim seq9)) - ((seq . m) * (lim seq9)))) - ((lim seq) * (lim seq9))) by SEQ_1:8
.= abs (((seq . m) * ((seq9 . m) - (lim seq9))) + (((seq . m) - (lim seq)) * (lim seq9))) ;
then A15: abs (((seq (#) seq9) . m) - ((lim seq) * (lim seq9))) <= (abs ((seq . m) * ((seq9 . m) - (lim seq9)))) + (abs (((seq . m) - (lim seq)) * (lim seq9))) by COMPLEX1:56;
 abs (seq . m) < r by A4;
then  (abs (seq . m)) * (abs ((seq9 . m) - (lim seq9))) < r * (p / ((abs (lim seq9)) + r)) by A11, A12, A13, XREAL_1:96;
then A16: abs ((seq . m) * ((seq9 . m) - (lim seq9))) < r * (p / ((abs (lim seq9)) + r)) by COMPLEX1:65;
 abs (((seq . m) - (lim seq)) * (lim seq9)) = (abs (lim seq9)) * (abs ((seq . m) - (lim seq))) by COMPLEX1:65;
then A17: abs (((seq . m) - (lim seq)) * (lim seq9)) <= (abs (lim seq9)) * (p / ((abs (lim seq9)) + r)) by A5, A14, XREAL_1:64;
(r * (p / ((abs (lim seq9)) + r))) + ((abs (lim seq9)) * (p / ((abs (lim seq9)) + r))) = (p / ((abs (lim seq9)) + r)) * ((abs (lim seq9)) + r)
.= p by A6, XCMPLX_1:87 ;
then  (abs ((seq . m) * ((seq9 . m) - (lim seq9)))) + (abs (((seq . m) - (lim seq)) * (lim seq9))) < p by A16, A17, XREAL_1:8;
hence  abs (((seq (#) seq9) . m) - ((lim seq) * (lim seq9))) < p by A15, XXREAL_0:2; ::_thesis: verum
end;
hence  lim (seq (#) seq9) = (lim seq) * (lim seq9) by A1, A2, Def7; ::_thesis: verum
end;

theorem Th16: :: SEQ_2:16
for seq being Real_Sequence st seq is convergent & lim seq <> 0 holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
(abs (lim seq)) / 2 < abs (seq . m)
proof
let seq be Real_Sequence; ::_thesis: ( seq is convergent & lim seq <> 0 implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
(abs (lim seq)) / 2 < abs (seq . m) )
assume that
A1: seq is convergent and
A2: lim seq <> 0 ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
(abs (lim seq)) / 2 < abs (seq . m)
 0 < abs (lim seq) by A2, COMPLEX1:47;
then  0 < (abs (lim seq)) / 2 ;
then consider n1 being Element of NAT  such that
A3: for m being Element of NAT st n1 <= m holds
abs ((seq . m) - (lim seq)) < (abs (lim seq)) / 2 by A1, Def7;
take n = n1; ::_thesis: for m being Element of NAT st n <= m holds
(abs (lim seq)) / 2 < abs (seq . m)
let m be Element of NAT ; ::_thesis: ( n <= m implies (abs (lim seq)) / 2 < abs (seq . m) )
assume  n <= m ; ::_thesis: (abs (lim seq)) / 2 < abs (seq . m)
then A4: abs ((seq . m) - (lim seq)) < (abs (lim seq)) / 2 by A3;
A5: (abs (lim seq)) - (abs (seq . m)) <= abs ((lim seq) - (seq . m)) by COMPLEX1:59;
abs ((lim seq) - (seq . m)) = abs (- ((seq . m) - (lim seq)))
.= abs ((seq . m) - (lim seq)) by COMPLEX1:52 ;
then A6: (abs (lim seq)) - (abs (seq . m)) < (abs (lim seq)) / 2 by A4, A5, XXREAL_0:2;
A7: ((abs (lim seq)) / 2) + ((abs (seq . m)) - ((abs (lim seq)) / 2)) = abs (seq . m) ;
 ((abs (lim seq)) - (abs (seq . m))) + ((abs (seq . m)) - ((abs (lim seq)) / 2)) = (abs (lim seq)) / 2 ;
hence  (abs (lim seq)) / 2 < abs (seq . m) by A6, A7, XREAL_1:6; ::_thesis: verum
end;

theorem Th17: :: SEQ_2:17
for seq being Real_Sequence st seq is convergent & ( for n being Element of NAT holds 0 <= seq . n ) holds
0 <= lim seq
proof
let seq be Real_Sequence; ::_thesis: ( seq is convergent & ( for n being Element of NAT holds 0 <= seq . n ) implies 0 <= lim seq )
assume that
A1: seq is convergent and
A2: for n being Element of NAT holds 0 <= seq . n and
A3: not 0 <= lim seq ; ::_thesis: contradiction
 0 < - (lim seq) by A3;
then consider n1 being Element of NAT  such that
A4: for m being Element of NAT st n1 <= m holds
abs ((seq . m) - (lim seq)) < - (lim seq) by A1, Def7;
 abs ((seq . n1) - (lim seq)) <= - (lim seq) by A4;
then  (seq . n1) - (lim seq) <= - (lim seq) by ABSVALUE:5;
then A5: ((seq . n1) - (lim seq)) + (lim seq) <= (- (lim seq)) + (lim seq) by XREAL_1:6;
now__::_thesis:_not_seq_._n1_=_0
assume  seq . n1 = 0 ; ::_thesis: contradiction
then  abs ((seq . n1) - (lim seq)) = - (lim seq) by A3, ABSVALUE:def_1;
hence  contradiction by A4; ::_thesis: verum
end;
hence  contradiction by A2, A5; ::_thesis: verum
end;

theorem :: SEQ_2:18
for seq, seq9 being Real_Sequence st seq is convergent & seq9 is convergent & ( for n being Element of NAT holds seq . n <= seq9 . n ) holds
lim seq <= lim seq9
proof
let seq, seq9 be Real_Sequence; ::_thesis: ( seq is convergent & seq9 is convergent & ( for n being Element of NAT holds seq . n <= seq9 . n ) implies lim seq <= lim seq9 )
assume that
A1: seq is convergent and
A2: seq9 is convergent and
A3: for n being Element of NAT holds seq . n <= seq9 . n ; ::_thesis: lim seq <= lim seq9
now__::_thesis:_for_n_being_Element_of_NAT_holds_0_<=_(seq9_-_seq)_._n
let n be Element of NAT ; ::_thesis: 0 <= (seq9 - seq) . n
 seq . n <= seq9 . n by A3;
then A4: (seq . n) - (seq . n) <= (seq9 . n) - (seq . n) by XREAL_1:9;
(seq9 - seq) . n = (seq9 . n) + ((- seq) . n) by SEQ_1:7
.= (seq9 . n) + (- (seq . n)) by SEQ_1:10
.= (seq9 . n) - (seq . n) ;
hence  0 <= (seq9 - seq) . n by A4; ::_thesis: verum
end;
then A5: 0 <= lim (seq9 - seq) by A1, A2, Th17;
 lim (seq9 - seq) = (lim seq9) - (lim seq) by A1, A2, Th12;
then  0 + (lim seq) <= ((lim seq9) - (lim seq)) + (lim seq) by A5, XREAL_1:6;
hence  lim seq <= lim seq9 ; ::_thesis: verum
end;

theorem Th19: :: SEQ_2:19
for seq, seq9, seq1 being Real_Sequence st seq is convergent & seq9 is convergent & ( for n being Element of NAT holds
( seq . n <= seq1 . n & seq1 . n <= seq9 . n ) ) & lim seq = lim seq9 holds
seq1 is convergent
proof
let seq, seq9, seq1 be Real_Sequence; ::_thesis: ( seq is convergent & seq9 is convergent & ( for n being Element of NAT holds
( seq . n <= seq1 . n & seq1 . n <= seq9 . n ) ) & lim seq = lim seq9 implies seq1 is convergent )
assume that
A1: seq is convergent and
A2: seq9 is convergent and
A3: for n being Element of NAT holds
( seq . n <= seq1 . n & seq1 . n <= seq9 . n ) and
A4: lim seq = lim seq9 ; ::_thesis: seq1 is convergent
take  lim seq ; :: according to SEQ_2:def_6 ::_thesis: for p being real number st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq1 . m) - (lim seq)) < p
let p be real number ; ::_thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq1 . m) - (lim seq)) < p )
assume A5: 0 < p ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq1 . m) - (lim seq)) < p
then consider n1 being Element of NAT  such that
A6: for m being Element of NAT st n1 <= m holds
abs ((seq . m) - (lim seq)) < p by A1, Def7;
consider n2 being Element of NAT  such that
A7: for m being Element of NAT st n2 <= m holds
abs ((seq9 . m) - (lim seq)) < p by A2, A4, A5, Def7;
take n = n1 + n2; ::_thesis: for m being Element of NAT st n <= m holds
abs ((seq1 . m) - (lim seq)) < p
let m be Element of NAT ; ::_thesis: ( n <= m implies abs ((seq1 . m) - (lim seq)) < p )
assume A8: n <= m ; ::_thesis: abs ((seq1 . m) - (lim seq)) < p
 n2 <= n by NAT_1:12;
then  n2 <= m by A8, XXREAL_0:2;
then  abs ((seq9 . m) - (lim seq)) < p by A7;
then A9: (seq9 . m) - (lim seq) < p by Th1;
 n1 <= n1 + n2 by NAT_1:12;
then  n1 <= m by A8, XXREAL_0:2;
then  abs ((seq . m) - (lim seq)) < p by A6;
then A10: - p < (seq . m) - (lim seq) by Th1;
 seq . m <= seq1 . m by A3;
then  (seq . m) - (lim seq) <= (seq1 . m) - (lim seq) by XREAL_1:9;
then A11: - p < (seq1 . m) - (lim seq) by A10, XXREAL_0:2;
 seq1 . m <= seq9 . m by A3;
then  (seq1 . m) - (lim seq) <= (seq9 . m) - (lim seq) by XREAL_1:9;
then  (seq1 . m) - (lim seq) < p by A9, XXREAL_0:2;
hence  abs ((seq1 . m) - (lim seq)) < p by A11, Th1; ::_thesis: verum
end;

theorem :: SEQ_2:20
for seq, seq9, seq1 being Real_Sequence st seq is convergent & seq9 is convergent & ( for n being Element of NAT holds
( seq . n <= seq1 . n & seq1 . n <= seq9 . n ) ) & lim seq = lim seq9 holds
lim seq1 = lim seq
proof
let seq, seq9, seq1 be Real_Sequence; ::_thesis: ( seq is convergent & seq9 is convergent & ( for n being Element of NAT holds
( seq . n <= seq1 . n & seq1 . n <= seq9 . n ) ) & lim seq = lim seq9 implies lim seq1 = lim seq )
assume that
A1: seq is convergent and
A2: seq9 is convergent and
A3: for n being Element of NAT holds
( seq . n <= seq1 . n & seq1 . n <= seq9 . n ) and
A4: lim seq = lim seq9 ; ::_thesis: lim seq1 = lim seq
A5: seq1 is convergent by A1, A2, A3, A4, Th19;
now__::_thesis:_for_p_being_real_number_st_0_<_p_holds_
ex_n_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_n_<=_m_holds_
abs_((seq1_._m)_-_(lim_seq))_<_p
let p be real number ; ::_thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq1 . m) - (lim seq)) < p )
assume A6: 0 < p ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq1 . m) - (lim seq)) < p
then consider n1 being Element of NAT  such that
A7: for m being Element of NAT st n1 <= m holds
abs ((seq . m) - (lim seq)) < p by A1, Def7;
consider n2 being Element of NAT  such that
A8: for m being Element of NAT st n2 <= m holds
abs ((seq9 . m) - (lim seq)) < p by A2, A4, A6, Def7;
take n = n1 + n2; ::_thesis: for m being Element of NAT st n <= m holds
abs ((seq1 . m) - (lim seq)) < p
let m be Element of NAT ; ::_thesis: ( n <= m implies abs ((seq1 . m) - (lim seq)) < p )
assume A9: n <= m ; ::_thesis: abs ((seq1 . m) - (lim seq)) < p
 n2 <= n by NAT_1:12;
then  n2 <= m by A9, XXREAL_0:2;
then  abs ((seq9 . m) - (lim seq)) < p by A8;
then A10: (seq9 . m) - (lim seq) < p by Th1;
 n1 <= n1 + n2 by NAT_1:12;
then  n1 <= m by A9, XXREAL_0:2;
then  abs ((seq . m) - (lim seq)) < p by A7;
then A11: - p < (seq . m) - (lim seq) by Th1;
 seq . m <= seq1 . m by A3;
then  (seq . m) - (lim seq) <= (seq1 . m) - (lim seq) by XREAL_1:9;
then A12: - p < (seq1 . m) - (lim seq) by A11, XXREAL_0:2;
 seq1 . m <= seq9 . m by A3;
then  (seq1 . m) - (lim seq) <= (seq9 . m) - (lim seq) by XREAL_1:9;
then  (seq1 . m) - (lim seq) < p by A10, XXREAL_0:2;
hence  abs ((seq1 . m) - (lim seq)) < p by A12, Th1; ::_thesis: verum
end;
hence  lim seq1 = lim seq by A5, Def7; ::_thesis: verum
end;

theorem Th21: :: SEQ_2:21
for seq being Real_Sequence st seq is convergent & lim seq <> 0 & seq is non-zero holds
seq " is convergent
proof
let seq be Real_Sequence; ::_thesis: ( seq is convergent & lim seq <> 0 & seq is non-zero implies seq " is convergent )
assume that
A1: seq is convergent and
A2: lim seq <> 0 and
A3: seq is non-zero ; ::_thesis: seq " is convergent
A4: 0 < abs (lim seq) by A2, COMPLEX1:47;
A5: 0 <> abs (lim seq) by A2, COMPLEX1:47;
consider n1 being Element of NAT  such that
A6: for m being Element of NAT st n1 <= m holds
(abs (lim seq)) / 2 < abs (seq . m) by A1, A2, Th16;
 0 * 0 < (abs (lim seq)) * (abs (lim seq)) by A4;
then A7: 0 < ((abs (lim seq)) * (abs (lim seq))) / 2 ;
take  (lim seq) " ; :: according to SEQ_2:def_6 ::_thesis: for p being real number st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((seq ") . m) - ((lim seq) ")) < p
let p be real number ; ::_thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((seq ") . m) - ((lim seq) ")) < p )
assume A8: 0 < p ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((seq ") . m) - ((lim seq) ")) < p
then  0 * 0 < p * (((abs (lim seq)) * (abs (lim seq))) / 2) by A7;
then consider n2 being Element of NAT  such that
A9: for m being Element of NAT st n2 <= m holds
abs ((seq . m) - (lim seq)) < p * (((abs (lim seq)) * (abs (lim seq))) / 2) by A1, Def7;
take n = n1 + n2; ::_thesis: for m being Element of NAT st n <= m holds
abs (((seq ") . m) - ((lim seq) ")) < p
let m be Element of NAT ; ::_thesis: ( n <= m implies abs (((seq ") . m) - ((lim seq) ")) < p )
assume A10: n <= m ; ::_thesis: abs (((seq ") . m) - ((lim seq) ")) < p
 n2 <= n by NAT_1:12;
then  n2 <= m by A10, XXREAL_0:2;
then A11: abs ((seq . m) - (lim seq)) < p * (((abs (lim seq)) * (abs (lim seq))) / 2) by A9;
 n1 <= n1 + n2 by NAT_1:12;
then  n1 <= m by A10, XXREAL_0:2;
then A12: (abs (lim seq)) / 2 < abs (seq . m) by A6;
A13: seq . m <> 0 by A3, SEQ_1:5;
then  (seq . m) * (lim seq) <> 0 by A2;
then  0 < abs ((seq . m) * (lim seq)) by COMPLEX1:47;
then  0 < (abs (seq . m)) * (abs (lim seq)) by COMPLEX1:65;
then A14: (abs ((seq . m) - (lim seq))) / ((abs (seq . m)) * (abs (lim seq))) < (p * (((abs (lim seq)) * (abs (lim seq))) / 2)) / ((abs (seq . m)) * (abs (lim seq))) by A11, XREAL_1:74;
A15: (p * (((abs (lim seq)) * (abs (lim seq))) / 2)) / ((abs (seq . m)) * (abs (lim seq))) = (p * ((2 ") * ((abs (lim seq)) * (abs (lim seq))))) * (((abs (seq . m)) * (abs (lim seq))) ") by XCMPLX_0:def_9
.= (p * (2 ")) * (((abs (lim seq)) * (abs (lim seq))) * (((abs (lim seq)) * (abs (seq . m))) "))
.= (p * (2 ")) * (((abs (lim seq)) * (abs (lim seq))) * (((abs (lim seq)) ") * ((abs (seq . m)) "))) by XCMPLX_1:204
.= (p * (2 ")) * (((abs (lim seq)) * ((abs (lim seq)) * ((abs (lim seq)) "))) * ((abs (seq . m)) "))
.= (p * (2 ")) * (((abs (lim seq)) * 1) * ((abs (seq . m)) ")) by A5, XCMPLX_0:def_7
.= (p * ((abs (lim seq)) / 2)) * ((abs (seq . m)) ")
.= (p * ((abs (lim seq)) / 2)) / (abs (seq . m)) by XCMPLX_0:def_9 ;
A16: abs (((seq ") . m) - ((lim seq) ")) = abs (((seq . m) ") - ((lim seq) ")) by VALUED_1:10
.= (abs ((seq . m) - (lim seq))) / ((abs (seq . m)) * (abs (lim seq))) by A2, A13, Th2 ;
A17: 0 < (abs (lim seq)) / 2 by A4;
A18: 0 <> (abs (lim seq)) / 2 by A2, COMPLEX1:47;
 0 * 0 < p * ((abs (lim seq)) / 2) by A8, A17;
then A19: (p * ((abs (lim seq)) / 2)) / (abs (seq . m)) < (p * ((abs (lim seq)) / 2)) / ((abs (lim seq)) / 2) by A12, A17, XREAL_1:76;
(p * ((abs (lim seq)) / 2)) / ((abs (lim seq)) / 2) = (p * ((abs (lim seq)) / 2)) * (((abs (lim seq)) / 2) ") by XCMPLX_0:def_9
.= p * (((abs (lim seq)) / 2) * (((abs (lim seq)) / 2) "))
.= p * 1 by A18, XCMPLX_0:def_7
.= p ;
hence  abs (((seq ") . m) - ((lim seq) ")) < p by A14, A15, A16, A19, XXREAL_0:2; ::_thesis: verum
end;

theorem Th22: :: SEQ_2:22
for seq being Real_Sequence st seq is convergent & lim seq <> 0 & seq is non-zero holds
lim (seq ") = (lim seq) "
proof
let seq be Real_Sequence; ::_thesis: ( seq is convergent & lim seq <> 0 & seq is non-zero implies lim (seq ") = (lim seq) " )
assume that
A1: seq is convergent and
A2: lim seq <> 0 and
A3: seq is non-zero ; ::_thesis: lim (seq ") = (lim seq) "
A4: seq " is convergent by A1, A2, A3, Th21;
A5: 0 < abs (lim seq) by A2, COMPLEX1:47;
A6: 0 <> abs (lim seq) by A2, COMPLEX1:47;
consider n1 being Element of NAT  such that
A7: for m being Element of NAT st n1 <= m holds
(abs (lim seq)) / 2 < abs (seq . m) by A1, A2, Th16;
 0 * 0 < (abs (lim seq)) * (abs (lim seq)) by A5;
then A8: 0 < ((abs (lim seq)) * (abs (lim seq))) / 2 ;
now__::_thesis:_for_p_being_real_number_st_0_<_p_holds_
ex_n_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_n_<=_m_holds_
abs_(((seq_")_._m)_-_((lim_seq)_"))_<_p
let p be real number ; ::_thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((seq ") . m) - ((lim seq) ")) < p )
assume A9: 0 < p ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((seq ") . m) - ((lim seq) ")) < p
then  0 * 0 < p * (((abs (lim seq)) * (abs (lim seq))) / 2) by A8;
then consider n2 being Element of NAT  such that
A10: for m being Element of NAT st n2 <= m holds
abs ((seq . m) - (lim seq)) < p * (((abs (lim seq)) * (abs (lim seq))) / 2) by A1, Def7;
take n = n1 + n2; ::_thesis: for m being Element of NAT st n <= m holds
abs (((seq ") . m) - ((lim seq) ")) < p
let m be Element of NAT ; ::_thesis: ( n <= m implies abs (((seq ") . m) - ((lim seq) ")) < p )
assume A11: n <= m ; ::_thesis: abs (((seq ") . m) - ((lim seq) ")) < p
 n2 <= n by NAT_1:12;
then  n2 <= m by A11, XXREAL_0:2;
then A12: abs ((seq . m) - (lim seq)) < p * (((abs (lim seq)) * (abs (lim seq))) / 2) by A10;
 n1 <= n1 + n2 by NAT_1:12;
then  n1 <= m by A11, XXREAL_0:2;
then A13: (abs (lim seq)) / 2 < abs (seq . m) by A7;
A14: seq . m <> 0 by A3, SEQ_1:5;
then  (seq . m) * (lim seq) <> 0 by A2;
then  0 < abs ((seq . m) * (lim seq)) by COMPLEX1:47;
then  0 < (abs (seq . m)) * (abs (lim seq)) by COMPLEX1:65;
then A15: (abs ((seq . m) - (lim seq))) / ((abs (seq . m)) * (abs (lim seq))) < (p * (((abs (lim seq)) * (abs (lim seq))) / 2)) / ((abs (seq . m)) * (abs (lim seq))) by A12, XREAL_1:74;
A16: (p * (((abs (lim seq)) * (abs (lim seq))) / 2)) / ((abs (seq . m)) * (abs (lim seq))) = (p * ((2 ") * ((abs (lim seq)) * (abs (lim seq))))) * (((abs (seq . m)) * (abs (lim seq))) ") by XCMPLX_0:def_9
.= (p * (2 ")) * (((abs (lim seq)) * (abs (lim seq))) * (((abs (lim seq)) * (abs (seq . m))) "))
.= (p * (2 ")) * (((abs (lim seq)) * (abs (lim seq))) * (((abs (lim seq)) ") * ((abs (seq . m)) "))) by XCMPLX_1:204
.= (p * (2 ")) * (((abs (lim seq)) * ((abs (lim seq)) * ((abs (lim seq)) "))) * ((abs (seq . m)) "))
.= (p * (2 ")) * (((abs (lim seq)) * 1) * ((abs (seq . m)) ")) by A6, XCMPLX_0:def_7
.= (p * ((abs (lim seq)) / 2)) * ((abs (seq . m)) ")
.= (p * ((abs (lim seq)) / 2)) / (abs (seq . m)) by XCMPLX_0:def_9 ;
A17: abs (((seq ") . m) - ((lim seq) ")) = abs (((seq . m) ") - ((lim seq) ")) by VALUED_1:10
.= (abs ((seq . m) - (lim seq))) / ((abs (seq . m)) * (abs (lim seq))) by A2, A14, Th2 ;
A18: 0 < (abs (lim seq)) / 2 by A5;
A19: 0 <> (abs (lim seq)) / 2 by A2, COMPLEX1:47;
 0 * 0 < p * ((abs (lim seq)) / 2) by A9, A18;
then A20: (p * ((abs (lim seq)) / 2)) / (abs (seq . m)) < (p * ((abs (lim seq)) / 2)) / ((abs (lim seq)) / 2) by A13, A18, XREAL_1:76;
(p * ((abs (lim seq)) / 2)) / ((abs (lim seq)) / 2) = (p * ((abs (lim seq)) / 2)) * (((abs (lim seq)) / 2) ") by XCMPLX_0:def_9
.= p * (((abs (lim seq)) / 2) * (((abs (lim seq)) / 2) "))
.= p * 1 by A19, XCMPLX_0:def_7
.= p ;
hence  abs (((seq ") . m) - ((lim seq) ")) < p by A15, A16, A17, A20, XXREAL_0:2; ::_thesis: verum
end;
hence  lim (seq ") = (lim seq) " by A4, Def7; ::_thesis: verum
end;

theorem :: SEQ_2:23
for seq9, seq being Real_Sequence st seq9 is convergent & seq is convergent & lim seq <> 0 & seq is non-zero holds
seq9 /" seq is convergent
proof
let seq9, seq be Real_Sequence; ::_thesis: ( seq9 is convergent & seq is convergent & lim seq <> 0 & seq is non-zero implies seq9 /" seq is convergent )
assume that
A1: seq9 is convergent and
A2: seq is convergent and
A3: lim seq <> 0 and
A4: seq is non-zero ; ::_thesis: seq9 /" seq is convergent
 seq " is convergent by A2, A3, A4, Th21;
hence  seq9 /" seq is convergent by A1; ::_thesis: verum
end;

theorem :: SEQ_2:24
for seq9, seq being Real_Sequence st seq9 is convergent & seq is convergent & lim seq <> 0 & seq is non-zero holds
lim (seq9 /" seq) = (lim seq9) / (lim seq)
proof
let seq9, seq be Real_Sequence; ::_thesis: ( seq9 is convergent & seq is convergent & lim seq <> 0 & seq is non-zero implies lim (seq9 /" seq) = (lim seq9) / (lim seq) )
assume that
A1: seq9 is convergent and
A2: seq is convergent and
A3: lim seq <> 0 and
A4: seq is non-zero ; ::_thesis: lim (seq9 /" seq) = (lim seq9) / (lim seq)
 seq " is convergent by A2, A3, A4, Th21;
then  lim (seq9 (#) (seq ")) = (lim seq9) * (lim (seq ")) by A1, Th15
.= (lim seq9) * ((lim seq) ") by A2, A3, A4, Th22
.= (lim seq9) / (lim seq) by XCMPLX_0:def_9 ;
hence  lim (seq9 /" seq) = (lim seq9) / (lim seq) ; ::_thesis: verum
end;

theorem Th25: :: SEQ_2:25
for seq, seq1 being Real_Sequence st seq is convergent & seq1 is bounded & lim seq = 0 holds
seq (#) seq1 is convergent
proof
let seq, seq1 be Real_Sequence; ::_thesis: ( seq is convergent & seq1 is bounded & lim seq = 0 implies seq (#) seq1 is convergent )
assume that
A1: seq is convergent and
A2: seq1 is bounded and
A3: lim seq = 0 ; ::_thesis: seq (#) seq1 is convergent
reconsider g1 = 0 as Real ;
take g = g1; :: according to SEQ_2:def_6 ::_thesis: for p being real number st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((seq (#) seq1) . m) - g) < p
let p be real number ; ::_thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((seq (#) seq1) . m) - g) < p )
assume A4: 0 < p ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((seq (#) seq1) . m) - g) < p
consider r being real number  such that
A5: 0 < r and
A6: for m being Element of NAT holds abs (seq1 . m) < r by A2, Th3;
A7: 0 < p / r by A4, A5;
then consider n1 being Element of NAT  such that
A8: for m being Element of NAT st n1 <= m holds
abs ((seq . m) - 0) < p / r by A1, A3, Def7;
take n = n1; ::_thesis: for m being Element of NAT st n <= m holds
abs (((seq (#) seq1) . m) - g) < p
let m be Element of NAT ; ::_thesis: ( n <= m implies abs (((seq (#) seq1) . m) - g) < p )
assume A9: n <= m ; ::_thesis: abs (((seq (#) seq1) . m) - g) < p
 abs (seq . m) = abs ((seq . m) - 0) ;
then A10: abs (seq . m) < p / r by A8, A9;
A11: abs (((seq (#) seq1) . m) - g) = abs (((seq . m) * (seq1 . m)) - 0) by SEQ_1:8
.= (abs (seq . m)) * (abs (seq1 . m)) by COMPLEX1:65 ;
now__::_thesis:_(_abs_(seq1_._m)_<>_0_implies_abs_(((seq_(#)_seq1)_._m)_-_g)_<_p_)
assume A12: abs (seq1 . m) <> 0 ; ::_thesis: abs (((seq (#) seq1) . m) - g) < p
(p / r) * r = (p * (r ")) * r by XCMPLX_0:def_9
.= p * ((r ") * r)
.= p * 1 by A5, XCMPLX_0:def_7
.= p ;
then A13: (p / r) * (abs (seq1 . m)) < p by A6, A7, XREAL_1:68;
 0 <= abs (seq1 . m) by COMPLEX1:46;
then  abs (((seq (#) seq1) . m) - g) < (p / r) * (abs (seq1 . m)) by A10, A11, A12, XREAL_1:68;
hence  abs (((seq (#) seq1) . m) - g) < p by A13, XXREAL_0:2; ::_thesis: verum
end;
hence  abs (((seq (#) seq1) . m) - g) < p by A4, A11; ::_thesis: verum
end;

theorem :: SEQ_2:26
for seq, seq1 being Real_Sequence st seq is convergent & seq1 is bounded & lim seq = 0 holds
lim (seq (#) seq1) = 0
proof
let seq, seq1 be Real_Sequence; ::_thesis: ( seq is convergent & seq1 is bounded & lim seq = 0 implies lim (seq (#) seq1) = 0 )
assume that
A1: seq is convergent and
A2: seq1 is bounded and
A3: lim seq = 0 ; ::_thesis: lim (seq (#) seq1) = 0
A4: seq (#) seq1 is convergent by A1, A2, A3, Th25;
now__::_thesis:_for_p_being_real_number_st_0_<_p_holds_
ex_n_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_n_<=_m_holds_
abs_(((seq_(#)_seq1)_._m)_-_0)_<_p
let p be real number ; ::_thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((seq (#) seq1) . m) - 0) < p )
assume A5: 0 < p ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((seq (#) seq1) . m) - 0) < p
consider r being real number  such that
A6: 0 < r and
A7: for m being Element of NAT holds abs (seq1 . m) < r by A2, Th3;
A8: 0 < p / r by A5, A6;
then consider n1 being Element of NAT  such that
A9: for m being Element of NAT st n1 <= m holds
abs ((seq . m) - 0) < p / r by A1, A3, Def7;
take n = n1; ::_thesis: for m being Element of NAT st n <= m holds
abs (((seq (#) seq1) . m) - 0) < p
let m be Element of NAT ; ::_thesis: ( n <= m implies abs (((seq (#) seq1) . m) - 0) < p )
assume  n <= m ; ::_thesis: abs (((seq (#) seq1) . m) - 0) < p
then A10: abs ((seq . m) - 0) < p / r by A9;
A11: abs (((seq (#) seq1) . m) - 0) = abs (((seq . m) * (seq1 . m)) - 0) by SEQ_1:8
.= (abs (seq . m)) * (abs (seq1 . m)) by COMPLEX1:65 ;
now__::_thesis:_(_abs_(seq1_._m)_<>_0_implies_abs_(((seq_(#)_seq1)_._m)_-_0)_<_p_)
assume A12: abs (seq1 . m) <> 0 ; ::_thesis: abs (((seq (#) seq1) . m) - 0) < p
(p / r) * r = (p * (r ")) * r by XCMPLX_0:def_9
.= p * ((r ") * r)
.= p * 1 by A6, XCMPLX_0:def_7 ;
then A13: (p / r) * (abs (seq1 . m)) < p by A7, A8, XREAL_1:68;
 0 <= abs (seq1 . m) by COMPLEX1:46;
then  abs (((seq (#) seq1) . m) - 0) < (p / r) * (abs (seq1 . m)) by A10, A11, A12, XREAL_1:68;
hence  abs (((seq (#) seq1) . m) - 0) < p by A13, XXREAL_0:2; ::_thesis: verum
end;
hence  abs (((seq (#) seq1) . m) - 0) < p by A5, A11; ::_thesis: verum
end;
hence  lim (seq (#) seq1) = 0 by A4, Def7; ::_thesis: verum
end;

registration
let s be convergent Complex_Sequence;
cluster|.s.| ->  convergent for Real_Sequence;
coherence
 for b1 being Real_Sequence st b1 = |.s.| holds
b1 is convergent
proof
 |.s.| is convergent
proof
consider g being Element of COMPLEX  such that
A1: for p being Real st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((s . m) - g).| < p by COMSEQ_2:def_5;
take  |.g.| ; :: according to SEQ_2:def_6 ::_thesis: for p being real number st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((|.s.| . m) - |.g.|) < p
let p be real number ; ::_thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((|.s.| . m) - |.g.|) < p )
assume A2: 0 < p ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((|.s.| . m) - |.g.|) < p
 p is Real by XREAL_0:def_1;
then consider n being Element of NAT  such that
A3: for m being Element of NAT st n <= m holds
|.((s . m) - g).| < p by A1, A2;
take  n ; ::_thesis: for m being Element of NAT st n <= m holds
abs ((|.s.| . m) - |.g.|) < p
let m be Element of NAT ; ::_thesis: ( n <= m implies abs ((|.s.| . m) - |.g.|) < p )
assume  n <= m ; ::_thesis: abs ((|.s.| . m) - |.g.|) < p
then  |.((s . m) - g).| < p by A3;
then  (abs (|.(s . m).| - |.g.|)) + |.((s . m) - g).| < p + |.((s . m) - g).| by COMPLEX1:64, XREAL_1:8;
then  ((abs (|.(s . m).| - |.g.|)) + |.((s . m) - g).|) - |.((s . m) - g).| < (p + |.((s . m) - g).|) - |.((s . m) - g).| by XREAL_1:9;
hence  abs ((|.s.| . m) - |.g.|) < p by VALUED_1:18; ::_thesis: verum
end;
hence  for b1 being Real_Sequence st b1 = |.s.| holds
b1 is convergent ; ::_thesis: verum
end;
end;


theorem Th27: :: SEQ_2:27
for s being Complex_Sequence st s is convergent holds
lim |.s.| = |.(lim s).|
proof
let s be Complex_Sequence; ::_thesis: ( s is convergent implies lim |.s.| = |.(lim s).| )
set g = lim s;
assume A1: s is convergent ; ::_thesis: lim |.s.| = |.(lim s).|
then reconsider s1 = s as convergent Complex_Sequence ;
reconsider w = |.s1.| as Real_Sequence ;
A2: w is convergent ;
reconsider w = |.(lim s).| as Real ;
now__::_thesis:_for_p_being_real_number_st_0_<_p_holds_
ex_n_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_n_<=_m_holds_
abs_((|.s.|_._m)_-_w)_<_p
let p be real number ; ::_thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((|.s.| . m) - w) < p )
assume A3: 0 < p ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((|.s.| . m) - w) < p
 p is Real by XREAL_0:def_1;
then consider n being Element of NAT  such that
A4: for m being Element of NAT st n <= m holds
|.((s . m) - (lim s)).| < p by A1, A3, COMSEQ_2:def_6;
take n = n; ::_thesis: for m being Element of NAT st n <= m holds
abs ((|.s.| . m) - w) < p
let m be Element of NAT ; ::_thesis: ( n <= m implies abs ((|.s.| . m) - w) < p )
assume  n <= m ; ::_thesis: abs ((|.s.| . m) - w) < p
then  |.((s . m) - (lim s)).| < p by A4;
then  (abs (|.(s . m).| - |.(lim s).|)) + |.((s . m) - (lim s)).| < p + |.((s . m) - (lim s)).| by COMPLEX1:64, XREAL_1:8;
then  ((abs (|.(s . m).| - |.(lim s).|)) + |.((s . m) - (lim s)).|) - |.((s . m) - (lim s)).| < (p + |.((s . m) - (lim s)).|) - |.((s . m) - (lim s)).| by XREAL_1:9;
hence  abs ((|.s.| . m) - w) < p by VALUED_1:18; ::_thesis: verum
end;
hence  lim |.s.| = |.(lim s).| by A2, Def7; ::_thesis: verum
end;

theorem :: SEQ_2:28
for s, s9 being convergent Complex_Sequence holds lim |.(s + s9).| = |.((lim s) + (lim s9)).|
proof
let s, s9 be convergent Complex_Sequence; ::_thesis: lim |.(s + s9).| = |.((lim s) + (lim s9)).|
thus  lim |.(s + s9).| = |.(lim (s + s9)).| by Th27
.= |.((lim s) + (lim s9)).| by COMSEQ_2:14 ; ::_thesis: verum
end;

theorem :: SEQ_2:29
for r being real number
for s being convergent Complex_Sequence holds lim |.(r (#) s).| = |.r.| * |.(lim s).|
proof
let r be real number ; ::_thesis: for s being convergent Complex_Sequence holds lim |.(r (#) s).| = |.r.| * |.(lim s).|
let s be convergent Complex_Sequence; ::_thesis: lim |.(r (#) s).| = |.r.| * |.(lim s).|
thus  lim |.(r (#) s).| = |.(lim (r (#) s)).| by Th27
.= |.(r * (lim s)).| by COMSEQ_2:18
.= |.r.| * |.(lim s).| by COMPLEX1:65 ; ::_thesis: verum
end;

theorem :: SEQ_2:30
for s being convergent Complex_Sequence holds lim |.(- s).| = |.(lim s).|
proof
let s be convergent Complex_Sequence; ::_thesis: lim |.(- s).| = |.(lim s).|
thus  lim |.(- s).| = |.(lim (- s)).| by Th27
.= |.(- (lim s)).| by COMSEQ_2:22
.= |.(lim s).| by COMPLEX1:52 ; ::_thesis: verum
end;

theorem :: SEQ_2:31
for s, s9 being convergent Complex_Sequence holds lim |.(s - s9).| = |.((lim s) - (lim s9)).|
proof
let s, s9 be convergent Complex_Sequence; ::_thesis: lim |.(s - s9).| = |.((lim s) - (lim s9)).|
thus  lim |.(s - s9).| = |.(lim (s - s9)).| by Th27
.= |.((lim s) - (lim s9)).| by COMSEQ_2:26 ; ::_thesis: verum
end;

theorem :: SEQ_2:32
for s, s9 being convergent Complex_Sequence holds lim |.(s (#) s9).| = |.(lim s).| * |.(lim s9).|
proof
let s, s9 be convergent Complex_Sequence; ::_thesis: lim |.(s (#) s9).| = |.(lim s).| * |.(lim s9).|
thus  lim |.(s (#) s9).| = |.(lim (s (#) s9)).| by Th27
.= |.((lim s) * (lim s9)).| by COMSEQ_2:30
.= |.(lim s).| * |.(lim s9).| by COMPLEX1:65 ; ::_thesis: verum
end;

theorem :: SEQ_2:33
for s being Complex_Sequence st s is convergent & lim s <> 0c & s is non-zero holds
lim |.(s ").| = |.(lim s).| "
proof
let s be Complex_Sequence; ::_thesis: ( s is convergent & lim s <> 0c & s is non-zero implies lim |.(s ").| = |.(lim s).| " )
assume A1: ( s is convergent & lim s <> 0c & s is non-zero ) ; ::_thesis: lim |.(s ").| = |.(lim s).| "
then  s " is convergent by COMSEQ_2:34;
hence  lim |.(s ").| = |.(lim (s ")).| by Th27
.= |.((lim s) ").| by A1, COMSEQ_2:35
.= |.(lim s).| " by COMPLEX1:66 ;
::_thesis: verum
end;

theorem :: SEQ_2:34
for s9, s being Complex_Sequence st s9 is convergent & s is convergent & lim s <> 0c & s is non-zero holds
lim |.(s9 /" s).| = |.(lim s9).| / |.(lim s).|
proof
let s9, s be Complex_Sequence; ::_thesis: ( s9 is convergent & s is convergent & lim s <> 0c & s is non-zero implies lim |.(s9 /" s).| = |.(lim s9).| / |.(lim s).| )
assume A1: ( s9 is convergent & s is convergent & lim s <> 0c & s is non-zero ) ; ::_thesis: lim |.(s9 /" s).| = |.(lim s9).| / |.(lim s).|
then  s9 /" s is convergent by COMSEQ_2:38;
hence  lim |.(s9 /" s).| = |.(lim (s9 /" s)).| by Th27
.= |.((lim s9) / (lim s)).| by A1, COMSEQ_2:39
.= |.(lim s9).| / |.(lim s).| by COMPLEX1:67 ;
::_thesis: verum
end;

theorem :: SEQ_2:35
for s, s1 being Complex_Sequence st s is convergent & s1 is bounded & lim s = 0c holds
lim |.(s (#) s1).| = 0
proof
let s, s1 be Complex_Sequence; ::_thesis: ( s is convergent & s1 is bounded & lim s = 0c implies lim |.(s (#) s1).| = 0 )
assume A1: ( s is convergent & s1 is bounded & lim s = 0c ) ; ::_thesis: lim |.(s (#) s1).| = 0
then  s (#) s1 is convergent by COMSEQ_2:42;
hence  lim |.(s (#) s1).| = |.(lim (s (#) s1)).| by Th27
.= 0 by A1, COMSEQ_2:43, COMPLEX1:44 ;
::_thesis: verum
end;