:: COMSEQ_2 semantic presentation

begin


theorem Th1: :: COMSEQ_2:1
for g, r being Element of COMPLEX st g <> 0c & r <> 0c holds
|.((g ") - (r ")).| = |.(g - r).| / (|.g.| * |.r.|)
proof
let g, r be Element of COMPLEX ; ::_thesis: ( g <> 0c & r <> 0c implies |.((g ") - (r ")).| = |.(g - r).| / (|.g.| * |.r.|) )
assume A1: ( g <> 0c & r <> 0c ) ; ::_thesis: |.((g ") - (r ")).| = |.(g - r).| / (|.g.| * |.r.|)
thus |.((g ") - (r ")).| = |.((1r / g) - (r ")).| by COMPLEX1:def_4, XCMPLX_1:215
.= |.((1r / g) - (1r / r)).| by COMPLEX1:def_4, XCMPLX_1:215
.= |.((1r / g) + (- (1r / r))).|
.= |.((1r / g) + (- (1r * (r ")))).| by XCMPLX_0:def_9
.= |.((1r / g) + ((- 1r) * (r "))).|
.= |.((1r / g) + ((- 1r) / r)).| by XCMPLX_0:def_9
.= |.(((1r * r) + ((- 1r) * g)) / (r * g)).| by A1, XCMPLX_1:116
.= |.(r - g).| / |.(g * r).| by COMPLEX1:67, COMPLEX1:def_4
.= |.(- (g - r)).| / (|.g.| * |.r.|) by COMPLEX1:65
.= |.(g - r).| / (|.g.| * |.r.|) by COMPLEX1:52 ; ::_thesis: verum
end;

theorem Th2: :: COMSEQ_2:2
for s being Complex_Sequence
for n being Element of NAT ex r being Real st
( 0 < r & ( for m being Element of NAT st m <= n holds
|.(s . m).| < r ) )
proof
let s be Complex_Sequence; ::_thesis: for n being Element of NAT ex r being Real st
( 0 < r & ( for m being Element of NAT st m <= n holds
|.(s . m).| < r ) )
let n be Element of NAT ; ::_thesis: ex r being Real st
( 0 < r & ( for m being Element of NAT st m <= n holds
|.(s . m).| < r ) )
defpred S1[ Element of NAT ] means  ex r being real number st
( 0 < r & ( for m being Element of NAT st m <= $1 holds
|.(s . m).| < r ) );
A1: 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 A2: 0 < R1 and
A3: for m being Element of NAT st m <= n holds
|.(s . m).| < R1 ; ::_thesis: S1[n + 1]
A4: now__::_thesis:_(_R1_<=_|.(s_._(n_+_1)).|_implies_ex_R_being_Element_of_REAL_st_
(_0_<_R_&_(_for_m_being_Element_of_NAT_st_m_<=_n_+_1_holds_
|.(s_._m).|_<_R_)_)_)
assume A5: R1 <= |.(s . (n + 1)).| ; ::_thesis: ex R being Element of REAL st
( 0 < R & ( for m being Element of NAT st m <= n + 1 holds
|.(s . m).| < R ) )
take R = |.(s . (n + 1)).| + 1; ::_thesis: ( 0 < R & ( for m being Element of NAT st m <= n + 1 holds
|.(s . 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
|.(s . m).| < R
let m be Element of NAT ; ::_thesis: ( m <= n + 1 implies |.(s . m).| < R )
assume A6: m <= n + 1 ; ::_thesis: |.(s . m).| < R
A7: now__::_thesis:_(_m_<=_n_implies_|.(s_._m).|_<_R_)
assume  m <= n ; ::_thesis: |.(s . m).| < R
then  |.(s . m).| < R1 by A3;
then  |.(s . m).| < |.(s . (n + 1)).| by A5, XXREAL_0:2;
then  |.(s . m).| + 0 < R by XREAL_1:8;
hence  |.(s . m).| < R ; ::_thesis: verum
end;
now__::_thesis:_(_m_=_n_+_1_implies_|.(s_._m).|_<_R_)
assume  m = n + 1 ; ::_thesis: |.(s . m).| < R
then  |.(s . m).| + 0 < R by XREAL_1:8;
hence  |.(s . m).| < R ; ::_thesis: verum
end;
hence  |.(s . m).| < R by A6, A7, NAT_1:8; ::_thesis: verum
end;
now__::_thesis:_(_|.(s_._(n_+_1)).|_<=_R1_implies_ex_R_being_Element_of_REAL_st_
(_R_>_0_&_(_for_m_being_Element_of_NAT_st_m_<=_n_+_1_holds_
|.(s_._m).|_<_R_)_)_)
assume A8: |.(s . (n + 1)).| <= R1 ; ::_thesis: ex R being Element of REAL st
( R > 0 & ( for m being Element of NAT st m <= n + 1 holds
|.(s . m).| < R ) )
take R = R1 + 1; ::_thesis: ( R > 0 & ( for m being Element of NAT st m <= n + 1 holds
|.(s . m).| < R ) )
thus  R > 0 by A2; ::_thesis: for m being Element of NAT st m <= n + 1 holds
|.(s . m).| < R
let m be Element of NAT ; ::_thesis: ( m <= n + 1 implies |.(s . m).| < R )
assume A9: m <= n + 1 ; ::_thesis: |.(s . m).| < R
A10: now__::_thesis:_(_m_<=_n_implies_|.(s_._m).|_<_R_)
assume  m <= n ; ::_thesis: |.(s . m).| < R
then A11: |.(s . m).| < R1 by A3;
 R1 + 0 < R by XREAL_1:8;
hence  |.(s . m).| < R by A11, XXREAL_0:2; ::_thesis: verum
end;
now__::_thesis:_(_m_=_n_+_1_implies_|.(s_._m).|_<_R_)
A12: R1 + 0 < R by XREAL_1:8;
assume  m = n + 1 ; ::_thesis: |.(s . m).| < R
hence  |.(s . m).| < R by A8, A12, XXREAL_0:2; ::_thesis: verum
end;
hence  |.(s . m).| < R by A9, A10, NAT_1:8; ::_thesis: verum
end;
hence  S1[n + 1] by A4; ::_thesis: verum
end;
A13: S1[ 0 ]
proof
take R = |.(s . 0).| + 1; ::_thesis: ( 0 < R & ( for m being Element of NAT st m <= 0 holds
|.(s . m).| < R ) )
 0 + 0 < |.(s . 0).| + 1 by COMPLEX1:46, XREAL_1:8;
hence  0 < R ; ::_thesis: for m being Element of NAT st m <= 0 holds
|.(s . m).| < R
let m be Element of NAT ; ::_thesis: ( m <= 0 implies |.(s . m).| < R )
assume  m <= 0 ; ::_thesis: |.(s . m).| < R
then  m = 0 by NAT_1:2;
then  |.(s . m).| + 0 < R by XREAL_1:8;
hence  |.(s . m).| < R ; ::_thesis: verum
end;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A13, A1);
then consider R being real number  such that
A14: ( R > 0 & ( for m being Element of NAT st m <= n holds
|.(s . m).| < R ) ) ;
 R is Real by XREAL_0:def_1;
hence  ex r being Real st
( 0 < r & ( for m being Element of NAT st m <= n holds
|.(s . m).| < r ) ) by A14; ::_thesis: verum
end;

begin

definition
let f be complex-valued Function;
deffunc H1( set ) ->  Element of COMPLEX = (f . $1) *' ;
funcf *'  ->  complex-valued Function means :Def1: :: COMSEQ_2:def 1
( dom it = dom f & ( for c being set st c in dom it holds
it . c = (f . c) *' ) );
existence
 ex b1 being complex-valued Function st
( dom b1 = dom f & ( for c being set st c in dom b1 holds
b1 . c = (f . c) *' ) )
proof
consider F being Function such that
A1: dom F = dom f and
A2: for x being set st x in dom f holds
F . x = H1(x) from FUNCT_1:sch_3();
 for x being set st x in dom F holds
F . x is complex
proof
let x be set ; ::_thesis: ( x in dom F implies F . x is complex )
assume  x in dom F ; ::_thesis: F . x is complex
then  F . x = H1(x) by A1, A2;
hence  F . x is complex ; ::_thesis: verum
end;
then reconsider F = F as complex-valued Function by VALUED_0:def_7;
take  F ; ::_thesis: ( dom F = dom f & ( for c being set st c in dom F holds
F . c = (f . c) *' ) )
thus  dom f = dom F by A1; ::_thesis: for c being set st c in dom F holds
F . c = (f . c) *'
thus  for c being set st c in dom F holds
F . c = (f . c) *' by A1, A2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being complex-valued Function st dom b1 = dom f & ( for c being set st c in dom b1 holds
b1 . c = (f . c) *' ) & dom b2 = dom f & ( for c being set st c in dom b2 holds
b2 . c = (f . c) *' ) holds
b1 = b2
proof
let h, g be complex-valued Function; ::_thesis: ( dom h = dom f & ( for c being set st c in dom h holds
h . c = (f . c) *' ) & dom g = dom f & ( for c being set st c in dom g holds
g . c = (f . c) *' ) implies h = g )
assume that
A3: dom h = dom f and
A4: for c being set st c in dom h holds
h . c = H1(c) and
A5: dom g = dom f and
A6: for c being set st c in dom g holds
g . c = H1(c) ; ::_thesis: h = g
thus  dom h = dom g by A3, A5; :: according to FUNCT_1:def_11 ::_thesis: for b1 being set holds
( not b1 in dom h or h . b1 = g . b1 )
let x be set ; ::_thesis: ( not x in dom h or h . x = g . x )
assume A7: x in dom h ; ::_thesis: h . x = g . x
hence h . x = H1(x) by A4
.= g . x by A3, A5, A6, A7 ;
::_thesis: verum
end;
involutiveness
 for b1, b2 being complex-valued Function st dom b1 = dom b2 & ( for c being set st c in dom b1 holds
b1 . c = (b2 . c) *' ) holds
( dom b2 = dom b1 & ( for c being set st c in dom b2 holds
b2 . c = (b1 . c) *' ) )
proof
let g, f be complex-valued Function; ::_thesis: ( dom g = dom f & ( for c being set st c in dom g holds
g . c = (f . c) *' ) implies ( dom f = dom g & ( for c being set st c in dom f holds
f . c = (g . c) *' ) ) )
assume that
A8: dom g = dom f and
A9: for c being set st c in dom g holds
g . c = (f . c) *' ; ::_thesis: ( dom f = dom g & ( for c being set st c in dom f holds
f . c = (g . c) *' ) )
thus  dom f = dom g by A8; ::_thesis: for c being set st c in dom f holds
f . c = (g . c) *'
let c be set ; ::_thesis: ( c in dom f implies f . c = (g . c) *' )
assume A10: c in dom f ; ::_thesis: f . c = (g . c) *'
thus f . c = ((f . c) *') *'
.= (g . c) *' by A8, A10, A9 ; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines *' COMSEQ_2:def_1_:_
 for f, b2 being complex-valued Function holds
( b2 = f *' iff ( dom b2 = dom f & ( for c being set st c in dom b2 holds
b2 . c = (f . c) *' ) ) );

definition
let C be non empty set ;
let f be Function of C,COMPLEX;
:: original: *'
redefine funcf *'  ->  Function of C,COMPLEX means :Def2: :: COMSEQ_2:def 2
( dom it = C & ( for n being Element of C holds it . n = (f . n) *' ) );
coherence
 f *' is Function of C,COMPLEX
proof
A1: dom (f *') = dom f by Def1
.= C by PARTFUN1:def_2 ;
 for x being set st x in C holds
(f *') . x in COMPLEX by XCMPLX_0:def_2;
hence  f *' is Function of C,COMPLEX by A1, FUNCT_2:3; ::_thesis: verum
end;
compatibility
 for b1 being Function of C,COMPLEX holds
( b1 = f *' iff ( dom b1 = C & ( for n being Element of C holds b1 . n = (f . n) *' ) ) )
proof
let IT be Function of C,COMPLEX; ::_thesis: ( IT = f *' iff ( dom IT = C & ( for n being Element of C holds IT . n = (f . n) *' ) ) )
thus  ( IT = f *' implies ( dom IT = C & ( for c being Element of C holds IT . c = (f . c) *' ) ) ) ::_thesis: ( dom IT = C & ( for n being Element of C holds IT . n = (f . n) *' ) implies IT = f *' )
proof
assume A2: IT = f *' ; ::_thesis: ( dom IT = C & ( for c being Element of C holds IT . c = (f . c) *' ) )
thus A3: dom IT = C by FUNCT_2:def_1; ::_thesis: for c being Element of C holds IT . c = (f . c) *'
let c be Element of C; ::_thesis: IT . c = (f . c) *'
thus  IT . c = (f . c) *' by A2, A3, Def1; ::_thesis: verum
end;
assume that
A4: dom IT = C and
A5: for c being Element of C holds IT . c = (f . c) *' ; ::_thesis: IT = f *'
A6: dom IT = dom f by A4, FUNCT_2:def_1;
 for c being set st c in dom IT holds
IT . c = (f . c) *' by A5;
hence  IT = f *' by A6, Def1; ::_thesis: verum
end;
end;

:: deftheorem Def2 defines *' COMSEQ_2:def_2_:_
 for C being non empty set
for f, b3 being Function of C,COMPLEX holds
( b3 = f *' iff ( dom b3 = C & ( for n being Element of C holds b3 . n = (f . n) *' ) ) );

registration
let C be non empty set ;
let s be complex-valued ManySortedSet of C;
clusters *'  -> C -defined complex-valued ;
coherence
 s *' is C -defined
proof
 dom s c= C ;
hence  dom (s *') c= C by Def1; :: according to RELAT_1:def_18 ::_thesis: verum
end;
end;

registration
let C be non empty set ;
let seq be complex-valued ManySortedSet of C;
clusterseq *'  -> C -defined total for C -defined Function;
coherence
 for b1 being C -defined Function st b1 = seq *' holds
b1 is total
proof
let f be C -defined Function; ::_thesis: ( f = seq *' implies f is total )
assume A1: f = seq *' ; ::_thesis: f is total
thus  dom f = dom seq by Def1, A1
.= C by PARTFUN1:def_2 ; :: according to PARTFUN1:def_2 ::_thesis: verum
end;
end;

theorem :: COMSEQ_2:3
for s being Complex_Sequence st s is non-zero holds
s *' is non-zero
proof
let s be Complex_Sequence; ::_thesis: ( s is non-zero implies s *' is non-zero )
assume A1: s is non-zero ; ::_thesis: s *' is non-zero
now__::_thesis:_for_n_being_Element_of_NAT_holds_(s_*')_._n_<>_0c
let n be Element of NAT ; ::_thesis: (s *') . n <> 0c
 (s . n) *' <> 0c by A1, COMPLEX1:29;
hence  (s *') . n <> 0c by Def2; ::_thesis: verum
end;
hence  s *' is non-zero by COMSEQ_1:4; ::_thesis: verum
end;

theorem :: COMSEQ_2:4
for r being Element of COMPLEX
for s being Complex_Sequence holds (r (#) s) *' = (r *') (#) (s *')
proof
let r be Element of COMPLEX ; ::_thesis: for s being Complex_Sequence holds (r (#) s) *' = (r *') (#) (s *')
let s be Complex_Sequence; ::_thesis: (r (#) s) *' = (r *') (#) (s *')
now__::_thesis:_for_n_being_Element_of_NAT_holds_((r_(#)_s)_*')_._n_=_((r_*')_(#)_(s_*'))_._n
let n be Element of NAT ; ::_thesis: ((r (#) s) *') . n = ((r *') (#) (s *')) . n
thus ((r (#) s) *') . n = ((r (#) s) . n) *' by Def2
.= (r * (s . n)) *' by VALUED_1:6
.= (r *') * ((s . n) *') by COMPLEX1:35
.= (r *') * ((s *') . n) by Def2
.= ((r *') (#) (s *')) . n by VALUED_1:6 ; ::_thesis: verum
end;
hence  (r (#) s) *' = (r *') (#) (s *') by FUNCT_2:63; ::_thesis: verum
end;

theorem :: COMSEQ_2:5
for s, s9 being Complex_Sequence holds (s (#) s9) *' = (s *') (#) (s9 *')
proof
let s, s9 be Complex_Sequence; ::_thesis: (s (#) s9) *' = (s *') (#) (s9 *')
now__::_thesis:_for_n_being_Element_of_NAT_holds_((s_(#)_s9)_*')_._n_=_((s_*')_(#)_(s9_*'))_._n
let n be Element of NAT ; ::_thesis: ((s (#) s9) *') . n = ((s *') (#) (s9 *')) . n
thus ((s (#) s9) *') . n = ((s (#) s9) . n) *' by Def2
.= ((s . n) * (s9 . n)) *' by VALUED_1:5
.= ((s . n) *') * ((s9 . n) *') by COMPLEX1:35
.= ((s *') . n) * ((s9 . n) *') by Def2
.= ((s *') . n) * ((s9 *') . n) by Def2
.= ((s *') (#) (s9 *')) . n by VALUED_1:5 ; ::_thesis: verum
end;
hence  (s (#) s9) *' = (s *') (#) (s9 *') by FUNCT_2:63; ::_thesis: verum
end;

theorem :: COMSEQ_2:6
for s being Complex_Sequence holds (s *') " = (s ") *'
proof
let s be Complex_Sequence; ::_thesis: (s *') " = (s ") *'
now__::_thesis:_for_n_being_Element_of_NAT_holds_((s_*')_")_._n_=_((s_")_*')_._n
let n be Element of NAT ; ::_thesis: ((s *') ") . n = ((s ") *') . n
thus ((s *') ") . n = ((s *') . n) " by VALUED_1:10
.= ((s . n) *') " by Def2
.= ((s . n) ") *' by COMPLEX1:36
.= ((s ") . n) *' by VALUED_1:10
.= ((s ") *') . n by Def2 ; ::_thesis: verum
end;
hence  (s *') " = (s ") *' by FUNCT_2:63; ::_thesis: verum
end;

theorem :: COMSEQ_2:7
for s9, s being Complex_Sequence holds (s9 /" s) *' = (s9 *') /" (s *')
proof
let s9, s be Complex_Sequence; ::_thesis: (s9 /" s) *' = (s9 *') /" (s *')
now__::_thesis:_for_n_being_Element_of_NAT_holds_((s9_/"_s)_*')_._n_=_((s9_*')_/"_(s_*'))_._n
let n be Element of NAT ; ::_thesis: ((s9 /" s) *') . n = ((s9 *') /" (s *')) . n
thus ((s9 /" s) *') . n = ((s9 (#) (s ")) . n) *' by Def2
.= ((s9 . n) * ((s ") . n)) *' by VALUED_1:5
.= ((s9 . n) * ((s . n) ")) *' by VALUED_1:10
.= ((s9 . n) *') * (((s . n) ") *') by COMPLEX1:35
.= ((s9 . n) *') * (((s . n) *') ") by COMPLEX1:36
.= ((s9 *') . n) * (((s . n) *') ") by Def2
.= ((s9 *') . n) * (((s *') . n) ") by Def2
.= ((s9 *') . n) * (((s *') ") . n) by VALUED_1:10
.= ((s9 *') /" (s *')) . n by VALUED_1:5 ; ::_thesis: verum
end;
hence  (s9 /" s) *' = (s9 *') /" (s *') by FUNCT_2:63; ::_thesis: verum
end;

begin

definition
let f be complex-valued Function;
attrf is bounded  means :: COMSEQ_2:def 3
 ex r being real number st
for y being set st y in dom f holds
abs (f . y) < r;
end;

:: deftheorem  defines bounded COMSEQ_2:def_3_:_
 for f being complex-valued Function holds
( f is bounded iff ex r being real number st
for y being set st y in dom f holds
abs (f . y) < r );

definition
let s be Complex_Sequence;
redefine attr s is bounded  means :Def4: :: COMSEQ_2:def 4
 ex r being Real st
for n being Element of NAT holds |.(s . n).| < r;
compatibility
 ( s is bounded iff ex r being Real st
for n being Element of NAT holds |.(s . n).| < r )
proof
thus  ( s is bounded implies ex r being Real st
for n being Element of NAT holds |.(s . n).| < r ) ::_thesis: ( ex r being Real st
for n being Element of NAT holds |.(s . n).| < r implies s is bounded )
proof
given r being real number  such that A1: for y being set st y in dom s holds
abs (s . y) < r ; :: according to COMSEQ_2:def_3 ::_thesis: ex r being Real st
for n being Element of NAT holds |.(s . n).| < r
reconsider r = r as Element of REAL by XREAL_0:def_1;
take  r ; ::_thesis: for n being Element of NAT holds |.(s . n).| < r
let n be Element of NAT ; ::_thesis: |.(s . n).| < r
 n in NAT ;
then  n in dom s by FUNCT_2:def_1;
hence  |.(s . n).| < r by A1; ::_thesis: verum
end;
given r being Real such that A2: for n being Element of NAT holds |.(s . n).| < r ; ::_thesis: s is bounded
take  r ; :: according to COMSEQ_2:def_3 ::_thesis: for y being set st y in dom s holds
abs (s . y) < r
let y be set ; ::_thesis: ( y in dom s implies abs (s . y) < r )
assume  y in dom s ; ::_thesis: abs (s . y) < r
hence  abs (s . y) < r by A2; ::_thesis: verum
end;
end;

:: deftheorem Def4 defines bounded COMSEQ_2:def_4_:_
 for s being Complex_Sequence holds
( s is bounded iff ex r being Real st
for n being Element of NAT holds |.(s . n).| < r );

reconsider sc = NAT --> 0c as Complex_Sequence ;

registration
cluster Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued bounded for Element of K19(K20(NAT,COMPLEX));
existence
 ex b1 being Complex_Sequence st b1 is bounded
proof
take  sc ; ::_thesis: sc is bounded
take  1 ; :: according to COMSEQ_2:def_4 ::_thesis: for n being Element of NAT holds |.(sc . n).| < 1
let n be Element of NAT ; ::_thesis: |.(sc . n).| < 1
thus  |.(sc . n).| < 1 by COMPLEX1:44, FUNCOP_1:7; ::_thesis: verum
end;
end;

theorem Th8: :: COMSEQ_2:8
for s being Complex_Sequence holds
( s is bounded iff ex r being Real st
( 0 < r & ( for n being Element of NAT holds |.(s . n).| < r ) ) )
proof
let s be Complex_Sequence; ::_thesis: ( s is bounded iff ex r being Real st
( 0 < r & ( for n being Element of NAT holds |.(s . n).| < r ) ) )
thus  ( s is bounded implies ex r being Real st
( 0 < r & ( for n being Element of NAT holds |.(s . n).| < r ) ) ) ::_thesis: ( ex r being Real st
( 0 < r & ( for n being Element of NAT holds |.(s . n).| < r ) ) implies s is bounded )
proof
assume  s is bounded ; ::_thesis: ex r being Real st
( 0 < r & ( for n being Element of NAT holds |.(s . n).| < r ) )
then consider r being Real such that
A1: for n being Element of NAT holds |.(s . n).| < r by Def4;
take  r ; ::_thesis: ( 0 < r & ( for n being Element of NAT holds |.(s . n).| < r ) )
now__::_thesis:_for_n_being_Element_of_NAT_holds_0_<_r
let n be Element of NAT ; ::_thesis: 0 < r
 0 <= |.(s . n).| by COMPLEX1:46;
hence  0 < r by A1; ::_thesis: verum
end;
hence  ( 0 < r & ( for n being Element of NAT holds |.(s . n).| < r ) ) by A1; ::_thesis: verum
end;
thus  ( ex r being Real st
( 0 < r & ( for n being Element of NAT holds |.(s . n).| < r ) ) implies s is bounded ) by Def4; ::_thesis: verum
end;

begin

definition
let s be complex-valued ManySortedSet of NAT ;
attrs is convergent  means :Def5: :: COMSEQ_2:def 5
 ex g being Element of COMPLEX st
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;
end;

:: deftheorem Def5 defines convergent COMSEQ_2:def_5_:_
 for s being complex-valued ManySortedSet of NAT holds
( s is convergent iff ex g being Element of COMPLEX st
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 );

definition
let s be Complex_Sequence;
assume A1: s is convergent ;
func lim s ->  Element of COMPLEX  means :Def6: :: COMSEQ_2:def 6
 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) - it).| < p;
existence
 ex b1 being Element of COMPLEX st
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) - b1).| < p by A1, Def5;
uniqueness
 for b1, b2 being Element of COMPLEX st ( 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) - b1).| < p ) & ( 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) - b2).| < p ) holds
b1 = b2
proof
let g1, g2 be Element of COMPLEX ; ::_thesis: ( ( 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) - g1).| < p ) & ( 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) - g2).| < p ) implies g1 = g2 )
assume that
A2: for p being Real st 0 < p holds
ex n1 being Element of NAT st
for m being Element of NAT st n1 <= m holds
|.((s . m) - g1).| < p and
A3: for p being Real st 0 < p holds
ex n2 being Element of NAT st
for m being Element of NAT st n2 <= m holds
|.((s . m) - g2).| < p and
A4: g1 <> g2 ; ::_thesis: contradiction
reconsider p = |.(g1 - g2).| / 2 as Real ;
A5: |.(g1 - g2).| > 0 by A4, COMPLEX1:62;
then consider n1 being Element of NAT  such that
A6: for m being Element of NAT st n1 <= m holds
|.((s . m) - g1).| < p by A2;
consider n2 being Element of NAT  such that
A7: for m being Element of NAT st n2 <= m holds
|.((s . m) - g2).| < p by A3, A5;
reconsider n = max (n1,n2) as Element of NAT by FINSEQ_2:1;
 for m being Element of NAT st n <= m holds
2 * p < 2 * p
proof
let m be Element of NAT ; ::_thesis: ( n <= m implies 2 * p < 2 * p )
assume A8: n <= m ; ::_thesis: 2 * p < 2 * p
 n2 <= n by XXREAL_0:25;
then  n + n2 <= n + m by A8, XREAL_1:7;
then  n2 <= m by XREAL_1:6;
then A9: |.((s . m) - g2).| < p by A7;
 |.(g1 - g2).| = |.((g1 - (s . m)) - (g2 - (s . m))).| ;
then  |.(g1 - g2).| <= |.(g1 - (s . m)).| + |.(g2 - (s . m)).| by COMPLEX1:57;
then A10: |.(g1 - g2).| <= |.((s . m) - g1).| + |.(g2 - (s . m)).| by COMPLEX1:60;
 n1 <= n by XXREAL_0:25;
then  n + n1 <= n + m by A8, XREAL_1:7;
then  n1 <= m by XREAL_1:6;
then  |.((s . m) - g1).| < p by A6;
then  |.((s . m) - g1).| + |.((s . m) - g2).| < p + p by A9, XREAL_1:8;
hence  2 * p < 2 * p by A10, COMPLEX1:60; ::_thesis: verum
end;
hence  contradiction ; ::_thesis: verum
end;
end;

:: deftheorem Def6 defines lim COMSEQ_2:def_6_:_
 for s being Complex_Sequence st s is convergent holds
for b2 being Element of COMPLEX holds
( b2 = lim s iff 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) - b2).| < p );

theorem Th9: :: COMSEQ_2:9
for s being Complex_Sequence st ex g being Element of COMPLEX st
for n being Element of NAT holds s . n = g holds
s is convergent
proof
let s be Complex_Sequence; ::_thesis: ( ex g being Element of COMPLEX st
for n being Element of NAT holds s . n = g implies s is convergent )
given g being Element of COMPLEX  such that A1: for n being Element of NAT holds s . n = g ; ::_thesis: s is convergent
take  g ; :: according to COMSEQ_2:def_5 ::_thesis: 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
now__::_thesis:_for_p_being_Real_st_0_<_p_holds_
ex_k_being_Element_of_NAT_st_
for_n_being_Element_of_NAT_st_k_<=_n_holds_
|.((s_._n)_-_g).|_<_p
let p be Real; ::_thesis: ( 0 < p implies ex k being Element of NAT st
for n being Element of NAT st k <= n holds
|.((s . n) - g).| < p )
assume A2: 0 < p ; ::_thesis: ex k being Element of NAT st
for n being Element of NAT st k <= n holds
|.((s . n) - g).| < p
take k = 0 ; ::_thesis: for n being Element of NAT st k <= n holds
|.((s . n) - g).| < p
let n be Element of NAT ; ::_thesis: ( k <= n implies |.((s . n) - g).| < p )
assume  k <= n ; ::_thesis: |.((s . n) - g).| < p
 s . n = g by A1;
hence  |.((s . n) - g).| < p by A2, COMPLEX1:44; ::_thesis: verum
end;
hence  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 ; ::_thesis: verum
end;

theorem Th10: :: COMSEQ_2:10
for s being Complex_Sequence
for g being Element of COMPLEX st ( for n being Element of NAT holds s . n = g ) holds
lim s = g
proof
let s be Complex_Sequence; ::_thesis: for g being Element of COMPLEX st ( for n being Element of NAT holds s . n = g ) holds
lim s = g
let g be Element of COMPLEX ; ::_thesis: ( ( for n being Element of NAT holds s . n = g ) implies lim s = g )
assume A1: for n being Element of NAT holds s . n = g ; ::_thesis: lim s = g
A2: now__::_thesis:_for_p_being_Real_st_0_<_p_holds_
ex_k_being_Element_of_NAT_st_
for_n_being_Element_of_NAT_st_k_<=_n_holds_
|.((s_._n)_-_g).|_<_p
let p be Real; ::_thesis: ( 0 < p implies ex k being Element of NAT st
for n being Element of NAT st k <= n holds
|.((s . n) - g).| < p )
assume A3: 0 < p ; ::_thesis: ex k being Element of NAT st
for n being Element of NAT st k <= n holds
|.((s . n) - g).| < p
take k = 0 ; ::_thesis: for n being Element of NAT st k <= n holds
|.((s . n) - g).| < p
let n be Element of NAT ; ::_thesis: ( k <= n implies |.((s . n) - g).| < p )
assume  k <= n ; ::_thesis: |.((s . n) - g).| < p
 s . n = g by A1;
hence  |.((s . n) - g).| < p by A3, COMPLEX1:44; ::_thesis: verum
end;
 s is convergent by A1, Th9;
hence  lim s = g by A2, Def6; ::_thesis: verum
end;

Lm1:  for n being Element of NAT holds sc . n = 0c
by FUNCOP_1:7;

registration
cluster Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued convergent for Element of K19(K20(NAT,COMPLEX));
existence
 ex b1 being Complex_Sequence st b1 is convergent by Lm1, Th9;
end;

registration
let s be convergent Complex_Sequence;
clusters *'  ->  convergent for Complex_Sequence;
coherence
 for b1 being Complex_Sequence st b1 = s *' holds
b1 is convergent
proof
let t be Complex_Sequence; ::_thesis: ( t = s *' implies t is convergent )
assume A1: t = s *' ; ::_thesis: t is convergent
consider g being Element of COMPLEX  such that
A2: 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 Def5;
reconsider z = g *' as Element of COMPLEX ;
take r = g *' ; :: according to COMSEQ_2:def_5 ::_thesis: 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
|.((t . m) - r).| < p
let p be Real; ::_thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((t . m) - r).| < p )
assume  0 < p ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((t . m) - r).| < p
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 A2;
take  n ; ::_thesis: for m being Element of NAT st n <= m holds
|.((t . m) - r).| < p
let m be Element of NAT ; ::_thesis: ( n <= m implies |.((t . m) - r).| < p )
assume A4: n <= m ; ::_thesis: |.((t . m) - r).| < p
|.(((s *') . m) - r).| = |.(((s . m) *') - (g *')).| by Def2
.= |.(((s . m) - g) *').| by COMPLEX1:34
.= |.((s . m) - g).| by COMPLEX1:53 ;
hence  |.((t . m) - r).| < p by A3, A4, A1; ::_thesis: verum
end;
end;

theorem :: COMSEQ_2:11
canceled;

theorem Th12: :: COMSEQ_2:12
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 ;
A2: now__::_thesis:_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)_-_((lim_s)_*')).|_<_p
let p be Real; ::_thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.(((s *') . m) - ((lim s) *')).| < p )
assume  0 < p ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.(((s *') . m) - ((lim s) *')).| < p
then consider n being Element of NAT  such that
A3: for m being Element of NAT st n <= m holds
|.((s . m) - (lim s)).| < p by A1, Def6;
take n = n; ::_thesis: for m being Element of NAT st n <= m holds
|.(((s *') . m) - ((lim s) *')).| < p
let m be Element of NAT ; ::_thesis: ( n <= m implies |.(((s *') . m) - ((lim s) *')).| < p )
assume A4: n <= m ; ::_thesis: |.(((s *') . m) - ((lim s) *')).| < p
|.(((s *') . m) - ((lim s) *')).| = |.(((s . m) *') - ((lim s) *')).| by Def2
.= |.(((s . m) - (lim s)) *').| by COMPLEX1:34
.= |.((s . m) - (lim s)).| by COMPLEX1:53 ;
hence  |.(((s *') . m) - ((lim s) *')).| < p by A3, A4; ::_thesis: verum
end;
 s1 *' is convergent ;
hence  lim (s *') = (lim s) *' by A2, Def6; ::_thesis: verum
end;

begin

registration
let s1, s2 be convergent Complex_Sequence;
clusters1 + s2 ->  convergent for Complex_Sequence;
coherence
 for b1 being Complex_Sequence st b1 = s1 + s2 holds
b1 is convergent
proof
let s be Complex_Sequence; ::_thesis: ( s = s1 + s2 implies s is convergent )
assume A1: s = s1 + s2 ; ::_thesis: s is convergent
consider g being Element of COMPLEX  such that
A2: 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
|.((s1 . m) - g).| < p by Def5;
consider g9 being Element of COMPLEX  such that
A3: 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
|.((s2 . m) - g9).| < p by Def5;
take g1 = g + g9; :: according to COMSEQ_2:def_5 ::_thesis: 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) - g1).| < p
let p be Real; ::_thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((s . m) - g1).| < p )
assume A4: p > 0 ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((s . m) - g1).| < p
then consider n1 being Element of NAT  such that
A5: for m being Element of NAT st n1 <= m holds
|.((s1 . m) - g).| < p / 2 by A2;
consider n2 being Element of NAT  such that
A6: for m being Element of NAT st n2 <= m holds
|.((s2 . m) - g9).| < p / 2 by A3, A4;
reconsider n = max (n1,n2) as Element of NAT by FINSEQ_2:1;
take  n ; ::_thesis: for m being Element of NAT st n <= m holds
|.((s . m) - g1).| < p
let m be Element of NAT ; ::_thesis: ( n <= m implies |.((s . m) - g1).| < p )
assume A7: n <= m ; ::_thesis: |.((s . m) - g1).| < p
 n2 <= n by XXREAL_0:25;
then  n + n2 <= n + m by A7, XREAL_1:7;
then  n2 <= m by XREAL_1:6;
then A8: |.((s2 . m) - g9).| < p / 2 by A6;
A9: |.(((s1 + s2) . m) - g1).| = |.(((s1 . m) + (s2 . m)) - (g + g9)).| by VALUED_1:1
.= |.(((s1 . m) - g) + ((s2 . m) - g9)).| ;
 n1 <= n by XXREAL_0:25;
then  n + n1 <= n + m by A7, XREAL_1:7;
then  n1 <= m by XREAL_1:6;
then  |.((s1 . m) - g).| < p / 2 by A5;
then  |.((s1 . m) - g).| + |.((s2 . m) - g9).| < (p / 2) + (p / 2) by A8, XREAL_1:8;
then  (|.((s1 . m) - g).| + |.((s2 . m) - g9).|) + |.(((s1 + s2) . m) - g1).| < p + (|.((s1 . m) - g).| + |.((s2 . m) - g9).|) by A9, COMPLEX1:56, XREAL_1:8;
hence  |.((s . m) - g1).| < p by A1, XREAL_1:6; ::_thesis: verum
end;
end;

theorem :: COMSEQ_2:13
canceled;

theorem Th14: :: COMSEQ_2:14
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)
 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 + s9) . m) - ((lim s) + (lim s9))).| < p
proof
let p be Real; ::_thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.(((s + s9) . m) - ((lim s) + (lim s9))).| < p )
assume  0 < p ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.(((s + s9) . m) - ((lim s) + (lim s9))).| < p
then A1: 0 < p / 2 ;
then consider n1 being Element of NAT  such that
A2: for m being Element of NAT st n1 <= m holds
|.((s . m) - (lim s)).| < p / 2 by Def6;
consider n2 being Element of NAT  such that
A3: for m being Element of NAT st n2 <= m holds
|.((s9 . m) - (lim s9)).| < p / 2 by A1, Def6;
reconsider n = max (n1,n2) as Element of NAT by FINSEQ_2:1;
take  n ; ::_thesis: for m being Element of NAT st n <= m holds
|.(((s + s9) . m) - ((lim s) + (lim s9))).| < p
let m be Element of NAT ; ::_thesis: ( n <= m implies |.(((s + s9) . m) - ((lim s) + (lim s9))).| < p )
assume A4: n <= m ; ::_thesis: |.(((s + s9) . m) - ((lim s) + (lim s9))).| < p
 n2 <= n by XXREAL_0:25;
then  n + n2 <= n + m by A4, XREAL_1:7;
then  n2 <= m by XREAL_1:6;
then A5: |.((s9 . m) - (lim s9)).| < p / 2 by A3;
A6: |.(((s + s9) . m) - ((lim s) + (lim s9))).| = |.(((s . m) + (s9 . m)) - ((lim s) + (lim s9))).| by VALUED_1:1
.= |.(((s . m) - (lim s)) + ((s9 . m) - (lim s9))).| ;
 n1 <= n by XXREAL_0:25;
then  n + n1 <= n + m by A4, XREAL_1:7;
then  n1 <= m by XREAL_1:6;
then  |.((s . m) - (lim s)).| < p / 2 by A2;
then  |.((s . m) - (lim s)).| + |.((s9 . m) - (lim s9)).| < (p / 2) + (p / 2) by A5, XREAL_1:8;
then  (|.((s . m) - (lim s)).| + |.((s9 . m) - (lim s9)).|) + |.(((s + s9) . m) - ((lim s) + (lim s9))).| < p + (|.((s . m) - (lim s)).| + |.((s9 . m) - (lim s9)).|) by A6, COMPLEX1:56, XREAL_1:8;
hence  |.(((s + s9) . m) - ((lim s) + (lim s9))).| < p by XREAL_1:6; ::_thesis: verum
end;
hence  lim (s + s9) = (lim s) + (lim s9) by Def6; ::_thesis: verum
end;

theorem :: COMSEQ_2:15
canceled;

theorem :: COMSEQ_2:16
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 Th12
.= ((lim s) + (lim s9)) *' by Th14
.= ((lim s) *') + ((lim s9) *') by COMPLEX1:32 ; ::_thesis: verum
end;

registration
let s be convergent Complex_Sequence;
let c be complex number ;
clusterc (#) s ->  convergent for Complex_Sequence;
coherence
 for b1 being Complex_Sequence st b1 = c (#) s holds
b1 is convergent
proof
A1: now__::_thesis:_for_c_being_Element_of_COMPLEX_holds_c_(#)_s_is_convergent
let c be Element of COMPLEX ; ::_thesis: b1 (#) s is convergent
percases ( c = 0c or c <> 0c ) ;
supposeA2: c = 0c ; ::_thesis: b1 (#) s is convergent
now__::_thesis:_for_n_being_Element_of_NAT_holds_(c_(#)_s)_._n_=_0c
let n be Element of NAT ; ::_thesis: (c (#) s) . n = 0c
thus (c (#) s) . n = 0c * (s . n) by A2, VALUED_1:6
.= 0c ; ::_thesis: verum
end;
hence  c (#) s is convergent by Th9; ::_thesis: verum
end;
supposeA3: c <> 0c ; ::_thesis: b1 (#) s is convergent
thus  c (#) s is convergent ::_thesis: verum
proof
consider g being Element of COMPLEX  such that
A4: 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 Def5;
take g9 = c * g; :: according to COMSEQ_2:def_5 ::_thesis: 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
|.(((c (#) s) . m) - g9).| < p
let p be Real; ::_thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.(((c (#) s) . m) - g9).| < p )
assume A5: 0 < p ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.(((c (#) s) . m) - g9).| < p
A6: |.c.| > 0 by A3, COMPLEX1:47;
consider n being Element of NAT  such that
A7: for m being Element of NAT st n <= m holds
|.((s . m) - g).| < p / |.c.| by A6, A4, A5;
take  n ; ::_thesis: for m being Element of NAT st n <= m holds
|.(((c (#) s) . m) - g9).| < p
let m be Element of NAT ; ::_thesis: ( n <= m implies |.(((c (#) s) . m) - g9).| < p )
assume  n <= m ; ::_thesis: |.(((c (#) s) . m) - g9).| < p
then  |.((s . m) - g).| < p / |.c.| by A7;
then  |.((s . m) - g).| * |.c.| < (p / |.c.|) * |.c.| by A6, XREAL_1:68;
then  |.((s . m) - g).| * |.c.| < (p * (|.c.| ")) * |.c.| by XCMPLX_0:def_9;
then  |.((s . m) - g).| * |.c.| < p * ((|.c.| ") * |.c.|) ;
then A8: |.((s . m) - g).| * |.c.| < p * 1 by A6, XCMPLX_0:def_7;
|.(((c (#) s) . m) - g9).| = |.((c * (s . m)) - (c * g)).| by VALUED_1:6
.= |.(c * ((s . m) - g)).|
.= |.((s . m) - g).| * |.c.| by COMPLEX1:65 ;
hence  |.(((c (#) s) . m) - g9).| < p by A8; ::_thesis: verum
end;
end;
end;
end;
 c in COMPLEX by XCMPLX_0:def_2;
hence  for b1 being Complex_Sequence st b1 = c (#) s holds
b1 is convergent by A1; ::_thesis: verum
end;
end;

theorem :: COMSEQ_2:17
canceled;

theorem Th18: :: COMSEQ_2:18
for s being convergent Complex_Sequence
for r being complex number holds lim (r (#) s) = r * (lim s)
proof
let s be convergent Complex_Sequence; ::_thesis: for r being complex number holds lim (r (#) s) = r * (lim s)
let r be complex number ; ::_thesis: lim (r (#) s) = r * (lim s)
reconsider r = r as Element of COMPLEX by XCMPLX_0:def_2;
percases ( r <> 0c or r = 0c ) ;
supposeA1: r <> 0c ; ::_thesis: lim (r (#) s) = r * (lim s)
 for p being Real st p > 0 holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.(((r (#) s) . m) - (r * (lim s))).| < p
proof
let p be Real; ::_thesis: ( p > 0 implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.(((r (#) s) . m) - (r * (lim s))).| < p )
assume A2: p > 0 ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.(((r (#) s) . m) - (r * (lim s))).| < p
A3: |.r.| > 0 by A1, COMPLEX1:47;
 p / |.r.| > 0 by A3, A2;
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 / |.r.| by Def6;
take  n ; ::_thesis: for m being Element of NAT st n <= m holds
|.(((r (#) s) . m) - (r * (lim s))).| < p
let m be Element of NAT ; ::_thesis: ( n <= m implies |.(((r (#) s) . m) - (r * (lim s))).| < p )
assume  n <= m ; ::_thesis: |.(((r (#) s) . m) - (r * (lim s))).| < p
then  |.((s . m) - (lim s)).| < p / |.r.| by A4;
then  |.((s . m) - (lim s)).| * |.r.| < (p / |.r.|) * |.r.| by A3, XREAL_1:68;
then  |.((s . m) - (lim s)).| * |.r.| < (p * (|.r.| ")) * |.r.| by XCMPLX_0:def_9;
then  |.((s . m) - (lim s)).| * |.r.| < p * ((|.r.| ") * |.r.|) ;
then A5: |.((s . m) - (lim s)).| * |.r.| < p * 1 by A3, XCMPLX_0:def_7;
|.(((r (#) s) . m) - (r * (lim s))).| = |.((r * (s . m)) - (r * (lim s))).| by VALUED_1:6
.= |.(r * ((s . m) - (lim s))).|
.= |.((s . m) - (lim s)).| * |.r.| by COMPLEX1:65 ;
hence  |.(((r (#) s) . m) - (r * (lim s))).| < p by A5; ::_thesis: verum
end;
hence  lim (r (#) s) = r * (lim s) by Def6; ::_thesis: verum
end;
supposeA6: r = 0c ; ::_thesis: lim (r (#) s) = r * (lim s)
now__::_thesis:_for_n_being_Element_of_NAT_holds_(r_(#)_s)_._n_=_0c
let n be Element of NAT ; ::_thesis: (r (#) s) . n = 0c
thus (r (#) s) . n = 0c * (s . n) by A6, VALUED_1:6
.= 0c ; ::_thesis: verum
end;
hence  lim (r (#) s) = r * (lim s) by A6, Th10; ::_thesis: verum
end;
end;
end;

theorem :: COMSEQ_2:19
canceled;

theorem :: COMSEQ_2:20
for r being Element of COMPLEX
for s being convergent Complex_Sequence holds lim ((r (#) s) *') = (r *') * ((lim s) *')
proof
let r be Element of COMPLEX ; ::_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 Th12
.= (r * (lim s)) *' by Th18
.= (r *') * ((lim s) *') by COMPLEX1:35 ; ::_thesis: verum
end;

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

theorem :: COMSEQ_2:21
canceled;

theorem Th22: :: COMSEQ_2:22
for s being convergent Complex_Sequence holds lim (- s) = - (lim s)
proof
let s be convergent Complex_Sequence; ::_thesis: lim (- s) = - (lim s)
lim (- s) = (- 1) * (lim s) by Th18
.= - (1r * (lim s)) by COMPLEX1:def_4 ;
hence  lim (- s) = - (lim s) by COMPLEX1:def_4; ::_thesis: verum
end;

theorem :: COMSEQ_2:23
canceled;

theorem :: COMSEQ_2:24
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 Th12
.= (- (lim s)) *' by Th22
.= - ((lim s) *') by COMPLEX1:33 ; ::_thesis: verum
end;

registration
let s1, s2 be convergent Complex_Sequence;
clusters1 - s2 ->  convergent for Complex_Sequence;
coherence
 for b1 being Complex_Sequence st b1 = s1 - s2 holds
b1 is convergent
proof
 - s2 is convergent ;
hence  for b1 being Complex_Sequence st b1 = s1 - s2 holds
b1 is convergent ; ::_thesis: verum
end;
end;

theorem :: COMSEQ_2:25
canceled;

theorem Th26: :: COMSEQ_2:26
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)
lim (s - s9) = (lim s) + (lim (- s9)) by Th14
.= (lim s) + (- (lim s9)) by Th22 ;
hence  lim (s - s9) = (lim s) - (lim s9) ; ::_thesis: verum
end;

theorem :: COMSEQ_2:27
canceled;

theorem :: COMSEQ_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 Th12
.= ((lim s) - (lim s9)) *' by Th26
.= ((lim s) *') - ((lim s9) *') by COMPLEX1:34 ; ::_thesis: verum
end;

registration
cluster Function-like V18( NAT , COMPLEX ) convergent  ->  bounded for Element of K19(K20(NAT,COMPLEX));
coherence
 for b1 being Complex_Sequence st b1 is convergent holds
b1 is bounded
proof
let s be Complex_Sequence; ::_thesis: ( s is convergent implies s is bounded )
assume  s is convergent ; ::_thesis: s is bounded
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
|.((s . m) - g).| < p by Def5;
consider n1 being Element of NAT  such that
A2: for m being Element of NAT st n1 <= m holds
|.((s . m) - g).| < 1 by A1;
now__::_thesis:_ex_R_being_Element_of_REAL_st_
(_0_<_R_&_(_for_m_being_Element_of_NAT_st_n1_<=_m_holds_
|.(s_._m).|_<_R_)_)
take R = |.g.| + 1; ::_thesis: ( 0 < R & ( for m being Element of NAT st n1 <= m holds
|.(s . 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
|.(s . m).| < R
let m be Element of NAT ; ::_thesis: ( n1 <= m implies |.(s . m).| < R )
A3: (|.(s . m).| - |.g.|) + |.g.| = |.(s . m).| ;
assume  n1 <= m ; ::_thesis: |.(s . m).| < R
then A4: |.((s . m) - g).| < 1 by A2;
 |.(s . m).| - |.g.| <= |.((s . m) - g).| by COMPLEX1:59;
then  |.(s . m).| - |.g.| < 1 by A4, XXREAL_0:2;
hence  |.(s . m).| < R by A3, XREAL_1:6; ::_thesis: verum
end;
then consider R1 being real number  such that
A5: 0 < R1 and
A6: for m being Element of NAT st n1 <= m holds
|.(s . m).| < R1 ;
consider R2 being Real such that
A7: 0 < R2 and
A8: for m being Element of NAT st m <= n1 holds
|.(s . m).| < R2 by Th2;
take R = R1 + R2; :: according to COMSEQ_2:def_4 ::_thesis: for n being Element of NAT holds |.(s . n).| < R
let m be Element of NAT ; ::_thesis: |.(s . m).| < R
A9: R2 + 0 < R by A5, XREAL_1:8;
A10: now__::_thesis:_(_m_<=_n1_implies_|.(s_._m).|_<_R_)
assume  m <= n1 ; ::_thesis: |.(s . m).| < R
then  |.(s . m).| < R2 by A8;
hence  |.(s . m).| < R by A9, XXREAL_0:2; ::_thesis: verum
end;
A11: R1 + 0 < R by A7, XREAL_1:8;
now__::_thesis:_(_n1_<=_m_implies_|.(s_._m).|_<_R_)
assume  n1 <= m ; ::_thesis: |.(s . m).| < R
then  |.(s . m).| < R1 by A6;
hence  |.(s . m).| < R by A11, XXREAL_0:2; ::_thesis: verum
end;
hence  |.(s . m).| < R by A10; ::_thesis: verum
end;
end;

registration
cluster Function-like V18( NAT , COMPLEX ) non bounded  ->  non convergent for Element of K19(K20(NAT,COMPLEX));
coherence
 for b1 being Complex_Sequence st not b1 is bounded holds
not b1 is convergent ;
end;

registration
let s1, s2 be convergent Complex_Sequence;
clusters1 (#) s2 ->  convergent for Complex_Sequence;
coherence
 for b1 being Complex_Sequence st b1 = s1 (#) s2 holds
b1 is convergent
proof
let s be Complex_Sequence; ::_thesis: ( s = s1 (#) s2 implies s is convergent )
assume A1: s = s1 (#) s2 ; ::_thesis: s is convergent
consider g1 being Element of COMPLEX  such that
A2: 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
|.((s1 . m) - g1).| < p by Def5;
consider g2 being Element of COMPLEX  such that
A3: 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
|.((s2 . m) - g2).| < p by Def5;
take g = g1 * g2; :: according to COMSEQ_2:def_5 ::_thesis: 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
let p be Real; ::_thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((s . m) - g).| < p )
consider R being Real such that
A4: 0 < R and
A5: for n being Element of NAT holds |.(s1 . n).| < R by Th8;
A6: 0 + 0 < |.g2.| + R by A4, COMPLEX1:46, XREAL_1:8;
assume A7: 0 < p ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((s . m) - g).| < p
then consider n1 being Element of NAT  such that
A8: for m being Element of NAT st n1 <= m holds
|.((s1 . m) - g1).| < p / (|.g2.| + R) by A2, A6;
consider n2 being Element of NAT  such that
A9: for m being Element of NAT st n2 <= m holds
|.((s2 . m) - g2).| < p / (|.g2.| + R) by A3, A6, A7;
take n = n1 + n2; ::_thesis: for m being Element of NAT st n <= m holds
|.((s . m) - g).| < p
let m be Element of NAT ; ::_thesis: ( n <= m implies |.((s . m) - g).| < p )
assume A10: n <= m ; ::_thesis: |.((s . m) - g).| < p
 n1 <= n1 + n2 by NAT_1:12;
then  n1 <= m by A10, XXREAL_0:2;
then A11: |.((s1 . m) - g1).| <= p / (|.g2.| + R) by A8;
 ( 0 <= |.g2.| & |.(((s1 . m) - g1) * g2).| = |.g2.| * |.((s1 . m) - g1).| ) by COMPLEX1:46, COMPLEX1:65;
then A12: |.(((s1 . m) - g1) * g2).| <= |.g2.| * (p / (|.g2.| + R)) by A11, XREAL_1:64;
|.(((s1 (#) s2) . m) - g).| = |.(((((s1 . m) * (s2 . m)) - ((s1 . m) * g2)) + ((s1 . m) * g2)) - (g1 * g2)).| by VALUED_1:5
.= |.(((s1 . m) * ((s2 . m) - g2)) + (((s1 . m) - g1) * g2)).| ;
then A13: |.(((s1 (#) s2) . m) - g).| <= |.((s1 . m) * ((s2 . m) - g2)).| + |.(((s1 . m) - g1) * g2).| by COMPLEX1:56;
 n2 <= n by NAT_1:12;
then  n2 <= m by A10, XXREAL_0:2;
then A14: |.((s2 . m) - g2).| < p / (|.g2.| + R) by A9;
A15: ( 0 <= |.(s1 . m).| & 0 <= |.((s2 . m) - g2).| ) by COMPLEX1:46;
 |.(s1 . m).| < R by A5;
then  |.(s1 . m).| * |.((s2 . m) - g2).| < R * (p / (|.g2.| + R)) by A15, A14, XREAL_1:96;
then A16: |.((s1 . m) * ((s2 . m) - g2)).| < R * (p / (|.g2.| + R)) by COMPLEX1:65;
(R * (p / (|.g2.| + R))) + (|.g2.| * (p / (|.g2.| + R))) = (p / (|.g2.| + R)) * (|.g2.| + R)
.= p by A6, XCMPLX_1:87 ;
then  |.((s1 . m) * ((s2 . m) - g2)).| + |.(((s1 . m) - g1) * g2).| < p by A16, A12, XREAL_1:8;
hence  |.((s . m) - g).| < p by A1, A13, XXREAL_0:2; ::_thesis: verum
end;
end;

theorem :: COMSEQ_2:29
canceled;

theorem Th30: :: COMSEQ_2:30
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)
consider R being Real such that
A1: 0 < R and
A2: for n being Element of NAT holds |.(s . n).| < R by Th8;
A3: 0 + 0 < |.(lim s9).| + R by A1, COMPLEX1:46, XREAL_1:8;
A4: 0 <= |.(lim s9).| by COMPLEX1:46;
now__::_thesis:_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_(#)_s9)_._m)_-_((lim_s)_*_(lim_s9))).|_<_p
let p be Real; ::_thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.(((s (#) s9) . m) - ((lim s) * (lim s9))).| < p )
assume  0 < p ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.(((s (#) s9) . m) - ((lim s) * (lim s9))).| < p
then A5: 0 < p / (|.(lim s9).| + R) by A3;
then consider n1 being Element of NAT  such that
A6: for m being Element of NAT st n1 <= m holds
|.((s . m) - (lim s)).| < p / (|.(lim s9).| + R) by Def6;
consider n2 being Element of NAT  such that
A7: for m being Element of NAT st n2 <= m holds
|.((s9 . m) - (lim s9)).| < p / (|.(lim s9).| + R) by A5, Def6;
take n = n1 + n2; ::_thesis: for m being Element of NAT st n <= m holds
|.(((s (#) s9) . m) - ((lim s) * (lim s9))).| < p
let m be Element of NAT ; ::_thesis: ( n <= m implies |.(((s (#) s9) . m) - ((lim s) * (lim s9))).| < p )
assume A8: n <= m ; ::_thesis: |.(((s (#) s9) . m) - ((lim s) * (lim s9))).| < p
 n1 <= n1 + n2 by NAT_1:12;
then  n1 <= m by A8, XXREAL_0:2;
then A9: |.((s . m) - (lim s)).| <= p / (|.(lim s9).| + R) by A6;
 |.(((s . m) - (lim s)) * (lim s9)).| = |.(lim s9).| * |.((s . m) - (lim s)).| by COMPLEX1:65;
then A10: |.(((s . m) - (lim s)) * (lim s9)).| <= |.(lim s9).| * (p / (|.(lim s9).| + R)) by A4, A9, XREAL_1:64;
A11: ( 0 <= |.(s . m).| & 0 <= |.((s9 . m) - (lim s9)).| ) by COMPLEX1:46;
 n2 <= n by NAT_1:12;
then  n2 <= m by A8, XXREAL_0:2;
then A12: |.((s9 . m) - (lim s9)).| < p / (|.(lim s9).| + R) by A7;
|.(((s (#) s9) . m) - ((lim s) * (lim s9))).| = |.(((((s . m) * (s9 . m)) - ((s . m) * (lim s9))) + ((s . m) * (lim s9))) - ((lim s) * (lim s9))).| by VALUED_1:5
.= |.(((s . m) * ((s9 . m) - (lim s9))) + (((s . m) - (lim s)) * (lim s9))).| ;
then A13: |.(((s (#) s9) . m) - ((lim s) * (lim s9))).| <= |.((s . m) * ((s9 . m) - (lim s9))).| + |.(((s . m) - (lim s)) * (lim s9)).| by COMPLEX1:56;
 |.(s . m).| < R by A2;
then  |.(s . m).| * |.((s9 . m) - (lim s9)).| < R * (p / (|.(lim s9).| + R)) by A11, A12, XREAL_1:96;
then A14: |.((s . m) * ((s9 . m) - (lim s9))).| < R * (p / (|.(lim s9).| + R)) by COMPLEX1:65;
(R * (p / (|.(lim s9).| + R))) + (|.(lim s9).| * (p / (|.(lim s9).| + R))) = (p / (|.(lim s9).| + R)) * (|.(lim s9).| + R)
.= p by A3, XCMPLX_1:87 ;
then  |.((s . m) * ((s9 . m) - (lim s9))).| + |.(((s . m) - (lim s)) * (lim s9)).| < p by A14, A10, XREAL_1:8;
hence  |.(((s (#) s9) . m) - ((lim s) * (lim s9))).| < p by A13, XXREAL_0:2; ::_thesis: verum
end;
hence  lim (s (#) s9) = (lim s) * (lim s9) by Def6; ::_thesis: verum
end;

theorem :: COMSEQ_2:31
canceled;

theorem :: COMSEQ_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 Th12
.= ((lim s) * (lim s9)) *' by Th30
.= ((lim s) *') * ((lim s9) *') by COMPLEX1:35 ; ::_thesis: verum
end;

theorem Th33: :: COMSEQ_2:33
for s being convergent Complex_Sequence st lim s <> 0c holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.(lim s).| / 2 < |.(s . m).|
proof
let s be convergent Complex_Sequence; ::_thesis: ( lim s <> 0c implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.(lim s).| / 2 < |.(s . m).| )
assume A1: lim s <> 0c ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.(lim s).| / 2 < |.(s . m).|
 0 < |.(lim s).| by A1, COMPLEX1:47;
then  0 < |.(lim s).| / 2 ;
then consider n1 being Element of NAT  such that
A2: for m being Element of NAT st n1 <= m holds
|.((s . m) - (lim s)).| < |.(lim s).| / 2 by Def6;
take n = n1; ::_thesis: for m being Element of NAT st n <= m holds
|.(lim s).| / 2 < |.(s . m).|
let m be Element of NAT ; ::_thesis: ( n <= m implies |.(lim s).| / 2 < |.(s . m).| )
assume  n <= m ; ::_thesis: |.(lim s).| / 2 < |.(s . m).|
then A3: |.((s . m) - (lim s)).| < |.(lim s).| / 2 by A2;
A4: |.((lim s) - (s . m)).| = |.(- ((s . m) - (lim s))).|
.= |.((s . m) - (lim s)).| by COMPLEX1:52 ;
A5: ( (|.(lim s).| / 2) + (|.(s . m).| - (|.(lim s).| / 2)) = |.(s . m).| & (|.(lim s).| - |.(s . m).|) + (|.(s . m).| - (|.(lim s).| / 2)) = |.(lim s).| / 2 ) ;
 |.(lim s).| - |.(s . m).| <= |.((lim s) - (s . m)).| by COMPLEX1:59;
then  |.(lim s).| - |.(s . m).| < |.(lim s).| / 2 by A3, A4, XXREAL_0:2;
hence  |.(lim s).| / 2 < |.(s . m).| by A5, XREAL_1:6; ::_thesis: verum
end;

theorem Th34: :: COMSEQ_2:34
for s being convergent Complex_Sequence st lim s <> 0c & s is non-zero holds
s " is convergent
proof
let s be convergent Complex_Sequence; ::_thesis: ( lim s <> 0c & s is non-zero implies s " is convergent )
assume that
A1: lim s <> 0c and
A2: s is non-zero ; ::_thesis: s " is convergent
consider n1 being Element of NAT  such that
A3: for m being Element of NAT st n1 <= m holds
|.(lim s).| / 2 < |.(s . m).| by A1, Th33;
take  (lim s) " ; :: according to COMSEQ_2:def_5 ::_thesis: 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) - ((lim s) ")).| < p
let p be Real; ::_thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.(((s ") . m) - ((lim s) ")).| < p )
assume A4: 0 < p ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.(((s ") . m) - ((lim s) ")).| < p
A5: 0 < |.(lim s).| by A1, COMPLEX1:47;
then  0 * 0 < |.(lim s).| * |.(lim s).| ;
then  0 < (|.(lim s).| * |.(lim s).|) / 2 ;
then  0 * 0 < p * ((|.(lim s).| * |.(lim s).|) / 2) by A4;
then consider n2 being Element of NAT  such that
A6: for m being Element of NAT st n2 <= m holds
|.((s . m) - (lim s)).| < p * ((|.(lim s).| * |.(lim s).|) / 2) by Def6;
take n = n1 + n2; ::_thesis: for m being Element of NAT st n <= m holds
|.(((s ") . m) - ((lim s) ")).| < p
let m be Element of NAT ; ::_thesis: ( n <= m implies |.(((s ") . m) - ((lim s) ")).| < p )
assume A7: n <= m ; ::_thesis: |.(((s ") . m) - ((lim s) ")).| < p
 n1 <= n1 + n2 by NAT_1:12;
then  n1 <= m by A7, XXREAL_0:2;
then A8: |.(lim s).| / 2 < |.(s . m).| by A3;
A9: 0 < |.(lim s).| / 2 by A5;
then  0 * 0 < p * (|.(lim s).| / 2) by A4;
then A10: (p * (|.(lim s).| / 2)) / |.(s . m).| < (p * (|.(lim s).| / 2)) / (|.(lim s).| / 2) by A8, A9, XREAL_1:76;
A11: 0 <> |.(lim s).| / 2 by A1, COMPLEX1:47;
A12: (p * (|.(lim s).| / 2)) / (|.(lim s).| / 2) = (p * (|.(lim s).| / 2)) * ((|.(lim s).| / 2) ") by XCMPLX_0:def_9
.= p * ((|.(lim s).| / 2) * ((|.(lim s).| / 2) "))
.= p * 1 by A11, XCMPLX_0:def_7
.= p ;
A13: 0 <> |.(lim s).| by A1, COMPLEX1:47;
A14: (p * ((|.(lim s).| * |.(lim s).|) / 2)) / (|.(s . m).| * |.(lim s).|) = (p * ((2 ") * (|.(lim s).| * |.(lim s).|))) * ((|.(s . m).| * |.(lim s).|) ") by XCMPLX_0:def_9
.= (p * (2 ")) * ((|.(lim s).| * |.(lim s).|) * ((|.(lim s).| * |.(s . m).|) "))
.= (p * (2 ")) * ((|.(lim s).| * |.(lim s).|) * ((|.(lim s).| ") * (|.(s . m).| "))) by XCMPLX_1:204
.= (p * (2 ")) * ((|.(lim s).| * (|.(lim s).| * (|.(lim s).| "))) * (|.(s . m).| "))
.= (p * (2 ")) * ((|.(lim s).| * 1) * (|.(s . m).| ")) by A13, XCMPLX_0:def_7
.= (p * (|.(lim s).| / 2)) * (|.(s . m).| ")
.= (p * (|.(lim s).| / 2)) / |.(s . m).| by XCMPLX_0:def_9 ;
 (s . m) * (lim s) <> 0c by A1, A2;
then  0 < |.((s . m) * (lim s)).| by COMPLEX1:47;
then A15: 0 < |.(s . m).| * |.(lim s).| by COMPLEX1:65;
 n2 <= n by NAT_1:12;
then  n2 <= m by A7, XXREAL_0:2;
then  |.((s . m) - (lim s)).| < p * ((|.(lim s).| * |.(lim s).|) / 2) by A6;
then A16: |.((s . m) - (lim s)).| / (|.(s . m).| * |.(lim s).|) < (p * ((|.(lim s).| * |.(lim s).|) / 2)) / (|.(s . m).| * |.(lim s).|) by A15, XREAL_1:74;
|.(((s ") . m) - ((lim s) ")).| = |.(((s . m) ") - ((lim s) ")).| by VALUED_1:10
.= |.((s . m) - (lim s)).| / (|.(s . m).| * |.(lim s).|) by A1, A2, Th1 ;
hence  |.(((s ") . m) - ((lim s) ")).| < p by A16, A14, A10, A12, XXREAL_0:2; ::_thesis: verum
end;

theorem Th35: :: COMSEQ_2:35
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 that
A1: s is convergent and
A2: lim s <> 0c and
A3: s is non-zero ; ::_thesis: lim (s ") = (lim s) "
consider n1 being Element of NAT  such that
A4: for m being Element of NAT st n1 <= m holds
|.(lim s).| / 2 < |.(s . m).| by A1, A2, Th33;
A5: 0 < |.(lim s).| by A2, COMPLEX1:47;
then  0 * 0 < |.(lim s).| * |.(lim s).| ;
then A6: 0 < (|.(lim s).| * |.(lim s).|) / 2 ;
A7: 0 <> |.(lim s).| by A2, COMPLEX1:47;
A8: now__::_thesis:_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)_-_((lim_s)_")).|_<_p
let p be Real; ::_thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.(((s ") . m) - ((lim s) ")).| < p )
A9: 0 <> |.(lim s).| / 2 by A2, COMPLEX1:47;
A10: (p * (|.(lim s).| / 2)) / (|.(lim s).| / 2) = (p * (|.(lim s).| / 2)) * ((|.(lim s).| / 2) ") by XCMPLX_0:def_9
.= p * ((|.(lim s).| / 2) * ((|.(lim s).| / 2) "))
.= p * 1 by A9, XCMPLX_0:def_7
.= p ;
assume A11: 0 < p ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.(((s ") . m) - ((lim s) ")).| < p
then  0 * 0 < p * ((|.(lim s).| * |.(lim s).|) / 2) by A6;
then consider n2 being Element of NAT  such that
A12: for m being Element of NAT st n2 <= m holds
|.((s . m) - (lim s)).| < p * ((|.(lim s).| * |.(lim s).|) / 2) by A1, Def6;
take n = n1 + n2; ::_thesis: for m being Element of NAT st n <= m holds
|.(((s ") . m) - ((lim s) ")).| < p
let m be Element of NAT ; ::_thesis: ( n <= m implies |.(((s ") . m) - ((lim s) ")).| < p )
assume A13: n <= m ; ::_thesis: |.(((s ") . m) - ((lim s) ")).| < p
 n1 <= n1 + n2 by NAT_1:12;
then  n1 <= m by A13, XXREAL_0:2;
then A14: |.(lim s).| / 2 < |.(s . m).| by A4;
A15: 0 < |.(lim s).| / 2 by A5;
then  0 * 0 < p * (|.(lim s).| / 2) by A11;
then A16: (p * (|.(lim s).| / 2)) / |.(s . m).| < (p * (|.(lim s).| / 2)) / (|.(lim s).| / 2) by A14, A15, XREAL_1:76;
A17: (p * ((|.(lim s).| * |.(lim s).|) / 2)) / (|.(s . m).| * |.(lim s).|) = (p * ((2 ") * (|.(lim s).| * |.(lim s).|))) * ((|.(s . m).| * |.(lim s).|) ") by XCMPLX_0:def_9
.= (p * (2 ")) * ((|.(lim s).| * |.(lim s).|) * ((|.(lim s).| * |.(s . m).|) "))
.= (p * (2 ")) * ((|.(lim s).| * |.(lim s).|) * ((|.(lim s).| ") * (|.(s . m).| "))) by XCMPLX_1:204
.= (p * (2 ")) * ((|.(lim s).| * (|.(lim s).| * (|.(lim s).| "))) * (|.(s . m).| "))
.= (p * (2 ")) * ((|.(lim s).| * 1) * (|.(s . m).| ")) by A7, XCMPLX_0:def_7
.= (p * (|.(lim s).| / 2)) * (|.(s . m).| ")
.= (p * (|.(lim s).| / 2)) / |.(s . m).| by XCMPLX_0:def_9 ;
 (s . m) * (lim s) <> 0c by A2, A3;
then  0 < |.((s . m) * (lim s)).| by COMPLEX1:47;
then A18: 0 < |.(s . m).| * |.(lim s).| by COMPLEX1:65;
 n2 <= n by NAT_1:12;
then  n2 <= m by A13, XXREAL_0:2;
then  |.((s . m) - (lim s)).| < p * ((|.(lim s).| * |.(lim s).|) / 2) by A12;
then A19: |.((s . m) - (lim s)).| / (|.(s . m).| * |.(lim s).|) < (p * ((|.(lim s).| * |.(lim s).|) / 2)) / (|.(s . m).| * |.(lim s).|) by A18, XREAL_1:74;
|.(((s ") . m) - ((lim s) ")).| = |.(((s . m) ") - ((lim s) ")).| by VALUED_1:10
.= |.((s . m) - (lim s)).| / (|.(s . m).| * |.(lim s).|) by A2, A3, Th1 ;
hence  |.(((s ") . m) - ((lim s) ")).| < p by A19, A17, A16, A10, XXREAL_0:2; ::_thesis: verum
end;
 s " is convergent by A1, A2, A3, Th34;
hence  lim (s ") = (lim s) " by A8, Def6; ::_thesis: verum
end;

theorem :: COMSEQ_2:36
canceled;

theorem :: COMSEQ_2:37
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 Th34;
hence  lim ((s ") *') = (lim (s ")) *' by Th12
.= ((lim s) ") *' by A1, Th35
.= ((lim s) *') " by COMPLEX1:36 ;
::_thesis: verum
end;

theorem Th38: :: COMSEQ_2:38
for s9, s being Complex_Sequence st s9 is convergent & s is convergent & lim s <> 0c & s is non-zero holds
s9 /" s is convergent
proof
let s9, s be Complex_Sequence; ::_thesis: ( s9 is convergent & s is convergent & lim s <> 0c & s is non-zero implies s9 /" s is convergent )
assume that
A1: s9 is convergent and
A2: ( s is convergent & lim s <> 0c & s is non-zero ) ; ::_thesis: s9 /" s is convergent
 s " is convergent by A2, Th34;
hence  s9 /" s is convergent by A1; ::_thesis: verum
end;

theorem Th39: :: COMSEQ_2:39
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 that
A1: s9 is convergent and
A2: ( s is convergent & lim s <> 0c & s is non-zero ) ; ::_thesis: lim (s9 /" s) = (lim s9) / (lim s)
 s " is convergent by A2, Th34;
then  lim (s9 (#) (s ")) = (lim s9) * (lim (s ")) by A1, Th30
.= (lim s9) * ((lim s) ") by A2, Th35
.= (lim s9) / (lim s) by XCMPLX_0:def_9 ;
hence  lim (s9 /" s) = (lim s9) / (lim s) ; ::_thesis: verum
end;

theorem :: COMSEQ_2:40
canceled;

theorem :: COMSEQ_2:41
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 Th38;
hence  lim ((s9 /" s) *') = (lim (s9 /" s)) *' by Th12
.= ((lim s9) / (lim s)) *' by A1, Th39
.= ((lim s9) *') / ((lim s) *') by COMPLEX1:37 ;
::_thesis: verum
end;

theorem Th42: :: COMSEQ_2:42
for s, s1 being Complex_Sequence st s is convergent & s1 is bounded & lim s = 0c holds
s (#) s1 is convergent
proof
let s, s1 be Complex_Sequence; ::_thesis: ( s is convergent & s1 is bounded & lim s = 0c implies s (#) s1 is convergent )
assume that
A1: s is convergent and
A2: s1 is bounded and
A3: lim s = 0c ; ::_thesis: s (#) s1 is convergent
take g = 0c ; :: according to COMSEQ_2:def_5 ::_thesis: 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 (#) s1) . m) - g).| < p
consider R being Real such that
A4: 0 < R and
A5: for m being Element of NAT holds |.(s1 . m).| < R by A2, Th8;
let p be Real; ::_thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.(((s (#) s1) . m) - g).| < p )
assume A6: 0 < p ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.(((s (#) s1) . m) - g).| < p
A7: 0 < p / R by A6, A4;
then consider n1 being Element of NAT  such that
A8: for m being Element of NAT st n1 <= m holds
|.((s . m) - 0c).| < p / R by A1, A3, Def6;
take n = n1; ::_thesis: for m being Element of NAT st n <= m holds
|.(((s (#) s1) . m) - g).| < p
let m be Element of NAT ; ::_thesis: ( n <= m implies |.(((s (#) s1) . m) - g).| < p )
assume A9: n <= m ; ::_thesis: |.(((s (#) s1) . m) - g).| < p
A10: |.(((s (#) s1) . m) - g).| = |.((s . m) * (s1 . m)).| by VALUED_1:5
.= |.(s . m).| * |.(s1 . m).| by COMPLEX1:65 ;
 |.(s . m).| = |.((s . m) - 0c).| ;
then A11: |.(s . m).| < p / R by A8, A9;
now__::_thesis:_(_|.(s1_._m).|_<>_0_implies_|.(((s_(#)_s1)_._m)_-_g).|_<_p_)
(p / R) * R = (p * (R ")) * R by XCMPLX_0:def_9
.= p * ((R ") * R)
.= p * 1 by A4, XCMPLX_0:def_7
.= p ;
then A12: (p / R) * |.(s1 . m).| < p by A5, A7, XREAL_1:68;
A13: 0 <= |.(s1 . m).| by COMPLEX1:46;
assume  |.(s1 . m).| <> 0 ; ::_thesis: |.(((s (#) s1) . m) - g).| < p
then  |.(((s (#) s1) . m) - g).| < (p / R) * |.(s1 . m).| by A11, A10, A13, XREAL_1:68;
hence  |.(((s (#) s1) . m) - g).| < p by A12, XXREAL_0:2; ::_thesis: verum
end;
hence  |.(((s (#) s1) . m) - g).| < p by A6, A10; ::_thesis: verum
end;

theorem Th43: :: COMSEQ_2:43
for s, s1 being Complex_Sequence st s is convergent & s1 is bounded & lim s = 0c holds
lim (s (#) s1) = 0c
proof
let s, s1 be Complex_Sequence; ::_thesis: ( s is convergent & s1 is bounded & lim s = 0c implies lim (s (#) s1) = 0c )
assume that
A1: s is convergent and
A2: s1 is bounded and
A3: lim s = 0c ; ::_thesis: lim (s (#) s1) = 0c
A4: now__::_thesis:_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_(#)_s1)_._m)_-_0c).|_<_p
consider R being Real such that
A5: 0 < R and
A6: for m being Element of NAT holds |.(s1 . m).| < R by A2, Th8;
let p be Real; ::_thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.(((s (#) s1) . m) - 0c).| < p )
assume A7: 0 < p ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.(((s (#) s1) . m) - 0c).| < p
A8: 0 < p / R by A7, A5;
then consider n1 being Element of NAT  such that
A9: for m being Element of NAT st n1 <= m holds
|.((s . m) - 0c).| < p / R by A1, A3, Def6;
take n = n1; ::_thesis: for m being Element of NAT st n <= m holds
|.(((s (#) s1) . m) - 0c).| < p
let m be Element of NAT ; ::_thesis: ( n <= m implies |.(((s (#) s1) . m) - 0c).| < p )
(p / R) * R = (p * (R ")) * R by XCMPLX_0:def_9
.= p * ((R ") * R)
.= p * 1 by A5, XCMPLX_0:def_7 ;
then A10: (p / R) * |.(s1 . m).| < p by A6, A8, XREAL_1:68;
assume  n <= m ; ::_thesis: |.(((s (#) s1) . m) - 0c).| < p
then A11: |.((s . m) - 0c).| < p / R by A9;
A12: |.(((s (#) s1) . m) - 0c).| = |.((s . m) * (s1 . m)).| by VALUED_1:5
.= |.(s . m).| * |.(s1 . m).| by COMPLEX1:65 ;
A13: 0 <= |.(s1 . m).| by COMPLEX1:46;
now__::_thesis:_(_|.(s1_._m).|_<>_0_implies_|.(((s_(#)_s1)_._m)_-_0c).|_<_p_)
assume  |.(s1 . m).| <> 0 ; ::_thesis: |.(((s (#) s1) . m) - 0c).| < p
then  |.(((s (#) s1) . m) - 0c).| < (p / R) * |.(s1 . m).| by A11, A12, A13, XREAL_1:68;
hence  |.(((s (#) s1) . m) - 0c).| < p by A10, XXREAL_0:2; ::_thesis: verum
end;
hence  |.(((s (#) s1) . m) - 0c).| < p by A7, A12; ::_thesis: verum
end;
 s (#) s1 is convergent by A1, A2, A3, Th42;
hence  lim (s (#) s1) = 0c by A4, Def6; ::_thesis: verum
end;

theorem :: COMSEQ_2:44
canceled;

theorem :: COMSEQ_2:45
for s, s1 being Complex_Sequence st s is convergent & s1 is bounded & lim s = 0c holds
lim ((s (#) s1) *') = 0c
proof
let s, s1 be Complex_Sequence; ::_thesis: ( s is convergent & s1 is bounded & lim s = 0c implies lim ((s (#) s1) *') = 0c )
assume A1: ( s is convergent & s1 is bounded & lim s = 0c ) ; ::_thesis: lim ((s (#) s1) *') = 0c
then  s (#) s1 is convergent by Th42;
hence  lim ((s (#) s1) *') = (lim (s (#) s1)) *' by Th12
.= 0c by A1, Th43, COMPLEX1:28 ;
::_thesis: verum
end;