comseq_2.miz



    begin

    reserve n,n1,n2,m for Nat;

    reserve r,g1,g2,g,g9 for Complex;

    reserve R,R2 for Real;

    reserve s,s9,s1 for Complex_Sequence;

    theorem :: COMSEQ_2:1

    

     Th1: g <> 0c & r <> 0c implies |.((g " ) - (r " )).| = ( |.(g - r).| / ( |.g.| * |.r.|))

    proof

      assume

       A1: g <> 0c & r <> 0c ;

      

      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;

    end;

    theorem :: COMSEQ_2:2

    

     Th2: for n holds ex r be Real st 0 < r & for m st m <= n holds |.(s . m).| < r

    proof

      let n;

      defpred P[ Nat] means ex r be Real st 0 < r & for m st m <= $1 holds |.(s . m).| < r;

      

       A1: for n st P[n] holds P[(n + 1)]

      proof

        let n;

        given R1 be Real such that

         A2: 0 < R1 and

         A3: for m st m <= n holds |.(s . m).| < R1;

         A4:

        now

          assume

           A5: R1 <= |.(s . (n + 1)).|;

          take R = ( |.(s . (n + 1)).| + 1);

          ( 0 + 0 ) < R by COMPLEX1: 46, XREAL_1: 8;

          hence 0 < R;

          let m such that

           A6: m <= (n + 1);

           A7:

          now

            assume m <= n;

            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;

          end;

          now

            assume m = (n + 1);

            then ( |.(s . m).| + 0 ) < R by XREAL_1: 8;

            hence |.(s . m).| < R;

          end;

          hence |.(s . m).| < R by A6, A7, NAT_1: 8;

        end;

        now

          assume

           A8: |.(s . (n + 1)).| <= R1;

          take R = (R1 + 1);

          thus R > 0 by A2;

          let m such that

           A9: m <= (n + 1);

           A10:

          now

            assume m <= n;

            then

             A11: |.(s . m).| < R1 by A3;

            (R1 + 0 ) < R by XREAL_1: 8;

            hence |.(s . m).| < R by A11, XXREAL_0: 2;

          end;

          now

            

             A12: (R1 + 0 ) < R by XREAL_1: 8;

            assume m = (n + 1);

            hence |.(s . m).| < R by A8, A12, XXREAL_0: 2;

          end;

          hence |.(s . m).| < R by A9, A10, NAT_1: 8;

        end;

        hence thesis by A4;

      end;

      

       A13: P[ 0 ]

      proof

        take R = ( |.(s . 0 ).| + 1);

        ( 0 + 0 ) < ( |.(s . 0 ).| + 1) by COMPLEX1: 46, XREAL_1: 8;

        hence 0 < R;

        let m;

        assume m <= 0 ;

        then m = 0 ;

        then ( |.(s . m).| + 0 ) < R by XREAL_1: 8;

        hence thesis;

      end;

      for n holds P[n] from NAT_1:sch 2( A13, A1);

      then

      consider R be Real such that

       A14: R > 0 & for m st m <= n holds |.(s . m).| < R;

      thus thesis by A14;

    end;

    begin

    definition

      let f be complex-valued Function;

      deffunc F( object) = ((f . $1) *' );

      :: COMSEQ_2:def1

      func f *' -> complex-valued Function means

      : Def1: ( dom it ) = ( dom f) & for c be set st c in ( dom it ) holds (it . c) = ((f . c) *' );

      existence

      proof

        consider F be Function such that

         A1: ( dom F) = ( dom f) and

         A2: for x be object st x in ( dom f) holds (F . x) = F(x) from FUNCT_1:sch 3;

        for x be object st x in ( dom F) holds (F . x) is complex

        proof

          let x be object;

          assume x in ( dom F);

          then (F . x) = F(x) by A1, A2;

          hence thesis;

        end;

        then

        reconsider F as complex-valued Function by VALUED_0:def 7;

        take F;

        thus ( dom f) = ( dom F) by A1;

        thus thesis by A1, A2;

      end;

      uniqueness

      proof

        let h,g be complex-valued Function such that

         A3: ( dom h) = ( dom f) and

         A4: for c be set st c in ( dom h) holds (h . c) = F(c) and

         A5: ( dom g) = ( dom f) and

         A6: for c be set st c in ( dom g) holds (g . c) = F(c);

        thus ( dom h) = ( dom g) by A3, A5;

        let x be object;

        assume

         A7: x in ( dom h);

        

        hence (h . x) = F(x) by A4

        .= (g . x) by A3, A5, A6, A7;

      end;

      involutiveness

      proof

        let g,f be complex-valued Function;

        assume that

         A8: ( dom g) = ( dom f) and

         A9: for c be set st c in ( dom g) holds (g . c) = ((f . c) *' );

        thus ( dom f) = ( dom g) by A8;

        let c be set;

        assume

         A10: c in ( dom f);

        

        thus (f . c) = (((f . c) *' ) *' )

        .= ((g . c) *' ) by A8, A10, A9;

      end;

    end

    definition

      let C be non empty set;

      let f be Function of C, COMPLEX ;

      :: original: *'

      redefine

      :: COMSEQ_2:def2

      func f *' -> Function of C, COMPLEX means

      : Def2: for n be Element of C holds (it . n) = ((f . n) *' );

      coherence

      proof

        

         A1: ( dom (f *' )) = ( dom f) by Def1

        .= C by PARTFUN1:def 2;

        for x be object 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;

      end;

      compatibility

      proof

        let IT be Function of C, COMPLEX ;

        

         A2: ( dom IT) = C by FUNCT_2:def 1;

        hence IT = (f *' ) implies for c be Element of C holds (IT . c) = ((f . c) *' ) by Def1;

        assume

         A3: for c be Element of C holds (IT . c) = ((f . c) *' );

        

         A4: ( dom IT) = ( dom f) by A2, FUNCT_2:def 1;

        for c be set st c in ( dom IT) holds (IT . c) = ((f . c) *' ) by A3;

        hence IT = (f *' ) by A4, Def1;

      end;

    end

    registration

      let C be non empty set;

      let s be complex-valued ManySortedSet of C;

      cluster (s *' ) -> C -defined;

      coherence

      proof

        ( dom s) c= C;

        hence ( dom (s *' )) c= C by Def1;

      end;

    end

    registration

      let C be non empty set;

      let seq be complex-valued ManySortedSet of C;

      cluster (seq *' ) -> total;

      coherence

      proof

        let f be C -defined Function;

        assume f = (seq *' );

        

        hence ( dom f) = ( dom seq) by Def1

        .= C by PARTFUN1:def 2;

      end;

    end

    theorem :: COMSEQ_2:3

    s is non-zero implies (s *' ) is non-zero

    proof

      assume

       A1: s is non-zero;

      now

        let n be Element of NAT ;

        (s . n) <> 0 by A1, COMSEQ_1: 3;

        then ((s . n) *' ) <> 0c by COMPLEX1: 29;

        hence ((s *' ) . n) <> 0c by Def2;

      end;

      hence thesis by COMSEQ_1: 4;

    end;

    theorem :: COMSEQ_2:4

    ((r (#) s) *' ) = ((r *' ) (#) (s *' ))

    proof

      now

        let n be Element of NAT ;

        

        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;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: COMSEQ_2:5

    ((s (#) s9) *' ) = ((s *' ) (#) (s9 *' ))

    proof

      now

        let n be Element of NAT ;

        

        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;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: COMSEQ_2:6

    ((s *' ) " ) = ((s " ) *' )

    proof

      now

        let n be Element of NAT ;

        

        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;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: COMSEQ_2:7

    ((s9 /" s) *' ) = ((s9 *' ) /" (s *' ))

    proof

      now

        let n be Element of NAT ;

        

        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;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    begin

    definition

      let f be complex-valued Function;

      :: COMSEQ_2:def3

      attr f is bounded means ex r be Real st for y be set st y in ( dom f) holds |.(f . y).| < r;

    end

    definition

      let s;

      :: original: bounded

      redefine

      :: COMSEQ_2:def4

      attr s is bounded means ex r be Real st for n holds |.(s . n).| < r;

      compatibility

      proof

        thus s is bounded implies ex r be Real st for n holds |.(s . n).| < r

        proof

          given r be Real such that

           A1: for y be set st y in ( dom s) holds |.(s . y).| < r;

          reconsider r as Element of REAL by XREAL_0:def 1;

          take r;

          let n;

          n in NAT by ORDINAL1:def 12;

          then n in ( dom s) by FUNCT_2:def 1;

          hence thesis by A1;

        end;

        given r be Real such that

         A2: for n holds |.(s . n).| < r;

        take r;

        let y be set;

        assume y in ( dom s);

        hence thesis by A2;

      end;

    end

    set sc = ( NAT --> 0c );

    registration

      cluster bounded for Complex_Sequence;

      existence

      proof

        1 in NAT ;

        then

        reconsider j = 1 as Element of REAL by NUMBERS: 19;

        take sc, j;

        let n;

        n in NAT by ORDINAL1:def 12;

        hence thesis by COMPLEX1: 44, FUNCOP_1: 7;

      end;

    end

    theorem :: COMSEQ_2:8

    

     Th8: s is bounded iff ex r be Real st ( 0 < r & for n holds |.(s . n).| < r)

    proof

      thus s is bounded implies ex r be Real st ( 0 < r & for n holds |.(s . n).| < r)

      proof

        assume s is bounded;

        then

        consider r be Real such that

         A1: for n holds |.(s . n).| < r;

        take r;

        now

          let n;

           0 <= |.(s . n).| by COMPLEX1: 46;

          hence 0 < r by A1;

        end;

        hence thesis by A1;

      end;

      thus thesis;

    end;

    begin

    definition

      let s be complex-valued ManySortedSet of NAT ;

      :: COMSEQ_2:def5

      attr s is convergent means

      : Def5: ex g st for p be Real st 0 < p holds ex n st for m st n <= m holds |.((s . m) - g).| < p;

    end

    definition

      let s;

      assume

       A1: s is convergent;

      :: COMSEQ_2:def6

      func lim s -> Complex means

      : Def6: for p be Real st 0 < p holds ex n st for m st n <= m holds |.((s . m) - it ).| < p;

      existence by A1;

      uniqueness

      proof

        let g1, g2;

        assume that

         A2: for p be Real st 0 < p holds ex n1 st for m st n1 <= m holds |.((s . m) - g1).| < p and

         A3: for p be Real st 0 < p holds ex n2 st for m st n2 <= m holds |.((s . m) - g2).| < p and

         A4: g1 <> g2;

        reconsider p = ( |.(g1 - g2).| / 2) as Real;

        

         A5: |.(g1 - g2).| > 0 by A4, COMPLEX1: 62;

        then

        consider n1 such that

         A6: for m st n1 <= m holds |.((s . m) - g1).| < p by A2;

        consider n2 such that

         A7: for m st n2 <= m holds |.((s . m) - g2).| < p by A3, A5;

        reconsider n = ( max (n1,n2)) as Element of NAT by ORDINAL1:def 12;

        for m st n <= m holds (2 * p) < (2 * p)

        proof

          let m;

          assume

           A8: n <= m;

          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 thesis by A10, COMPLEX1: 60;

        end;

        hence contradiction;

      end;

    end

    theorem :: COMSEQ_2:9

    

     Th9: (ex g st for n be Nat holds (s . n) = g) implies s is convergent

    proof

      reconsider zz = 0 as Nat;

      given g such that

       A1: for n be Nat holds (s . n) = g;

      take g;

      now

        let p be Real such that

         A2: 0 < p;

        take k = zz;

        let n such that k <= n;

        (s . n) = g by A1;

        hence |.((s . n) - g).| < p by A2, COMPLEX1: 44;

      end;

      hence thesis;

    end;

    theorem :: COMSEQ_2:10

    

     Th10: for g st for n be Nat holds (s . n) = g holds ( lim s) = g

    proof

      let g;

      assume

       A1: for n be Nat holds (s . n) = g;

       A2:

      now

        let p be Real such that

         A3: 0 < p;

        reconsider zz = 0 as Nat;

        take k = zz;

        let n such that k <= n;

        (s . n) = g by A1;

        hence |.((s . n) - g).| < p by A3, COMPLEX1: 44;

      end;

      s is convergent by A1, Th9;

      hence thesis by A2, Def6;

    end;

    registration

      cluster convergent for Complex_Sequence;

      existence

      proof

        for n be Nat holds (sc . n) = 0c by ORDINAL1:def 12, FUNCOP_1: 7;

        hence thesis by Th9;

      end;

    end

    registration

      let s be convergent Complex_Sequence;

      cluster (s *' ) -> convergent;

      coherence

      proof

        let t be Complex_Sequence such that

         A1: t = (s *' );

        consider g such that

         A2: for p be Real st 0 < p holds ex n st for m st n <= m holds |.((s . m) - g).| < p by Def5;

        reconsider z = (g *' ) as Element of COMPLEX by XCMPLX_0:def 2;

        take r = z;

        let p be Real;

        assume 0 < p;

        then

        consider n such that

         A3: for m st n <= m holds |.((s . m) - g).| < p by A2;

        take n;

        let m such that

         A4: n <= m;

        m in NAT by ORDINAL1:def 12;

        

        then |.(((s *' ) . m) - r).| = |.(((s . m) *' ) - (g *' )).| by Def2

        .= |.(((s . m) - g) *' ).| by COMPLEX1: 34

        .= |.((s . m) - g).| by COMPLEX1: 53;

        hence thesis by A3, A4, A1;

      end;

    end

    ::$Canceled

    theorem :: COMSEQ_2:12

    

     Th11: s is convergent implies ( lim (s *' )) = (( lim s) *' )

    proof

      set g = ( lim s);

      assume

       A1: s is convergent;

      then

      reconsider s1 = s as convergent Complex_Sequence;

       A2:

      now

        let p be Real;

        assume 0 < p;

        then

        consider n such that

         A3: for m st n <= m holds |.((s . m) - g).| < p by A1, Def6;

        take n;

        let m such that

         A4: n <= m;

        m in NAT by ORDINAL1:def 12;

        

        then |.(((s *' ) . m) - (g *' )).| = |.(((s . m) *' ) - (g *' )).| by Def2

        .= |.(((s . m) - g) *' ).| by COMPLEX1: 34

        .= |.((s . m) - g).| by COMPLEX1: 53;

        hence |.(((s *' ) . m) - (( lim s) *' )).| < p by A3, A4;

      end;

      (s1 *' ) is convergent;

      hence thesis by A2, Def6;

    end;

    begin

    registration

      let s1,s2 be convergent Complex_Sequence;

      cluster (s1 + s2) -> convergent;

      coherence

      proof

        let s be Complex_Sequence such that

         A1: s = (s1 + s2);

        consider g such that

         A2: for p be Real st 0 < p holds ex n st for m st n <= m holds |.((s1 . m) - g).| < p by Def5;

        consider g9 such that

         A3: for p be Real st 0 < p holds ex n st for m st n <= m holds |.((s2 . m) - g9).| < p by Def5;

        take g1 = (g + g9);

        let p be Real;

        assume

         A4: p > 0 ;

        then

        consider n1 such that

         A5: for m st n1 <= m holds |.((s1 . m) - g).| < (p / 2) by A2;

        consider n2 such that

         A6: for m st n2 <= m holds |.((s2 . m) - g9).| < (p / 2) by A3, A4;

        reconsider n = ( max (n1,n2)) as Element of NAT by ORDINAL1:def 12;

        take n;

        let m such that

         A7: n <= m;

        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;

        m in NAT by ORDINAL1:def 12;

        

        then

         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 thesis by A1, XREAL_1: 6;

      end;

    end

    ::$Canceled

    theorem :: COMSEQ_2:14

    

     Th12: for s,s9 be convergent Complex_Sequence holds ( lim (s + s9)) = (( lim s) + ( lim s9))

    proof

      let s,s9 be convergent Complex_Sequence;

      for p be Real st 0 < p holds ex n st for m st n <= m holds |.(((s + s9) . m) - (( lim s) + ( lim s9))).| < p

      proof

        let p be Real;

        assume 0 < p;

        then

         A1: 0 < (p / 2);

        then

        consider n1 such that

         A2: for m st n1 <= m holds |.((s . m) - ( lim s)).| < (p / 2) by Def6;

        consider n2 such that

         A3: for m st n2 <= m holds |.((s9 . m) - ( lim s9)).| < (p / 2) by A1, Def6;

        reconsider n = ( max (n1,n2)) as Element of NAT by ORDINAL1:def 12;

        take n;

        let m such that

         A4: n <= m;

        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;

        m in NAT by ORDINAL1:def 12;

        

        then

         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 thesis by XREAL_1: 6;

      end;

      hence thesis by Def6;

    end;

    ::$Canceled

    theorem :: COMSEQ_2:16

    for s,s9 be convergent Complex_Sequence holds ( lim ((s + s9) *' )) = ((( lim s) *' ) + (( lim s9) *' ))

    proof

      let s,s9 be convergent Complex_Sequence;

      

      thus ( lim ((s + s9) *' )) = (( lim (s + s9)) *' ) by Th11

      .= ((( lim s) + ( lim s9)) *' ) by Th12

      .= ((( lim s) *' ) + (( lim s9) *' )) by COMPLEX1: 32;

    end;

    registration

      let s be convergent Complex_Sequence, c be Complex;

      cluster (c (#) s) -> convergent;

      coherence

      proof

         A1:

        now

          let c be Element of COMPLEX ;

          per cases ;

            suppose

             A2: c = 0c ;

            now

              let n;

              

              thus ((c (#) s) . n) = ( 0c * (s . n)) by A2, VALUED_1: 6

              .= 0c ;

            end;

            hence (c (#) s) is convergent by Th9;

          end;

            suppose

             A3: c <> 0c ;

            thus (c (#) s) is convergent

            proof

              consider g such that

               A4: for p be Real st 0 < p holds ex n st for m st n <= m holds |.((s . m) - g).| < p by Def5;

              take g9 = (c * g);

              let p be Real such that

               A5: 0 < p;

              

               A6: |.c.| > 0 by A3, COMPLEX1: 47;

              consider n such that

               A7: for m st n <= m holds |.((s . m) - g).| < (p / |.c.|) by A6, A4, A5;

              take n;

              let m;

              assume n <= m;

              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 thesis by A8;

            end;

          end;

        end;

        c in COMPLEX by XCMPLX_0:def 2;

        hence thesis by A1;

      end;

    end

    ::$Canceled

    theorem :: COMSEQ_2:18

    

     Th14: for s be convergent Complex_Sequence, r be Complex holds ( lim (r (#) s)) = (r * ( lim s))

    proof

      let s be convergent Complex_Sequence, r be Complex;

      reconsider r as Element of COMPLEX by XCMPLX_0:def 2;

      per cases ;

        suppose

         A1: r <> 0c ;

        for p be Real st p > 0 holds ex n st for m st n <= m holds |.(((r (#) s) . m) - (r * ( lim s))).| < p

        proof

          let p be Real such that

           A2: p > 0 ;

          

           A3: |.r.| > 0 by A1, COMPLEX1: 47;

          (p / |.r.|) > 0 by A3, A2;

          then

          consider n such that

           A4: for m st n <= m holds |.((s . m) - ( lim s)).| < (p / |.r.|) by Def6;

          take n;

          let m;

          assume n <= m;

          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 thesis by A5;

        end;

        hence thesis by Def6;

      end;

        suppose

         A6: r = 0c ;

        now

          let n;

          

          thus ((r (#) s) . n) = ( 0c * (s . n)) by A6, VALUED_1: 6

          .= 0c ;

        end;

        hence thesis by A6, Th10;

      end;

    end;

    ::$Canceled

    theorem :: COMSEQ_2:20

    for s be convergent Complex_Sequence holds ( lim ((r (#) s) *' )) = ((r *' ) * (( lim s) *' ))

    proof

      let s be convergent Complex_Sequence;

      

      thus ( lim ((r (#) s) *' )) = (( lim (r (#) s)) *' ) by Th11

      .= ((r * ( lim s)) *' ) by Th14

      .= ((r *' ) * (( lim s) *' )) by COMPLEX1: 35;

    end;

    registration

      let s be convergent Complex_Sequence;

      cluster ( - s) -> convergent;

      coherence ;

    end

    ::$Canceled

    theorem :: COMSEQ_2:22

    

     Th16: for s be convergent Complex_Sequence holds ( lim ( - s)) = ( - ( lim s))

    proof

      let s be convergent Complex_Sequence;

      ( lim ( - s)) = (( - 1) * ( lim s)) by Th14

      .= ( - ( 1r * ( lim s))) by COMPLEX1:def 4;

      hence thesis by COMPLEX1:def 4;

    end;

    ::$Canceled

    theorem :: COMSEQ_2:24

    for s be convergent Complex_Sequence holds ( lim (( - s) *' )) = ( - (( lim s) *' ))

    proof

      let s be convergent Complex_Sequence;

      

      thus ( lim (( - s) *' )) = (( lim ( - s)) *' ) by Th11

      .= (( - ( lim s)) *' ) by Th16

      .= ( - (( lim s) *' )) by COMPLEX1: 33;

    end;

    registration

      let s1,s2 be convergent Complex_Sequence;

      cluster (s1 - s2) -> convergent;

      coherence

      proof

        ( - s2) is convergent;

        hence thesis;

      end;

    end

    ::$Canceled

    theorem :: COMSEQ_2:26

    

     Th18: for s,s9 be convergent Complex_Sequence holds ( lim (s - s9)) = (( lim s) - ( lim s9))

    proof

      let s,s9 be convergent Complex_Sequence;

      ( lim (s - s9)) = (( lim s) + ( lim ( - s9))) by Th12

      .= (( lim s) + ( - ( lim s9))) by Th16;

      hence thesis;

    end;

    ::$Canceled

    theorem :: COMSEQ_2:28

    for s,s9 be convergent Complex_Sequence holds ( lim ((s - s9) *' )) = ((( lim s) *' ) - (( lim s9) *' ))

    proof

      let s,s9 be convergent Complex_Sequence;

      

      thus ( lim ((s - s9) *' )) = (( lim (s - s9)) *' ) by Th11

      .= ((( lim s) - ( lim s9)) *' ) by Th18

      .= ((( lim s) *' ) - (( lim s9) *' )) by COMPLEX1: 34;

    end;

    registration

      cluster convergent -> bounded for Complex_Sequence;

      coherence

      proof

        let s;

        assume s is convergent;

        then

        consider g such that

         A1: for p be Real st 0 < p holds ex n st for m st n <= m holds |.((s . m) - g).| < p;

        1 in NAT ;

        then

        reconsider j = 1 as Element of REAL by NUMBERS: 19;

        consider n1 such that

         A2: for m st n1 <= m holds |.((s . m) - g).| < j by A1;

        now

          take R = ( |.g.| + 1);

          ( 0 + 0 ) < R by COMPLEX1: 46, XREAL_1: 8;

          hence 0 < R;

          let m;

          

           A3: (( |.(s . m).| - |.g.|) + |.g.|) = |.(s . m).|;

          assume n1 <= m;

          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;

        end;

        then

        consider R1 be Real such that

         A5: 0 < R1 and

         A6: for m st n1 <= m holds |.(s . m).| < R1;

        consider R2 such that

         A7: 0 < R2 and

         A8: for m st m <= n1 holds |.(s . m).| < R2 by Th2;

        reconsider R = (R1 + R2) as Real;

        take R;

        let m;

        

         A9: (R2 + 0 ) < R by A5, XREAL_1: 8;

         A10:

        now

          assume m <= n1;

          then |.(s . m).| < R2 by A8;

          hence thesis by A9, XXREAL_0: 2;

        end;

        

         A11: (R1 + 0 ) < R by A7, XREAL_1: 8;

        now

          assume n1 <= m;

          then |.(s . m).| < R1 by A6;

          hence thesis by A11, XXREAL_0: 2;

        end;

        hence thesis by A10;

      end;

    end

    registration

      cluster non bounded -> non convergent for Complex_Sequence;

      coherence ;

    end

    registration

      let s1,s2 be convergent Complex_Sequence;

      cluster (s1 (#) s2) -> convergent;

      coherence

      proof

        let s be Complex_Sequence such that

         A1: s = (s1 (#) s2);

        consider g1 such that

         A2: for p be Real st 0 < p holds ex n st for m st n <= m holds |.((s1 . m) - g1).| < p by Def5;

        consider g2 such that

         A3: for p be Real st 0 < p holds ex n st for m st n <= m holds |.((s2 . m) - g2).| < p by Def5;

        take g = (g1 * g2);

        let p be Real;

        consider R such that

         A4: 0 < R and

         A5: for n holds |.(s1 . n).| < R by Th8;

        

         A6: ( 0 + 0 ) < ( |.g2.| + R) by A4, COMPLEX1: 46, XREAL_1: 8;

        assume

         A7: 0 < p;

        then

        consider n1 such that

         A8: for m st n1 <= m holds |.((s1 . m) - g1).| < (p / ( |.g2.| + R)) by A2, A6;

        consider n2 such that

         A9: for m st n2 <= m holds |.((s2 . m) - g2).| < (p / ( |.g2.| + R)) by A3, A6, A7;

        take n = (n1 + n2);

        let m such that

         A10: n <= m;

        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 thesis by A1, A13, XXREAL_0: 2;

      end;

    end

    ::$Canceled

    theorem :: COMSEQ_2:30

    

     Th20: for s,s9 be convergent Complex_Sequence holds ( lim (s (#) s9)) = (( lim s) * ( lim s9))

    proof

      let s,s9 be convergent Complex_Sequence;

      consider R such that

       A1: 0 < R and

       A2: for n 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

        let p be Real;

        assume 0 < p;

        then

         A5: 0 < (p / ( |.( lim s9).| + R)) by A3;

        then

        consider n1 such that

         A6: for m st n1 <= m holds |.((s . m) - ( lim s)).| < (p / ( |.( lim s9).| + R)) by Def6;

        consider n2 such that

         A7: for m st n2 <= m holds |.((s9 . m) - ( lim s9)).| < (p / ( |.( lim s9).| + R)) by A5, Def6;

        take n = (n1 + n2);

        let m such that

         A8: n <= m;

        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;

      end;

      hence thesis by Def6;

    end;

    ::$Canceled

    theorem :: COMSEQ_2:32

    for s,s9 be convergent Complex_Sequence holds ( lim ((s (#) s9) *' )) = ((( lim s) *' ) * (( lim s9) *' ))

    proof

      let s,s9 be convergent Complex_Sequence;

      

      thus ( lim ((s (#) s9) *' )) = (( lim (s (#) s9)) *' ) by Th11

      .= ((( lim s) * ( lim s9)) *' ) by Th20

      .= ((( lim s) *' ) * (( lim s9) *' )) by COMPLEX1: 35;

    end;

    theorem :: COMSEQ_2:33

    

     Th22: for s be convergent Complex_Sequence st ( lim s) <> 0c holds ex n st for m st n <= m holds ( |.( lim s).| / 2) < |.(s . m).|

    proof

      let s be convergent Complex_Sequence such that

       A1: ( lim s) <> 0c ;

       0 < |.( lim s).| by A1, COMPLEX1: 47;

      then 0 < ( |.( lim s).| / 2);

      then

      consider n1 such that

       A2: for m st n1 <= m holds |.((s . m) - ( lim s)).| < ( |.( lim s).| / 2) by Def6;

      take n = n1;

      let m;

      assume n <= 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 thesis by A5, XREAL_1: 6;

    end;

    theorem :: COMSEQ_2:34

    

     Th23: for s be convergent Complex_Sequence st ( lim s) <> 0c & s is non-zero holds (s " ) is convergent

    proof

      let s be convergent Complex_Sequence;

      assume that

       A1: ( lim s) <> 0c and

       A2: s is non-zero;

      consider n1 such that

       A3: for m st n1 <= m holds ( |.( lim s).| / 2) < |.(s . m).| by A1, Th22;

      take (( lim s) " );

      let p be Real;

      assume

       A4: 0 < 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 such that

       A6: for m st n2 <= m holds |.((s . m) - ( lim s)).| < (p * (( |.( lim s).| * |.( lim s).|) / 2)) by Def6;

      take n = (n1 + n2);

      let m such that

       A7: n <= m;

      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;

      m in NAT by ORDINAL1:def 12;

      then

       A15: (s . m) <> 0 by A2, COMSEQ_1: 3;

      then ((s . m) * ( lim s)) <> 0c by A1;

      then 0 < |.((s . m) * ( lim s)).| by COMPLEX1: 47;

      then

       A16: 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

       A17: ( |.((s . m) - ( lim s)).| / ( |.(s . m).| * |.( lim s).|)) < ((p * (( |.( lim s).| * |.( lim s).|) / 2)) / ( |.(s . m).| * |.( lim s).|)) by A16, 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, Th1, A15;

      hence thesis by A17, A14, A10, A12, XXREAL_0: 2;

    end;

    theorem :: COMSEQ_2:35

    

     Th24: s is convergent & ( lim s) <> 0c & s is non-zero implies ( lim (s " )) = (( lim s) " )

    proof

      assume that

       A1: s is convergent and

       A2: ( lim s) <> 0c and

       A3: s is non-zero;

      consider n1 such that

       A4: for m st n1 <= m holds ( |.( lim s).| / 2) < |.(s . m).| by A1, A2, Th22;

      

       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

        let p be Real;

        

         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;

        then ( 0 * 0 ) < (p * (( |.( lim s).| * |.( lim s).|) / 2)) by A6;

        then

        consider n2 such that

         A12: for m st n2 <= m holds |.((s . m) - ( lim s)).| < (p * (( |.( lim s).| * |.( lim s).|) / 2)) by A1, Def6;

        take n = (n1 + n2);

        let m such that

         A13: n <= m;

        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;

        m in NAT by ORDINAL1:def 12;

        then

         A18: (s . m) <> 0 by A3, COMSEQ_1: 3;

        then ((s . m) * ( lim s)) <> 0c by A2;

        then 0 < |.((s . m) * ( lim s)).| by COMPLEX1: 47;

        then

         A19: 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

         A20: ( |.((s . m) - ( lim s)).| / ( |.(s . m).| * |.( lim s).|)) < ((p * (( |.( lim s).| * |.( lim s).|) / 2)) / ( |.(s . m).| * |.( lim s).|)) by A19, 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, Th1, A18;

        hence |.(((s " ) . m) - (( lim s) " )).| < p by A20, A17, A16, A10, XXREAL_0: 2;

      end;

      (s " ) is convergent by A1, A2, A3, Th23;

      hence thesis by A8, Def6;

    end;

    ::$Canceled

    theorem :: COMSEQ_2:37

    s is convergent & ( lim s) <> 0c & s is non-zero implies ( lim ((s " ) *' )) = ((( lim s) *' ) " )

    proof

      assume

       A1: s is convergent & ( lim s) <> 0c & s is non-zero;

      then (s " ) is convergent by Th23;

      

      hence ( lim ((s " ) *' )) = (( lim (s " )) *' ) by Th11

      .= ((( lim s) " ) *' ) by A1, Th24

      .= ((( lim s) *' ) " ) by COMPLEX1: 36;

    end;

    theorem :: COMSEQ_2:38

    

     Th26: s9 is convergent & s is convergent & ( lim s) <> 0c & s is non-zero implies (s9 /" s) is convergent

    proof

      assume that

       A1: s9 is convergent and

       A2: s is convergent & ( lim s) <> 0c & s is non-zero;

      (s " ) is convergent by A2, Th23;

      hence thesis by A1;

    end;

    theorem :: COMSEQ_2:39

    

     Th27: s9 is convergent & s is convergent & ( lim s) <> 0c & s is non-zero implies ( lim (s9 /" s)) = (( lim s9) / ( lim s))

    proof

      assume that

       A1: s9 is convergent and

       A2: s is convergent & ( lim s) <> 0c & s is non-zero;

      (s " ) is convergent by A2, Th23;

      

      then ( lim (s9 (#) (s " ))) = (( lim s9) * ( lim (s " ))) by A1, Th20

      .= (( lim s9) * (( lim s) " )) by A2, Th24

      .= (( lim s9) / ( lim s)) by XCMPLX_0:def 9;

      hence thesis;

    end;

    ::$Canceled

    theorem :: COMSEQ_2:41

    s9 is convergent & s is convergent & ( lim s) <> 0c & s is non-zero implies ( lim ((s9 /" s) *' )) = ((( lim s9) *' ) / (( lim s) *' ))

    proof

      assume

       A1: s9 is convergent & s is convergent & ( lim s) <> 0c & s is non-zero;

      then (s9 /" s) is convergent by Th26;

      

      hence ( lim ((s9 /" s) *' )) = (( lim (s9 /" s)) *' ) by Th11

      .= ((( lim s9) / ( lim s)) *' ) by A1, Th27

      .= ((( lim s9) *' ) / (( lim s) *' )) by COMPLEX1: 37;

    end;

    theorem :: COMSEQ_2:42

    

     Th29: s is convergent & s1 is bounded & ( lim s) = 0c implies (s (#) s1) is convergent

    proof

      assume that

       A1: s is convergent and

       A2: s1 is bounded and

       A3: ( lim s) = 0c ;

      take g = 0c ;

      consider R such that

       A4: 0 < R and

       A5: for m holds |.(s1 . m).| < R by A2, Th8;

      let p be Real such that

       A6: 0 < p;

      

       A7: 0 < (p / R) by A6, A4;

      then

      consider n1 such that

       A8: for m st n1 <= m holds |.((s . m) - 0c ).| < (p / R) by A1, A3, Def6;

      take n = n1;

      let m such that

       A9: n <= m;

      

       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

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

        then |.(((s (#) s1) . m) - g).| < ((p / R) * |.(s1 . m).|) by A11, A10, A13, XREAL_1: 68;

        hence thesis by A12, XXREAL_0: 2;

      end;

      hence thesis by A6, A10;

    end;

    theorem :: COMSEQ_2:43

    

     Th30: s is convergent & s1 is bounded & ( lim s) = 0c implies ( lim (s (#) s1)) = 0c

    proof

      assume that

       A1: s is convergent and

       A2: s1 is bounded and

       A3: ( lim s) = 0c ;

       A4:

      now

        consider R such that

         A5: 0 < R and

         A6: for m holds |.(s1 . m).| < R by A2, Th8;

        let p be Real such that

         A7: 0 < p;

        

         A8: 0 < (p / R) by A7, A5;

        then

        consider n1 such that

         A9: for m st n1 <= m holds |.((s . m) - 0c ).| < (p / R) by A1, A3, Def6;

        take n = n1;

        let m;

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

        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

          assume |.(s1 . m).| <> 0 ;

          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;

        end;

        hence |.(((s (#) s1) . m) - 0c ).| < p by A7, A12;

      end;

      (s (#) s1) is convergent by A1, A2, A3, Th29;

      hence thesis by A4, Def6;

    end;

    ::$Canceled

    theorem :: COMSEQ_2:45

    s is convergent & s1 is bounded & ( lim s) = 0c implies ( lim ((s (#) s1) *' )) = 0c

    proof

      assume

       A1: s is convergent & s1 is bounded & ( lim s) = 0c ;

      then (s (#) s1) is convergent by Th29;

      

      hence ( lim ((s (#) s1) *' )) = (( lim (s (#) s1)) *' ) by Th11

      .= 0c by A1, Th30, COMPLEX1: 28;

    end;