basel_1.miz

    begin

    reserve X for set;

    reserve k,m,n for Nat;

    reserve i for Integer;

    reserve a,b,c,d,e,g,p,r,x,y for Real;

    reserve z for Complex;

    set p = (( PI ^2 ) / 6);

    theorem :: BASEL_1:1



     Th1: 0 < a implies ex m st 0 < ((a * m) + b)

    proof

      assume

       A1: 0 < a;

      then

       A2: ((( - b) / a) * a) = ( - b) by XCMPLX_1: 87;

      consider m such that

       A3: ( - (b / a)) < m by SEQ_4: 3;

      take m;

      (( - (b / a)) * a) < (m * a) by A1, A3, XREAL_1: 68;

      then (( - b) + b) < ((a * m) + b) by A2, XREAL_1: 8;

      hence thesis;

    end;



     Lm1: for f be FinSequence, h be Function st ( dom h) = ( dom f) holds h is FinSequence

    proof

      let f be FinSequence, h be Function such that

       A1: ( dom h) = ( dom f);

      h is FinSequence-like

      proof

        take ( len f);

        thus thesis by A1, FINSEQ_1:def 3;

      end;

      hence thesis;

    end;



     Lm2: for f be FinSequence, y be object st y in ( rng f) holds ex n be Nat st 1 <= n <= ( len f) & y = (f . n)

    proof

      let f be FinSequence;

      let y be object;

      assume y in ( rng f);

      then

      consider n be object such that

       A1: n in ( dom f) and

       A2: (f . n) = y by FUNCT_1:def 3;

      reconsider n as Nat by A1;

      take n;

      thus thesis by A1, A2, FINSEQ_3: 25;

    end;



     Lm3: for f be complex-valued FinSequence holds ( len (f " )) = ( len f)

    proof

      let f be complex-valued FinSequence;

      ( dom (f " )) = ( dom f) by VALUED_1:def 7;

      hence thesis by FINSEQ_3: 29;

    end;

    registration

      let f be real-valued FinSequence;

      let n;

      cluster (f | n) -> REAL -valued;

      coherence ;

    end

    registration

      let f be complex-valued FinSequence;

      cluster (f ^2 ) -> ( len f) -element;

      coherence

      proof

        ( dom (f ^2 )) = ( dom f) by VALUED_1: 11;

        hence ( len (f ^2 )) = ( len f) by FINSEQ_3: 29;

      end;

      cluster (f " ) -> ( len f) -element;

      coherence

      proof

        ( dom (f " )) = ( dom f) by VALUED_1:def 7;

        hence ( len (f " )) = ( len f) by FINSEQ_3: 29;

      end;

    end

    registration

      let f be complex-valued FinSequence;

      let c be Complex;

      cluster (c + f) -> ( len f) -element;

      coherence

      proof

        ( dom (c + f)) = ( dom f) by VALUED_1:def 2;

        hence ( len (c + f)) = ( len f) by FINSEQ_3: 29;

      end;

    end

    theorem :: BASEL_1:2



     Th2: for c,z be Complex holds (c + <*z*>) = <*(c + z)*>

    proof

      let c,z be Complex;



       A1: ( len <*z*>) = 1 by FINSEQ_1: 39;



       A2: ( len <*(c + z)*>) = 1 by FINSEQ_1: 39;



       A3: ( len (c + <*z*>)) = ( len <*z*>) by CARD_1:def 7;

      thus ( len (c + <*z*>)) = ( len <*(c + z)*>) by A1, A2, CARD_1:def 7;

      let k such that

       A4: 1 <= k & k <= ( len (c + <*z*>));



       A5: k = 1 by A1, A3, A4, XXREAL_0: 1;

      k in ( dom (c + <*z*>)) by A4, FINSEQ_3: 25;



      hence ((c + <*z*>) . k) = (c + ( <*z*> . k)) by VALUED_1:def 2

      .= ( <*(c + z)*> . k) by A5;

    end;

    theorem :: BASEL_1:3



     Th3: for f,g be complex-valued FinSequence, c be Complex holds (c + (f ^ g)) = ((c + f) ^ (c + g))

    proof

      let f,g be complex-valued FinSequence;

      let c be Complex;



       A1: ( len (c + (f ^ g))) = ( len (f ^ g)) by CARD_1:def 7;



       A2: ( len (c + f)) = ( len f) by CARD_1:def 7;



       A3: ( len (c + g)) = ( len g) by CARD_1:def 7;



       A4: ( len (f ^ g)) = (( len f) + ( len g)) by FINSEQ_1: 22;



       A5: ( len ((c + f) ^ (c + g))) = (( len (c + f)) + ( len (c + g))) by FINSEQ_1: 22;

      hence ( len (c + (f ^ g))) = ( len ((c + f) ^ (c + g))) by A2, A3, A4, CARD_1:def 7;

      let k such that

       A6: 1 <= k and

       A7: k <= ( len (c + (f ^ g)));

      k in ( dom (c + (f ^ g))) by A6, A7, FINSEQ_3: 25;

      then

       A8: ((c + (f ^ g)) . k) = (c + ((f ^ g) . k)) by VALUED_1:def 2;

      per cases ;

        suppose

         A9: k <= ( len f);

        then

         A10: ((f ^ g) . k) = (f . k) by A6, FINSEQ_1: 64;

        k in ( dom (c + f)) by A2, A6, A9, FINSEQ_3: 25;



        hence ((c + (f ^ g)) . k) = ((c + f) . k) by A8, A10, VALUED_1:def 2

        .= (((c + f) ^ (c + g)) . k) by A2, A6, A9, FINSEQ_1: 64;

      end;

        suppose

         A11: k > ( len f);

        then

         A12: ((f ^ g) . k) = (g . (k - ( len f))) by A1, A7, FINSEQ_1: 24;



         A13: (( len f) - ( len f)) < (k - ( len f)) by A11, XREAL_1: 9;



         A14: (k - ( len f)) is Nat by A11, NAT_1: 21;

        then

         A15: ( 0 + 1) <= (k - ( len f)) by A13, NAT_1: 13;

        (k - ( len f)) <= ((( len f) + ( len g)) - ( len f)) by A1, A4, A7, XREAL_1: 9;

        then

         A16: (k - ( len f)) in ( dom (c + g)) by A14, A15, A3, FINSEQ_3: 25;



        thus ((c + (f ^ g)) . k) = ((c + g) . (k - ( len f))) by A8, A12, A16, VALUED_1:def 2

        .= (((c + f) ^ (c + g)) . k) by A1, A2, A3, A4, A5, A7, A11, FINSEQ_1: 24;

      end;

    end;

    theorem :: BASEL_1:4

    for f be complex-valued FinSequence, c be Complex holds ( Sum (c + f)) = ((c * ( len f)) + ( Sum f))

    proof

      let f be complex-valued FinSequence;

      let c be Complex;

      defpred P[ complex-valued FinSequence] means ( Sum (c + $1)) = ((c * ( len $1)) + ( Sum $1));



       A1: P[( <*> COMPLEX )];



       A2: for p be FinSequence of COMPLEX , x be Element of COMPLEX st P[p] holds P[(p ^ <*x*>)]

      proof

        let p be FinSequence of COMPLEX , x be Element of COMPLEX such that

         A3: ( Sum (c + p)) = ((c * ( len p)) + ( Sum p));

        set g = (p ^ <*x*>);



         A4: ( len <*x*>) = 1 by FINSEQ_1: 39;



         A5: ( len g) = (( len p) + ( len <*x*>)) by FINSEQ_1: 22;



         A6: (c + <*x*>) = <*(c + x)*> by Th2;



         A7: ( Sum g) = (( Sum p) + ( Sum <*x*>)) by RVSUM_2: 32;

        (c + g) = ((c + p) ^ (c + <*x*>)) by Th3;



        hence ( Sum (c + g)) = (( Sum (c + p)) + ( Sum (c + <*x*>))) by RVSUM_2: 32

        .= ((c * ( len g)) + ( Sum g)) by A3, A4, A5, A6, A7;

      end;



       A8: for p be FinSequence of COMPLEX holds P[p] from FINSEQ_2:sch 2( A1, A2);

      f is FinSequence of COMPLEX by RVSUM_1: 146;

      hence thesis by A8;

    end;

    begin

    definition

      let a,b,c,d be Complex;

      deffunc F( Nat) = (( Polynom (a,b,$1)) / ( Polynom (c,d,$1)));

      :: BASEL_1:def1

      func Rat_Exp_Seq (a,b,c,d) -> Complex_Sequence means

      : Def1: (it . n) = (( Polynom (a,b,n)) / ( Polynom (c,d,n)));

      existence

      proof

        ex f be Complex_Sequence st for n holds (f . n) = F(n) from COMSEQ_1:sch 1;

        hence thesis;

      end;

      uniqueness

      proof

        let f,f1 be Complex_Sequence such that

         A1: (f . n) = F(n) and

         A2: (f1 . n) = F(n);

        let n be Element of NAT ;



        thus (f . n) = F(n) by A1

        .= (f1 . n) by A2;

      end;

    end

    definition

      let a, b, c, d;

      :: BASEL_1:def2

      func rseq (a,b,c,d) -> Real_Sequence equals ( Re ( Rat_Exp_Seq (a,b,c,d)));

      coherence ;

    end

    theorem :: BASEL_1:5



     Th5: (( rseq (a,b,c,d)) . n) = (((a * n) + b) / ((c * n) + d))

    proof



       A1: ( dom ( Re ( Rat_Exp_Seq (a,b,c,d)))) = NAT & n in NAT by FUNCT_2:def 1, ORDINAL1:def 12;



      thus (( rseq (a,b,c,d)) . n) = ( Re (( Rat_Exp_Seq (a,b,c,d)) . n)) by COMSEQ_3:def 3, A1

      .= ( Re (( Polynom (a,b,n)) / ( Polynom (c,d,n)))) by Def1

      .= ( Re (((a * n) + b) / ( Polynom (c,d,n)))) by POLYEQ_1:def 1

      .= (((a * n) + b) / ((c * n) + d)) by POLYEQ_1:def 1;

    end;

    theorem :: BASEL_1:6



     Th6: (( rseq ( 0 ,b, 0 ,d)) . n) = (b / d)

    proof



      thus (( rseq ( 0 ,b, 0 ,d)) . n) = ((( 0 * n) + b) / (( 0 * n) + d)) by Th5

      .= (b / d);

    end;

    registration

      let a, b;

      cluster ( rseq (a,b, 0 , 0 )) -> constant;

      coherence

      proof

        set f = ( rseq (a,b, 0 , 0 ));

        let x,y be object;

        assume x in ( dom f) & y in ( dom f);

        then

        reconsider n = x, m = y as Nat;



        thus (f . x) = (((a * n) + b) / (( 0 * n) + 0 )) by Th5

        .= (((a * m) + b) / (( 0 * m) + 0 ))

        .= (f . y) by Th5;

      end;

    end

    registration

      let b, d;

      cluster ( rseq ( 0 ,b, 0 ,d)) -> constant;

      coherence

      proof

        set f = ( rseq ( 0 ,b, 0 ,d));

        let x,y be object such that

         A1: x in ( dom f) and

         A2: y in ( dom f);



        thus (f . x) = (b / d) by A1, Th6

        .= (f . y) by A2, Th6;

      end;

    end

    theorem :: BASEL_1:7



     Th7: ( rseq ( 0 ,b,c,d)) = (b (#) ( rseq ( 0 ,1,c,d))) & ( rseq ( 0 ,b,c,d)) = (( - b) (#) ( rseq ( 0 ,1,( - c),( - d))))

    proof

      thus ( rseq ( 0 ,b,c,d)) = (b (#) ( rseq ( 0 ,1,c,d)))

      proof

        set f1 = ( rseq ( 0 ,1,c,d));

        let n be Element of NAT ;



        thus (( rseq ( 0 ,b,c,d)) . n) = ((( 0 * n) + b) / ((c * n) + d)) by Th5

        .= (b * ((( 0 * n) + 1) / ((c * n) + d)))

        .= (b * (f1 . n)) by Th5

        .= ((b (#) f1) . n) by VALUED_1: 6;

      end;

      thus ( rseq ( 0 ,b,c,d)) = (( - b) (#) ( rseq ( 0 ,1,( - c),( - d))))

      proof

        set f1 = ( rseq ( 0 ,1,( - c),( - d)));

        let n be Element of NAT ;



        thus (( rseq ( 0 ,b,c,d)) . n) = ((( 0 * n) + b) / ((c * n) + d)) by Th5

        .= ((( - 1) * b) / (( - 1) * ((c * n) + d))) by XCMPLX_1: 91

        .= (( - b) * ((( 0 * n) + 1) / ((( - c) * n) + ( - d))))

        .= (( - b) * (f1 . n)) by Th5

        .= ((( - b) (#) f1) . n) by VALUED_1: 6;

      end;

    end;

    theorem :: BASEL_1:8



     Th8: ( rseq (a, 0 ,c,d)) = (a (#) ( rseq (1, 0 ,c,d))) & ( rseq (a, 0 ,c,d)) = (( - a) (#) ( rseq (1, 0 ,( - c),( - d))))

    proof

      thus ( rseq (a, 0 ,c,d)) = (a (#) ( rseq (1, 0 ,c,d)))

      proof

        set f = ( rseq (a, 0 ,c,d));

        set f1 = ( rseq (1, 0 ,c,d));

        let n be Element of NAT ;



         A1: (f1 . n) = (((1 * n) + 0 ) / ((c * n) + d)) by Th5;



        thus (f . n) = (((a * n) + 0 ) / ((c * n) + d)) by Th5

        .= (a * (((1 * n) + 0 ) / ((c * n) + d)))

        .= ((a (#) f1) . n) by A1, VALUED_1: 6;

      end;

      thus ( rseq (a, 0 ,c,d)) = (( - a) (#) ( rseq (1, 0 ,( - c),( - d))))

      proof

        set f = ( rseq (a, 0 ,c,d));

        set f1 = ( rseq (1, 0 ,( - c),( - d)));

        let n be Element of NAT ;



         A2: (f1 . n) = (((1 * n) + 0 ) / ((( - c) * n) + ( - d))) by Th5;



        thus (f . n) = (((a * n) + 0 ) / ((c * n) + d)) by Th5

        .= ((( - 1) * (a * n)) / (( - 1) * ((c * n) + d))) by XCMPLX_1: 91

        .= (( - a) * (((1 * n) + 0 ) / ((( - c) * n) + ( - d))))

        .= ((( - a) (#) f1) . n) by A2, VALUED_1: 6;

      end;

    end;



     Lm4: 0 < c implies for p st 0 < p holds ex n st for m st n <= m holds |.((( rseq ( 0 ,1,c,d)) . m) - 0 ).| < p

    proof

      set f = ( rseq ( 0 ,1,c,d));

      assume

       A1: 0 < c;

      let p such that

       A2: 0 < p;

      consider z be Nat such that

       A3: ((c * z) + d) > 0 by A1, Th1;

      consider n such that

       A4: n > ((1 - (p * d)) / (c * p)) by SEQ_4: 3;

      reconsider mm = ( max (n,z)) as Nat by TARSKI: 1;

      take mm;

      let m such that

       A5: mm <= m;



       A6: (f . m) = ((( 0 * m) + 1) / ((c * m) + d)) by Th5

      .= (1 / ((c * m) + d));

      mm >= z by XXREAL_0: 25;

      then m >= z by A5, XXREAL_0: 2;

      then (c * m) >= (c * z) by A1, XREAL_1: 64;

      then

       A7: ((c * m) + d) >= ((c * z) + d) by XREAL_1: 6;



       A8: ((p * ((c * m) + d)) / ((c * m) + d)) = p by A3, A7, XCMPLX_1: 89;



       A9: (((1 - (p * d)) / (c * p)) * (c * p)) = (1 - (p * d)) by A1, A2, XCMPLX_1: 87;

      mm >= n by XXREAL_0: 25;

      then ((1 - (p * d)) / (c * p)) < mm by A4, XXREAL_0: 2;

      then ((1 - (p * d)) / (c * p)) < m by A5, XXREAL_0: 2;

      then (((1 - (p * d)) / (c * p)) * (c * p)) < (m * (c * p)) by A1, A2, XREAL_1: 68;

      then ((1 - (p * d)) + (p * d)) < ((m * (c * p)) + (p * d)) by A9, XREAL_1: 8;

      then

       A10: (1 / ((c * m) + d)) < p by A8, A3, A7, XREAL_1: 74;

      ( - p) < 0 by A2;

      hence |.((f . m) - 0 ).| < p by A3, A7, A6, A10, SEQ_2: 1;

    end;



     Lm5: 0 < c implies ( rseq ( 0 ,1,c,d)) is convergent

    proof

      set f = ( rseq ( 0 ,1,c,d));

      assume

       A1: 0 < c;

      take 0 ;

      let p;

      assume 0 < p;

      then

      consider n such that

       A2: for m st n <= m holds |.((f . m) - 0 ).| < p by A1, Lm4;

      take n;

      thus thesis by A2;

    end;



     Lm6: ( rseq ( 0 ,1,c,d)) is convergent

    proof

      set f = ( rseq ( 0 ,1,c,d));

      per cases ;

        suppose c = 0 ;

        hence thesis;

      end;

        suppose c > 0 ;

        hence thesis by Lm5;

      end;

        suppose

         A1: c < 0 ;



         A2: ( rseq ( 0 ,1,c,d)) = (( - 1) (#) ( rseq ( 0 ,1,( - c),( - d)))) by Th7;

        ( rseq ( 0 ,1,( - c),( - d))) is convergent by A1, Lm5;

        hence thesis by A2;

      end;

    end;



     Lm7: 0 < c implies ( lim ( rseq ( 0 ,1,c,d))) = 0

    proof

      set f = ( rseq ( 0 ,1,c,d));

      assume

       A1: 0 < c;

      then

       A2: f is convergent by Lm5;

      for p st 0 < p holds ex n st for m st n <= m holds |.((f . m) - 0 ).| < p by A1, Lm4;

      hence thesis by A2, SEQ_2:def 7;

    end;



     Lm8: c < 0 implies ( lim ( rseq ( 0 ,1,c,d))) = 0

    proof

      set f = ( rseq ( 0 ,1,c,d));

      assume

       A1: c < 0 ;

      set f1 = ( rseq ( 0 ,1,( - c),( - d)));



       A2: f = (( - 1) (#) f1) by Th7;

      ( lim f1) = 0 by A1, Lm7;



      hence 0 = (( - 1) * ( lim f1))

      .= ( lim f) by A1, A2, Lm5, SEQ_2: 8;

    end;

    registration

      let b, c, d;

      cluster ( rseq ( 0 ,b,c,d)) -> convergent;

      coherence

      proof

        set f1 = ( rseq ( 0 ,1,c,d));



         A1: ( rseq ( 0 ,b,c,d)) = (b (#) f1)

        proof

          let n be Element of NAT ;

          (f1 . n) = ((( 0 * n) + 1) / ((c * n) + d)) by Th5;



          hence ((b (#) f1) . n) = ((( 0 * n) + b) / ((c * n) + d)) by VALUED_1: 6

          .= (( rseq ( 0 ,b,c,d)) . n) by Th5;

        end;

        f1 is convergent by Lm6;

        hence thesis by A1;

      end;

    end

    theorem :: BASEL_1:9

    ( lim ( rseq ( 0 ,b, 0 ,d))) = (b / d)

    proof



      thus ( lim ( rseq ( 0 ,b, 0 ,d))) = (( rseq ( 0 ,b, 0 ,d)) . 0 ) by SEQ_4: 26

      .= (b / d) by Th6;

    end;

    theorem :: BASEL_1:10



     Th10: for c be non zero Real holds ( lim ( rseq ( 0 ,b,c,d))) = 0

    proof

      let c be non zero Real;

      set f1 = ( rseq ( 0 ,1,c,d));



       A1: ( rseq ( 0 ,b,c,d)) = (b (#) f1)

      proof

        let n be Element of NAT ;

        (f1 . n) = ((( 0 * n) + 1) / ((c * n) + d)) by Th5;



        hence ((b (#) f1) . n) = ((( 0 * n) + b) / ((c * n) + d)) by VALUED_1: 6

        .= (( rseq ( 0 ,b,c,d)) . n) by Th5;

      end;

      c < 0 or 0 < c;

      then ( lim f1) = 0 by Lm7, Lm8;



      hence 0 = (b * ( lim f1))

      .= ( lim ( rseq ( 0 ,b,c,d))) by A1, SEQ_2: 8;

    end;



     Lm9: 0 < c implies for p st 0 < p holds ex n st for m st n <= m holds |.((( rseq (1, 0 ,c,d)) . m) - (1 / c)).| < p

    proof

      set f = ( rseq (1, 0 ,c,d));

      assume

       A1: 0 < c;

      let p such that

       A2: 0 < p;

      set f1 = ( rseq ( 0 ,( - d),(c * c),(c * d)));

      ( lim f1) = 0 by A1, Th10;

      then

      consider n such that

       A3: for m st n <= m holds |.((f1 . m) - 0 ).| < p by A2, SEQ_2:def 7;

      consider m1 be Nat such that

       A4: 0 < ((c * m1) + d) by A1, Th1;

      reconsider mm = ( max (m1,(n + 1))) as Nat by TARSKI: 1;

      take mm;

      let m such that

       A5: mm <= m;

      m1 <= mm by XXREAL_0: 25;

      then m1 <= m by A5, XXREAL_0: 2;

      then (c * m1) <= (c * m) by A1, XREAL_1: 64;

      then

       A6: ((c * m1) + d) <= ((c * m) + d) by XREAL_1: 6;



       A7: (n + 0 ) <= (n + 1) by XREAL_1: 6;

      (n + 1) <= mm by XXREAL_0: 25;

      then n <= mm by A7, XXREAL_0: 2;

      then

       A8: n <= m by A5, XXREAL_0: 2;

      ((f . m) - (1 / c)) = ((((1 * m) + 0 ) / ((c * m) + d)) - (1 / c)) by Th5

      .= (((m * c) - (1 * ((c * m) + d))) / (((c * m) + d) * c)) by A1, A6, A4, XCMPLX_1: 130

      .= ((( 0 * m) + ( - d)) / (((c * c) * m) + (c * d)))

      .= ((f1 . m) - 0 ) by Th5;

      hence |.((f . m) - (1 / c)).| < p by A3, A8;

    end;



     Lm10: 0 < c implies ( rseq (1, 0 ,c,d)) is convergent

    proof

      assume

       A1: 0 < c;

      take (1 / c);

      thus thesis by A1, Lm9;

    end;



     Lm11: 0 < c implies ( lim ( rseq (1, 0 ,c,d))) = (1 / c)

    proof

      assume

       A1: 0 < c;

      then

       A2: ( rseq (1, 0 ,c,d)) is convergent by Lm10;

      for p st 0 < p holds ex n st for m st n <= m holds |.((( rseq (1, 0 ,c,d)) . m) - (1 / c)).| < p by A1, Lm9;

      hence thesis by A2, SEQ_2:def 7;

    end;



     Lm12: for c be non zero Real holds ( rseq (1, 0 ,c,d)) is convergent

    proof

      let c be non zero Real;

      per cases ;

        suppose 0 < c;

        hence thesis by Lm10;

      end;

        suppose

         A1: c < 0 ;



         A2: ( rseq (1, 0 ,c,d)) = (( - 1) (#) ( rseq (1, 0 ,( - c),( - d)))) by Th8;

        ( rseq (1, 0 ,( - c),( - d))) is convergent by A1, Lm10;

        hence thesis by A2;

      end;

    end;



     Lm13: for c be non zero Real holds ( lim ( rseq (1, 0 ,c,d))) = (1 / c)

    proof

      let c be non zero Real;

      per cases ;

        suppose 0 < c;

        hence thesis by Lm11;

      end;

        suppose

         A1: c < 0 ;

        set f = ( rseq (1, 0 ,c,d));

        set f1 = ( rseq (1, 0 ,( - c),( - d)));



         A2: f = (( - 1) (#) f1) by Th8;

        ( lim f1) = (1 / ( - c)) by A1, Lm11;



        hence ( lim f) = (( - 1) / ( - c)) by A2, A1, Lm10, SEQ_2: 8

        .= (1 / c) by XCMPLX_1: 191;

      end;

    end;

    registration

      let c be non zero Real;

      let a, b, d;

      cluster ( rseq (a,b,c,d)) -> convergent;

      coherence

      proof

        set f2 = ( rseq (1, 0 ,c,d));

        set f3 = ( rseq ( 0 ,b,c,d));



         A1: ( rseq (a,b,c,d)) = ((a (#) f2) + f3)

        proof

          let n be Element of NAT ;



           A2: (f2 . n) = (((1 * n) + 0 ) / ((c * n) + d)) by Th5;



           A3: (f3 . n) = ((( 0 * n) + b) / ((c * n) + d)) by Th5;

          ((a (#) f2) . n) = (a * (f2 . n)) by VALUED_1: 6;



          hence (((a (#) f2) + f3) . n) = ((a * (f2 . n)) + (f3 . n)) by VALUED_1: 1

          .= (((a * n) + b) / ((c * n) + d)) by A2, A3

          .= (( rseq (a,b,c,d)) . n) by Th5;

        end;

        f2 is convergent by Lm12;

        hence thesis by A1;

      end;

    end

    registration

      let a,d be positive Real;

      let b be Real;

      cluster ( rseq (a,b, 0 ,d)) -> non bounded_above;

      coherence

      proof

        let r;



         A1: ((r * d) / d) = r by XCMPLX_1: 89;



         A2: ((((d * r) - b) / a) * a) = ((d * r) - b) by XCMPLX_1: 87;

        consider n such that

         A3: n > (((d * r) - b) / a) by SEQ_4: 3;

        take n;



         A4: (( rseq (a,b, 0 ,d)) . n) = (((a * n) + b) / (( 0 * n) + d)) by Th5;

        (a * n) >= ((a * ((d * r) - b)) / a) by A2, A3, XREAL_1: 64;

        then ((a * n) + b) >= (((d * r) - b) + b) by A2, XREAL_1: 6;

        hence thesis by A1, A4, XREAL_1: 72;

      end;

    end

    registration

      let a,d be negative Real;

      let b;

      cluster ( rseq (a,b, 0 ,d)) -> non bounded_above;

      coherence

      proof

        let r;



         A1: ((r * d) / d) = r by XCMPLX_1: 89;



         A2: ((((d * r) - b) / a) * a) = ((d * r) - b) by XCMPLX_1: 87;

        consider n such that

         A3: n > (((d * r) - b) / a) by SEQ_4: 3;

        take n;



         A4: (( rseq (a,b, 0 ,d)) . n) = (((a * n) + b) / (( 0 * n) + d)) by Th5;

        (a * n) <= ((a * ((d * r) - b)) / a) by A2, A3, XREAL_1: 65;

        then ((a * n) + b) <= (((d * r) - b) + b) by A2, XREAL_1: 6;

        hence thesis by A1, A4, XREAL_1: 73;

      end;

    end

    registration

      let a be positive Real;

      let b;

      let d be negative Real;

      cluster ( rseq (a,b, 0 ,d)) -> non bounded_below;

      coherence

      proof

        let r;



         A1: ((r * d) / d) = r by XCMPLX_1: 89;



         A2: ((((d * r) - b) / a) * a) = ((d * r) - b) by XCMPLX_1: 87;

        consider n such that

         A3: n > (((d * r) - b) / a) by SEQ_4: 3;

        take n;



         A4: (( rseq (a,b, 0 ,d)) . n) = (((a * n) + b) / (( 0 * n) + d)) by Th5;

        (a * n) >= ((d * r) - b) by A2, A3, XREAL_1: 64;

        then ((a * n) + b) >= (((d * r) - b) + b) by XREAL_1: 6;

        hence thesis by A1, A4, XREAL_1: 73;

      end;

    end

    registration

      let a be negative Real;

      let b;

      let d be positive Real;

      cluster ( rseq (a,b, 0 ,d)) -> non bounded_below;

      coherence

      proof

        let r;



         A1: ((r * d) / d) = r by XCMPLX_1: 89;



         A2: ((((d * r) - b) / a) * a) = ((d * r) - b) by XCMPLX_1: 87;

        consider n such that

         A3: n > (((d * r) - b) / a) by SEQ_4: 3;

        take n;



         A4: (( rseq (a,b, 0 ,d)) . n) = (((a * n) + b) / (( 0 * n) + d)) by Th5;

        (a * n) <= ((a * ((d * r) - b)) / a) by A2, A3, XREAL_1: 65;

        then ((a * n) + b) <= (((d * r) - b) + b) by A2, XREAL_1: 6;

        hence thesis by A1, A4, XREAL_1: 72;

      end;

    end

    registration

      let a,d be non zero Real;

      let b;

      cluster ( rseq (a,b, 0 ,d)) -> non bounded;

      coherence

      proof

        (a is positive or a is negative) & (d is positive or d is negative);

        hence thesis;

      end;

    end

    registration

      let a,d be non zero Real;

      let b;

      cluster ( rseq (a,b, 0 ,d)) -> non convergent;

      coherence ;

    end

    theorem :: BASEL_1:11



     Th11: for c be non zero Real holds ( lim ( rseq (a,b,c,d))) = (a / c)

    proof

      let c be non zero Real;

      set f2 = ( rseq (1, 0 ,c,d));

      set f3 = ( rseq ( 0 ,b,c,d));



       A1: ( rseq (a,b,c,d)) = ((a (#) f2) + f3)

      proof

        let n be Element of NAT ;



         A2: (f2 . n) = (((1 * n) + 0 ) / ((c * n) + d)) by Th5;



         A3: (f3 . n) = ((( 0 * n) + b) / ((c * n) + d)) by Th5;

        ((a (#) f2) . n) = (a * (f2 . n)) by VALUED_1: 6;



        hence (((a (#) f2) + f3) . n) = ((a * (f2 . n)) + (f3 . n)) by VALUED_1: 1

        .= (((a * n) + b) / ((c * n) + d)) by A2, A3

        .= (( rseq (a,b,c,d)) . n) by Th5;

      end;



       A4: ( lim f2) = (1 / c) by Lm13;



       A5: ( lim f3) = 0 by Th10;



      thus ( lim ( rseq (a,b,c,d))) = (( lim (a (#) f2)) + ( lim f3)) by A1, SEQ_2: 6

      .= (a / c) by A4, A5, SEQ_2: 8;

    end;

    theorem :: BASEL_1:12



     Th12: for a be non zero Real holds ( lim ( rseq (a,b,a,d))) = 1

    proof

      let a be non zero Real;



      thus ( lim ( rseq (a,b,a,d))) = (a / a) by Th11

      .= 1 by XCMPLX_1: 60;

    end;

    begin

    theorem :: BASEL_1:13

    ( sin ( PI * i)) = 0

    proof

      per cases ;

        suppose i is even;

        then

        consider j be Integer such that

         A1: i = (2 * j) by INT_1:def 3, ABIAN:def 1;



        thus ( sin ( PI * i)) = ( sin (((2 * PI ) * j) + 0 )) by A1

        .= 0 by SIN_COS: 31, COMPLEX2: 8;

      end;

        suppose i is odd;

        then

        consider j be Integer such that

         A2: i = ((2 * j) + 1) by ABIAN: 1;



        thus ( sin ( PI * i)) = ( sin (((2 * PI ) * j) + PI )) by A2

        .= 0 by SIN_COS: 77, COMPLEX2: 8;

      end;

    end;

    theorem :: BASEL_1:14



     Th14: ( cos (( PI / 2) + ( PI * i))) = 0

    proof

      per cases ;

        suppose i is even;

        then

        consider j be Integer such that

         A1: i = (2 * j) by INT_1:def 3, ABIAN:def 1;



        thus ( cos (( PI / 2) + ( PI * i))) = ( cos (( PI / 2) + ((2 * PI ) * j))) by A1

        .= ( cos ( PI / 2)) by COMPLEX2: 9

        .= 0 by SIN_COS: 76;

      end;

        suppose i is odd;

        then

        consider j be Integer such that

         A2: i = ((2 * j) + 1) by ABIAN: 1;



        thus ( cos (( PI / 2) + ( PI * i))) = ( cos (( PI + ( PI / 2)) + ((2 * PI ) * j))) by A2

        .= ( cos ( PI + ( PI / 2))) by COMPLEX2: 9

        .= 0 by SIN_COS: 76;

      end;

    end;

    theorem :: BASEL_1:15



     Th15: ( tan r) = (( cot r) " ) & ( cot r) = (( tan r) " )

    proof



      thus ( tan r) = (((( sin r) * (( cos r) " )) " ) " )

      .= (((( sin r) " ) * ((( cos r) " ) " )) " ) by XCMPLX_1: 204

      .= (( cot r) " );



      thus ( cot r) = (((( cos r) * (( sin r) " )) " ) " )

      .= (((( cos r) " ) * ((( sin r) " ) " )) " ) by XCMPLX_1: 204

      .= (( tan r) " );

    end;

    theorem :: BASEL_1:16



     Th16: ( dom tan ) = ( union the set of all ].(( - ( PI / 2)) + ( PI * i)), (( PI / 2) + ( PI * i)).[ where i be Integer)

    proof

      set S = the set of all ].(( - ( PI / 2)) + ( PI * i)), (( PI / 2) + ( PI * i)).[ where i be Integer;

      set T = ( dom tan );



       A1: ( dom sin ) = REAL & ( dom cos ) = REAL by FUNCT_2:def 1;

      then T = ( REAL /\ ( REAL \ ( cos " { 0 }))) by RFUNCT_1:def 1;

      then

       A2: T = ( REAL \ ( cos " { 0 })) by XBOOLE_1: 28;

      thus T c= ( union S)

      proof

        let x be object;

        assume

         A3: x in T;

        then

        reconsider x as Element of REAL ;

         not x in ( cos " { 0 }) by A2, A3, XBOOLE_0:def 5;

        then not ( cos x) in { 0 } by A1, FUNCT_1:def 7;

        then

         A4: ( cos x) <> 0 by TARSKI:def 1;

        set xP = ((x - ( PI / 2)) / PI ), E = [\xP/];



         A5: ].(( - ( PI / 2)) + ( PI * (E + 1))), (( PI / 2) + ( PI * (E + 1))).[ in S;

        (xP * PI ) = (x - ( PI / 2)) by XCMPLX_1: 87;

        then

         A6: x = (( PI / 2) + (xP * PI ));

        then

         A7: E <> xP by Th14, A4;

        E <= xP < (E + 1) by INT_1:def 6, INT_1: 29;

        then E < xP < (E + 1) by A7, XXREAL_0: 1;

        then (E * PI ) < (xP * PI ) < ((E + 1) * PI ) by XREAL_1: 68;

        then (( PI / 2) + (E * PI )) < x < (( PI / 2) + ((E + 1) * PI )) by A6, XREAL_1: 6;

        then x in ].(( - ( PI / 2)) + ( PI * (E + 1))), (( PI / 2) + ( PI * (E + 1))).[ by XXREAL_1: 4;

        hence thesis by A5, TARSKI:def 4;

      end;

      for X be set st X in S holds X c= T

      proof

        let X be set;

        assume X in S;

        then

        consider i be Integer such that

         A8: X = ].(( - ( PI / 2)) + ( PI * i)), (( PI / 2) + ( PI * i)).[;



         A9: (X /\ ( cos " { 0 })) = {}

        proof

          assume (X /\ ( cos " { 0 })) <> {} ;

          then

          consider r be object such that

           A10: r in (X /\ ( cos " { 0 })) by XBOOLE_0: 7;

          reconsider r as Element of REAL by A10;

          r in ( cos " { 0 }) by A10, XBOOLE_0:def 4;

          then

           A11: ( cos . r) in { 0 } by FUNCT_1:def 7;

          ( cos . r) <> 0

          proof



             A12: r in X by A10, XBOOLE_0:def 4;

            then

             A13: (( - ( PI / 2)) + ( PI * i)) < r < (( PI / 2) + ( PI * i)) by A8, XXREAL_1: 4;

            per cases ;

              suppose i is even;

              then

              consider j be Integer such that

               A14: i = (2 * j) by INT_1:def 3, ABIAN:def 1;

              ( - ( PI / 2)) < (r - ( PI * i)) < ( PI / 2) by A13, XREAL_1: 19, XREAL_1: 20;

              then (r - ( PI * i)) in ].( - ( PI / 2)), ( PI / 2).[ by XXREAL_1: 4;

              then ( cos (r + ((2 * PI ) * ( - j)))) > 0 by A14, COMPTRIG: 11;

              then ( cos r) > 0 by COMPLEX2: 9;

              hence thesis;

            end;

              suppose i is odd;

              then

              consider j be Integer such that

               A15: i = ((2 * j) + 1) by ABIAN: 1;

              ((( - ( PI / 2)) + PI ) + ((2 * PI ) * j)) < r < ((( PI / 2) + PI ) + ((2 * PI ) * j)) by A12, A8, XXREAL_1: 4, A15;

              then (( - ( PI / 2)) + PI ) < (r - ((2 * PI ) * j)) < (( PI / 2) + PI ) by XREAL_1: 19, XREAL_1: 20;

              then (r - ((2 * PI ) * j)) in ].( PI / 2), ((3 / 2) * PI ).[ by XXREAL_1: 4;

              then ( cos (r + ((2 * PI ) * ( - j)))) < 0 by COMPTRIG: 13;

              then ( cos r) < 0 by COMPLEX2: 9;

              hence thesis;

            end;

          end;

          hence contradiction by A11, TARSKI:def 1;

        end;

        (X \ ( cos " { 0 })) c= T by A8, A2, XBOOLE_1: 33;

        hence thesis by A9, XBOOLE_0:def 7, XBOOLE_1: 83;

      end;

      hence ( union S) c= T by ZFMISC_1: 76;

    end;

    registration

      cluster ( dom tan ) -> open;

      coherence

      proof

        set T = ( dom tan );

        for r be Element of REAL st r in T holds ex N be Neighbourhood of r st N c= T

        proof

          let r be Element of REAL ;

          assume r in T;

          then

          consider X be set such that

           A1: r in X & X in the set of all ].(( - ( PI / 2)) + ( PI * i)), (( PI / 2) + ( PI * i)).[ where i be Integer by Th16, TARSKI:def 4;

          consider i be Integer such that

           A2: X = ].(( - ( PI / 2)) + ( PI * i)), (( PI / 2) + ( PI * i)).[ by A1;

          consider N be Neighbourhood of r such that

           A3: N c= X by A1, A2, RCOMP_1: 18;

          X c= T by A1, Th16, ZFMISC_1: 74;

          hence thesis by A3, XBOOLE_1: 1;

        end;

        hence thesis by RCOMP_1: 20;

      end;

    end

    theorem :: BASEL_1:17



     Th17: 0 <= r implies ( sin . r) <= r

    proof

      assume 0 <= r;

      then

      reconsider A = [. 0 , r.] as non empty closed_interval Subset of REAL by MEASURE5:def 3, XXREAL_1: 1;



       A1: ( dom cos ) = REAL by FUNCT_2:def 1;

      then ( dom ( cos | A)) = A by RELAT_1: 62;

      then ( cos | A) is total by PARTFUN1:def 2;

      then

      reconsider cA = ( cos || A) as Function of A, REAL ;



       A2: (cA | A) is bounded & cA is integrable

      proof

        ( cos | A) is continuous;

        hence thesis by INTEGRA5:def 1, INTEGRA5: 11, INTEGRA5: 10, A1;

      end;



       A3: ( integral cA) = ( sin . r)

      proof



        thus ( integral cA) = ( integral ( cos ,A)) by INTEGRA5:def 2

        .= ( integral ( cos , 0 ,r)) by INTEGRA5: 19

        .= (( sin . r) - ( sin . 0 )) by INTEGRA7: 24

        .= ( sin . r) by SIN_COS: 30;

      end;

      set Z0 = ( #Z 0 );



       A4: ( dom Z0) = REAL by FUNCT_2:def 1;

      then ( dom (Z0 | A)) = A by RELAT_1: 62;

      then (Z0 | A) is total by PARTFUN1:def 2;

      then

      reconsider ZA = (Z0 || A) as Function of A, REAL ;



       A5: (ZA | A) is bounded & ZA is integrable

      proof

        (Z0 | A) is continuous;

        hence thesis by A4, INTEGRA5:def 1, INTEGRA5: 11, INTEGRA5: 10;

      end;



       A6: ( integral ZA) = r

      proof

        set Z1 = ( #Z 1);



         A7: (( 0 + 1) (#) Z0) = Z0 by RFUNCT_1: 21;



         A8: (Z1 . r) = (r #Z 1) by TAYLOR_1:def 1

        .= r by PREPOWER: 35;



         A9: (Z1 . 0 ) = ( 0 #Z 1) by TAYLOR_1:def 1

        .= 0 by PREPOWER: 35;



        thus ( integral ZA) = ( integral (Z0,A)) by INTEGRA5:def 2

        .= ( integral (Z0, 0 ,r)) by INTEGRA5: 19

        .= ((Z1 . r) - (Z1 . 0 )) by A7, INTEGRA7: 30

        .= r by A8, A9;

      end;

      for r st r in A holds (cA . r) <= (ZA . r)

      proof

        let r;

        assume

         A10: r in A;

        then (ZA . r) = (Z0 . r) by FUNCT_1: 49;



        then

         A11: (ZA . r) = (r #Z 0 ) by TAYLOR_1:def 1

        .= 1 by PREPOWER: 34;

        ( cos r) <= 1 by SIN_COS6: 6;

        hence thesis by A11, A10, FUNCT_1: 49;

      end;

      hence ( sin . r) <= r by A2, A3, A5, A6, INTEGRA2: 34;

    end;

    theorem :: BASEL_1:18



     Th18: 0 <= r < ( PI / 2) implies r <= ( tan . r)

    proof

      assume

       A1: 0 <= r < ( PI / 2);

      then

      reconsider A = [. 0 , r.] as non empty closed_interval Subset of REAL by MEASURE5:def 3, XXREAL_1: 1;



       A2: ( dom cos ) = REAL by FUNCT_2:def 1;

      set Z0 = ( #Z 0 );



       A3: ( dom Z0) = REAL by FUNCT_2:def 1;

      then ( dom (Z0 | A)) = A by RELAT_1: 62;

      then (Z0 | A) is total by PARTFUN1:def 2;

      then

      reconsider ZA = (Z0 || A) as Function of A, REAL ;



       A4: (ZA | A) is bounded & ZA is integrable

      proof

        (Z0 | A) is continuous;

        hence thesis by INTEGRA5:def 1, INTEGRA5: 11, INTEGRA5: 10, A3;

      end;



       A5: ( integral ZA) = r

      proof

        set Z1 = ( #Z 1);



         A6: (( 0 + 1) (#) Z0) = Z0 by RFUNCT_1: 21;



         A7: (Z1 . r) = (r #Z 1) by TAYLOR_1:def 1

        .= r by PREPOWER: 35;



         A8: (Z1 . 0 ) = ( 0 #Z 1) by TAYLOR_1:def 1

        .= 0 by PREPOWER: 35;



        thus ( integral ZA) = ( integral (Z0,A)) by INTEGRA5:def 2

        .= ( integral (Z0, 0 ,r)) by INTEGRA5: 19

        .= ((Z1 . r) - (Z1 . 0 )) by A6, INTEGRA7: 30

        .= r by A7, A8;

      end;

      set T = ( dom tan );

      ( dom sin ) = REAL by FUNCT_2:def 1;

      then T = ( REAL /\ (( dom cos ) \ ( cos " { 0 }))) by RFUNCT_1:def 1;

      then

       A9: T = ( REAL \ ( cos " { 0 })) by A2, XBOOLE_1: 28;

      set cc = ( cos (#) cos ), ccT = (cc | T), Z0ccT = (Z0 / ccT);

      ( dom cc) = REAL by FUNCT_2:def 1;

      then

       A10: ( dom ccT) = T by RELAT_1: 62;

      then

       A11: T = (( dom ccT) /\ ( dom Z0)) by A3, XBOOLE_1: 28;



       A12: A c= ].( - ( PI / 2)), ( PI / 2).[ by A1, XXREAL_1: 47;

      then

       A13: A c= T by SIN_COS9: 1;



       A14: (ccT " { 0 }) = {}

      proof

        assume (ccT " { 0 }) <> {} ;

        then

        consider x be object such that

         A15: x in (ccT " { 0 }) by XBOOLE_0:def 1;

        reconsider x as Element of REAL by A15;



         A16: x in ( dom ccT) & (ccT . x) in { 0 } by A15, FUNCT_1:def 7;



        then 0 = (ccT . x) by TARSKI:def 1

        .= (cc . x) by A16, FUNCT_1: 47

        .= (( cos . x) * ( cos . x)) by VALUED_1: 5;

        then ( cos . x) = 0 ;

        then ( cos . x) in { 0 } by TARSKI:def 1;

        then x in ( cos " { 0 }) by FUNCT_1:def 7, A2;

        hence contradiction by A9, A10, A16, XBOOLE_0:def 5;

      end;

      then (( dom ccT) \ (ccT " { 0 })) = ( dom ccT);

      then

       A17: T = ( dom Z0ccT) by A11, RFUNCT_1:def 1;

      then ( dom (Z0ccT | A)) = A by A13, RELAT_1: 62;

      then ((Z0ccT | A) | A) is total & ((Z0ccT | A) | A) = (Z0ccT | A) by PARTFUN1:def 2;

      then

      reconsider Z0ccTA = (Z0ccT || A) as Function of A, REAL ;



       A18: (Z0ccT | A) is continuous & (Z0ccTA | A) is bounded & Z0ccTA is integrable

      proof



         A19: A c= (( dom Z0) /\ ( dom ccT)) by A10, A13, A3, XBOOLE_1: 28;



         A20: (ccT | A) is continuous;

        (Z0 | A) is continuous;

        then (Z0ccT | A) is continuous by A19, FCONT_1: 24, A20, A14;

        hence thesis by INTEGRA5:def 1, INTEGRA5: 11, INTEGRA5: 10, A17, A13;

      end;



       A21: for s be Real st s in T holds (Z0ccT . s) = (1 / (( cos . s) ^2 )) & ( cos . s) <> 0

      proof

        let s be Real such that

         A22: s in T;



         A23: (Z0 . s) = (s #Z 0 ) by TAYLOR_1:def 1

        .= 1 by PREPOWER: 34;

        (ccT . s) = (cc . s) by A22, A10, FUNCT_1: 47

        .= (( cos . s) ^2 ) by VALUED_1: 5;

        hence (Z0ccT . s) = (1 / (( cos . s) ^2 )) by A23, RFUNCT_1:def 1, A22, A17;



         A24: s in REAL by XREAL_0:def 1;

        assume ( cos . s) = 0 ;

        then ( cos . s) in { 0 } by TARSKI:def 1;

        then s in ( cos " { 0 }) by FUNCT_1:def 7, A2, A24;

        hence thesis by A22, A9, XBOOLE_0:def 5;

      end;



       A25: ( integral Z0ccTA) = ( tan . r)

      proof



         A26: ( upper_bound A) = r & ( lower_bound A) = 0 by A1, JORDAN5A: 19;



        thus ( integral Z0ccTA) = ( integral (Z0ccT,A)) by INTEGRA5:def 2

        .= (( tan . r) - ( tan . 0 )) by A13, A17, A21, A18, A26, INTEGRA8: 59

        .= ( tan . r) by SIN_COS9: 41;

      end;

      for r st r in A holds (ZA . r) <= (Z0ccTA . r)

      proof

        let r;

        assume

         A27: r in A;

        then

         A28: (Z0ccTA . r) = (Z0ccT . r) & (ZA . r) = (Z0 . r) by FUNCT_1: 49;



        then

         A29: (ZA . r) = (r #Z 0 ) by TAYLOR_1:def 1

        .= 1 by PREPOWER: 34;



         A30: (Z0ccTA . r) = (1 / (( cos . r) ^2 )) by A28, A27, A21, A13;



         A31: ( cos r) > 0 by A27, A12, COMPTRIG: 11;

        ( cos r) <= 1 & ( cos . r) = ( cos r) by SIN_COS6: 6;

        then (( cos . r) ^2 ) <= (1 ^2 ) & (( cos . r) ^2 ) > 0 by XREAL_1: 66, A31;

        then (1 " ) <= ((( cos . r) ^2 ) " ) by XREAL_1: 85;

        hence thesis by A29, A30;

      end;

      hence r <= ( tan . r) by A4, A5, A18, A25, INTEGRA2: 34;

    end;

    begin

    definition

      let f be real-valued Function;

      :: BASEL_1:def3

      func cot (f) -> Function means

      : Def3: ( dom it ) = ( dom f) & for x be object st x in ( dom f) holds (it . x) = ( cot (f . x));

      existence

      proof

        deffunc F( object) = ( cot (f . $1));

        thus ex g be Function st ( dom g) = ( dom f) & for x be object st x in ( dom f) holds (g . x) = F(x) from FUNCT_1:sch 3;

      end;

      uniqueness

      proof

        let g,h be Function such that

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

         A2: for x be object st x in ( dom f) holds (g . x) = ( cot (f . x)) and

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

         A4: for x be object st x in ( dom f) holds (h . x) = ( cot (f . x));

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

        let x be object such that

         A5: x in ( dom g);



        thus (g . x) = ( cot (f . x)) by A1, A2, A5

        .= (h . x) by A1, A4, A5;

      end;

      :: BASEL_1:def4

      func cosec (f) -> Function means

      : Def4: ( dom it ) = ( dom f) & for x be object st x in ( dom f) holds (it . x) = ( cosec (f . x));

      existence

      proof

        deffunc F( object) = ( cosec (f . $1));

        thus ex g be Function st ( dom g) = ( dom f) & for x be object st x in ( dom f) holds (g . x) = F(x) from FUNCT_1:sch 3;

      end;

      uniqueness

      proof

        let g,h be Function such that

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

         A7: for x be object st x in ( dom f) holds (g . x) = ( cosec (f . x)) and

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

         A9: for x be object st x in ( dom f) holds (h . x) = ( cosec (f . x));

        thus ( dom g) = ( dom h) by A6, A8;

        let x be object such that

         A10: x in ( dom g);



        thus (g . x) = ( cosec (f . x)) by A6, A7, A10

        .= (h . x) by A6, A9, A10;

      end;

    end

    registration

      let f be real-valued Function;

      cluster ( cot f) -> REAL -valued;

      coherence

      proof

        set g = ( cot f);

        thus ( rng g) c= REAL

        proof

          let y be object;

          assume y in ( rng g);

          then

          consider x be object such that

           A1: x in ( dom g) and

           A2: y = (g . x) by FUNCT_1:def 3;

          ( dom g) = ( dom f) by Def3;

          then (g . x) = ( cot (f . x)) by A1, Def3;

          hence thesis by A2, XREAL_0:def 1;

        end;

      end;

      cluster ( cosec f) -> REAL -valued;

      coherence

      proof

        set g = ( cosec f);

        thus ( rng g) c= REAL

        proof

          let y be object;

          assume y in ( rng g);

          then

          consider x be object such that

           A3: x in ( dom g) and

           A4: y = (g . x) by FUNCT_1:def 3;

          ( dom g) = ( dom f) by Def4;

          then (g . x) = ( cosec (f . x)) by A3, Def4;

          hence thesis by A4, XREAL_0:def 1;

        end;

      end;

    end

    registration

      let f be real-valued FinSequence;

      cluster ( cot f) -> FinSequence-like;

      coherence

      proof

        ( dom ( cot f)) = ( dom f) by Def3;

        hence thesis by Lm1;

      end;

      cluster ( cosec f) -> FinSequence-like;

      coherence

      proof

        ( dom ( cosec f)) = ( dom f) by Def4;

        hence thesis by Lm1;

      end;

    end

    theorem :: BASEL_1:19



     Lm14: for f be real-valued FinSequence holds ( len ( cot f)) = ( len f)

    proof

      let f be real-valued FinSequence;

      ( dom ( cot f)) = ( dom f) by Def3;

      hence thesis by FINSEQ_3: 29;

    end;

    theorem :: BASEL_1:20



     Lm15: for f be real-valued FinSequence holds ( len ( cosec f)) = ( len f)

    proof

      let f be real-valued FinSequence;

      ( dom ( cosec f)) = ( dom f) by Def4;

      hence thesis by FINSEQ_3: 29;

    end;

    registration

      let f be real-valued FinSequence;

      cluster ( cot f) -> ( len f) -element;

      coherence

      proof

        ( dom ( cot f)) = ( dom f) by Def3;

        hence ( len ( cot f)) = ( len f) by FINSEQ_3: 29;

      end;

      cluster ( cosec f) -> ( len f) -element;

      coherence

      proof

        ( dom ( cosec f)) = ( dom f) by Def4;

        hence ( len ( cosec f)) = ( len f) by FINSEQ_3: 29;

      end;

    end



     Lm16: (( rseq ( 0 ,1,1, 0 )) . n) = (1 / n)

    proof



      thus (( rseq ( 0 ,1,1, 0 )) . n) = ((( 0 * n) + 1) / ((1 * n) + 0 )) by Th5

      .= (1 / n);

    end;



     Lm17: ( lim ( rseq (2, 0 ,2,1))) = 1 by Th12;



     Lm18: ( lim ( rseq (2,( - 1),2,1))) = 1 by Th12;



     Lm19: ( lim ( rseq (2,2,2,1))) = 1 by Th12;

    definition

      let m;

      :: BASEL_1:def5

      func x_r-seq (m) -> FinSequence equals (( PI / ((2 * m) + 1)) (#) ( idseq m));

      coherence ;

    end

    theorem :: BASEL_1:21



     Th19: ( len ( x_r-seq m)) = m & for k st 1 <= k <= m holds (( x_r-seq m) . k) = ((k * PI ) / ((2 * m) + 1))

    proof



       A1: ( dom ( x_r-seq m)) = ( dom ( idseq m)) by VALUED_1:def 5;

      hence ( len ( x_r-seq m)) = m by FINSEQ_3: 29;

      let k;

      assume 1 <= k <= m;

      then k in ( dom ( x_r-seq m)) & k in ( Seg m) by A1, FINSEQ_3: 25;

      then (( x_r-seq m) . k) = (( PI / ((2 * m) + 1)) * (( idseq m) . k)) & (( idseq m) . k) = k by VALUED_1:def 5, FINSEQ_2: 49;

      hence thesis;

    end;

    theorem :: BASEL_1:22



     Th20: ( rng ( x_r-seq m)) c= ]. 0 , ( PI / 2).[

    proof

      set f = ( x_r-seq m);

      let y be object;

      assume y in ( rng f);

      then

      consider n such that

       A1: 1 <= n and

       A2: n <= ( len f) and

       A3: y = (f . n) by Lm2;



       A4: ( len f) = m by Th19;

      then

       A5: (f . n) = ((n * PI ) / ((2 * m) + 1)) by A1, A2, Th19;

      (2 * n) <= (2 * m) by A2, A4, XREAL_1: 64;

      then ((2 * n) + 1) <= ((2 * m) + 1) by XREAL_1: 6;

      then

       A6: ((n * PI ) / ((2 * n) + 1)) >= ((n * PI ) / ((2 * m) + 1)) by XREAL_1: 118;



       A7: ((((2 * n) + 1) * (n " )) " ) = ((((2 * n) + 1) " ) * ((n " ) " )) by XCMPLX_1: 204;



       A8: ((2 * n) / n) = 2 by A1, XCMPLX_1: 89;

      (2 + (1 / n)) > (2 + 0 ) by A1, XREAL_1: 8;

      then ((((2 * n) + 1) * (n " )) " ) < ((2 * (1 " )) " ) by A8, XREAL_1: 88;

      then ( PI * (n / ((2 * n) + 1))) < ( PI * (1 / 2)) by A7, XREAL_1: 68;

      then ((n * PI ) / ((2 * m) + 1)) < ( PI / 2) by A6, XXREAL_0: 2;

      hence thesis by A1, A3, A5, XXREAL_1: 4;

    end;

    registration

      let m;

      cluster ( x_r-seq m) -> REAL -valued;

      coherence ;

    end

    theorem :: BASEL_1:23



     Th21: 1 <= k <= m implies 0 < (( x_r-seq m) . k) < ( PI / 2)

    proof

      set f = ( x_r-seq m);



       A1: ( rng f) c= ]. 0 , ( PI / 2).[ by Th20;



       A2: ( len f) = m by Th19;

      assume 1 <= k <= m;

      then k in ( dom f) by A2, FINSEQ_3: 25;

      then (f . k) in ( rng f) by FUNCT_1:def 3;

      hence thesis by A1, XXREAL_1: 4;

    end;

    registration

      cluster ( x_r-seq 0 ) -> empty;

      coherence ;

    end

    theorem :: BASEL_1:24

    1 <= k <= m implies ((2 / (k * PI )) + ((( x_r-seq m) " ) . k)) = ((( x_r-seq (m + 1)) " ) . k)

    proof

      assume that

       A1: 1 <= k and

       A2: k <= m;

      set f = ( x_r-seq m);

      set g = ( x_r-seq (m + 1));

      (m + 0 ) <= (m + 1) by XREAL_1: 6;

      then k <= (m + 1) by A2, XXREAL_0: 2;

      then

       A3: (g . k) = ((k * PI ) / ((2 * (m + 1)) + 1)) by A1, Th19;

      (f . k) = ((k * PI ) / ((2 * m) + 1)) by A1, A2, Th19;



      then (((2 * m) + 1) / (k * PI )) = ((f . k) " ) by XCMPLX_1: 213

      .= ((f " ) . k) by VALUED_1: 10;



      hence ((2 / (k * PI )) + ((f " ) . k)) = (((2 * (m + 1)) + 1) / (k * PI ))

      .= ((g . k) " ) by A3, XCMPLX_1: 213

      .= ((g " ) . k) by VALUED_1: 10;

    end;

    theorem :: BASEL_1:25

    1 <= k <= m implies (((2 * m) + 1) * (( x_r-seq m) . k)) = (k * PI )

    proof

      assume 1 <= k <= m;

      then

       A1: (( x_r-seq m) . k) = ((k * PI ) / ((2 * m) + 1)) by Th19;

      ((((2 * m) + 1) * (k * PI )) / ((2 * m) + 1)) = (k * PI ) by XCMPLX_1: 89;

      hence thesis by A1;

    end;

    theorem :: BASEL_1:26

    ( sqr ( cosec ( x_r-seq m))) = (1 + ( sqr ( cot ( x_r-seq m))))

    proof

      set f = ( x_r-seq m);



       A1: ( len ( sqr ( cosec f))) = ( len ( cosec f)) by CARD_1:def 7;



       A2: ( len ( cosec f)) = ( len f) by CARD_1:def 7;



       A3: ( len f) = m by Th19;



       A4: ( len (1 + ( sqr ( cot ( x_r-seq m))))) = ( len ( sqr ( cot ( x_r-seq m)))) by CARD_1:def 7;



       A5: ( len ( sqr ( cot ( x_r-seq m)))) = ( len ( cot ( x_r-seq m))) by CARD_1:def 7;



       A6: ( len ( cot ( x_r-seq m))) = ( len ( x_r-seq m)) by CARD_1:def 7;

      thus ( len ( sqr ( cosec f))) = ( len (1 + ( sqr ( cot ( x_r-seq m))))) by A1, A2, A4, A5, CARD_1:def 7;

      let k such that

       A7: 1 <= k and

       A8: k <= ( len ( sqr ( cosec f)));



       A9: k in ( dom f) by A1, A2, A7, A8, FINSEQ_3: 25;

      then

       A10: (( cosec f) . k) = ( cosec (f . k)) by Def4;



       A11: (( sqr ( cot f)) . k) = ((( cot f) . k) ^2 ) by VALUED_1: 11;



       A12: (( cot f) . k) = ( cot (f . k)) by A9, Def3;



       A13: 0 < (f . k) by A1, A2, A3, A7, A8, Th21;



       A14: (f . k) < ( PI / 2) by A1, A2, A3, A7, A8, Th21;

      ( PI / 2) < ( PI / 1) by XREAL_1: 76;

      then (f . k) < PI by A14, XXREAL_0: 2;

      then (f . k) in ]. 0 , PI .[ by A13, XXREAL_1: 4;

      then ( sin (f . k)) <> 0 by COMPTRIG: 7;

      then

       A15: (( cosec (f . k)) ^2 ) = (1 + (( cot (f . k)) ^2 )) by SIN_COS5: 14;

      k in ( dom (1 + ( sqr ( cot f)))) by A1, A2, A4, A5, A6, A7, A8, FINSEQ_3: 25;



      hence ((1 + ( sqr ( cot f))) . k) = ((( cosec f) . k) ^2 ) by A10, A11, A12, A15, VALUED_1:def 2

      .= (( sqr ( cosec f)) . k) by VALUED_1: 11;

    end;

    theorem :: BASEL_1:27



     Th25: ( x_r-seq n) is one-to-one

    proof

      set f = ( x_r-seq n);

      let x1,x2 be object such that

       A1: x1 in ( dom f) & x2 in ( dom f) & (f . x1) = (f . x2);

      reconsider x1, x2 as Nat by A1;

      ( len f) = n by Th19;

      then 1 <= x1 <= n & 1 <= x2 <= n by A1, FINSEQ_3: 25;

      then

       A2: (f . x1) = ((x1 * PI ) / ((2 * n) + 1)) & (f . x2) = ((x2 * PI ) / ((2 * n) + 1)) by Th19;

      (x1 * PI ) = (x2 * PI ) by A1, A2, XCMPLX_1: 53;

      hence thesis by XCMPLX_1: 5;

    end;

    theorem :: BASEL_1:28

    ( sqr ( cot ( x_r-seq n))) is one-to-one

    proof

      set f = ( x_r-seq n);



       A1: f is one-to-one by Th25;

      let x1,x2 be object such that

       A2: x1 in ( dom ( sqr ( cot f))) & x2 in ( dom ( sqr ( cot f))) & (( sqr ( cot f)) . x1) = (( sqr ( cot f)) . x2);

      reconsider x1, x2 as Nat by A2;



       A3: ( len ( sqr ( cot f))) = ( len ( cot f)) = ( len f) = n by CARD_1:def 7;

      then

       A4: ( dom ( sqr ( cot f))) = ( dom ( cot f)) = ( dom f) by FINSEQ_3: 29;

      1 <= x1 <= n & 1 <= x2 <= n by FINSEQ_3: 25, A3, A2;

      then

       A5: 0 < (f . x1) < ( PI / 2) & 0 < (f . x2) < ( PI / 2) & ( PI / 2) < PI by Th21, COMPTRIG: 5;

      then (f . x1) < PI & (f . x2) < PI by XXREAL_0: 2;

      then

       A6: (f . x1) in ]. 0 , PI .[ & (f . x2) in ]. 0 , PI .[ & (f . x1) in ]. 0 , ( PI / 2).[ & (f . x2) in ]. 0 , ( PI / 2).[ by A5, XXREAL_1: 4;

      then

       A7: ( sin (f . x1)) > 0 & ( sin (f . x2)) > 0 & ( cos (f . x1)) > 0 & ( cos (f . x2)) > 0 by COMPTRIG: 7, SIN_COS: 80;



       A8: (( cot f) . x1) = ( cot (f . x1)) & (( cot f) . x2) = ( cot (f . x2)) by Def3, A2, A4;



       A9: ( cot (f . x1)) = ( cot (f . x2))

      proof

        (( sqr ( cot f)) . x1) = ((( cot f) . x1) ^2 ) & (( sqr ( cot f)) . x2) = ((( cot f) . x2) ^2 ) by VALUED_1: 11;

        then (( cot f) . x1) = (( cot f) . x2) or (( cot f) . x1) = ( - (( cot f) . x2)) by A2, SQUARE_1: 40;

        hence thesis by A7, A8;

      end;

      (f . x1) = (f . x2)

      proof



         A10: ( cot . (f . x1)) = ( cot (f . x1)) & ( cot . (f . x2)) = ( cot (f . x2)) by A6, SIN_COS9: 2, RFUNCT_1:def 1;



         A11: (f . x1) in ( dom ( cot | ]. 0 , PI .[)) & (f . x2) in ( dom ( cot | ]. 0 , PI .[)) by A6, SIN_COS9: 2, RELAT_1: 57;

        then ( cot . (f . x1)) = (( cot | ]. 0 , PI .[) . (f . x1)) & ( cot . (f . x2)) = (( cot | ]. 0 , PI .[) . (f . x2)) by FUNCT_1: 47;

        hence thesis by A9, A10, A11, FUNCT_1:def 4, SIN_COS9: 10;

      end;

      hence thesis by A1, A2, A4, FUNCT_1:def 4;

    end;

    theorem :: BASEL_1:29

    ( Sum ( sqr ( cot ( x_r-seq m)))) <= ( Sum (( sqr ( x_r-seq m)) " ))

    proof

      set f = ( x_r-seq m);

      set f1 = ( sqr ( cot f));

      set f2 = (( sqr f) " );



       A1: ( len f) = m by Th19;



       A2: ( len ( cot f)) = ( len f) by Lm14;



       A3: ( len ( sqr f)) = ( len f) by RVSUM_1: 143;

      now

        let n;

        assume n in ( Seg m);

        then

         A4: 1 <= n & n <= m by FINSEQ_1: 1;

        then

         A5: n in ( dom f) by A1, FINSEQ_3: 25;



         A6: (f1 . n) = ((( cot f) . n) ^2 ) by VALUED_1: 11;



         A7: (( cot f) . n) = ( cot (f . n)) by A5, Def3;



         A8: (f2 . n) = ((( sqr f) . n) " ) by VALUED_1: 10;



         A9: (( sqr f) . n) = ((f . n) ^2 ) by VALUED_1: 11;



         A10: (( tan (f . n)) " ) = ( cot (f . n)) by Th15;



         A11: (f . n) < ( PI / 2) by A4, Th21;



         A12: 0 < (f . n) by A4, Th21;

        then

         A13: (f . n) in ].(( - ( PI / 2)) + ( PI * 0 )), (( PI / 2) + ( PI * 0 )).[ by A11, XXREAL_1: 4;

         ].(( - ( PI / 2)) + ( PI * 0 )), (( PI / 2) + ( PI * 0 )).[ in the set of all ].(( - ( PI / 2)) + ( PI * i)), (( PI / 2) + ( PI * i)).[ where i be Integer;

        then (f . n) in ( dom tan ) by A13, Th16, TARSKI:def 4;

        then ( tan . (f . n)) = ( tan (f . n)) by RFUNCT_1:def 1;

        then

         A14: ((( tan . (f . n)) ^2 ) " ) = (( cot (f . n)) ^2 ) by A10, XCMPLX_1: 204;

        (f . n) <= ( tan . (f . n)) by A4, A12, Th18, Th21;

        then ((f . n) ^2 ) <= (( tan . (f . n)) ^2 ) by A12, XREAL_1: 66;

        hence (f1 . n) <= (f2 . n) by A6, A7, A8, A9, A12, A14, XREAL_1: 85;

      end;

      hence thesis by A1, A2, A3, RVSUM_1: 82;

    end;

    theorem :: BASEL_1:30

    ( Sum (( sqr ( x_r-seq m)) " )) <= ( Sum ( sqr ( cosec ( x_r-seq m))))

    proof

      set f = ( x_r-seq m);

      set f1 = ( sqr ( cosec f));

      set f2 = (( sqr f) " );



       A1: ( len f) = m by Th19;



       A2: ( len ( cosec f)) = ( len f) by Lm15;



       A3: ( len ( sqr f)) = ( len f) by RVSUM_1: 143;

      now

        let n;

        assume n in ( Seg m);

        then

         A4: 1 <= n & n <= m by FINSEQ_1: 1;

        then

         A5: n in ( dom f) by A1, FINSEQ_3: 25;



         A6: (f1 . n) = ((( cosec f) . n) ^2 ) by VALUED_1: 11;



         A7: (( cosec f) . n) = ( cosec (f . n)) by A5, Def4;



         A8: (f2 . n) = ((( sqr f) . n) " ) by VALUED_1: 10;



         A9: (( sqr f) . n) = ((f . n) ^2 ) by VALUED_1: 11;



         A10: (f . n) < ( PI / 2) by A4, Th21;



         A11: 0 < (f . n) by A4, Th21;



         A12: ((( sin . (f . n)) ^2 ) " ) = (( cosec (f . n)) ^2 ) by XCMPLX_1: 204;

        ( PI / 2) < ( PI / 1) by XREAL_1: 76;

        then (f . n) < PI by A10, XXREAL_0: 2;

        then (f . n) in ]. 0 , PI .[ by A11, XXREAL_1: 4;

        then

         A13: 0 < ( sin (f . n)) by COMPTRIG: 7;

        ( sin . (f . n)) <= (f . n) by A11, Th17;

        then (( sin . (f . n)) ^2 ) <= ((f . n) ^2 ) by A13, XREAL_1: 66;

        hence (f2 . n) <= (f1 . n) by A6, A7, A8, A9, A12, A13, XREAL_1: 85;

      end;

      hence thesis by A1, A2, A3, RVSUM_1: 82;

    end;

    definition

      :: BASEL_1:def6

      func Basel-seq -> Real_Sequence equals (( rseq ( 0 ,1,1, 0 )) (#) ( rseq ( 0 ,1,1, 0 )));

      coherence ;

      :: BASEL_1:def7

      func Basel-seq1 -> Real_Sequence equals (((( PI ^2 ) / 6) (#) ( rseq (2, 0 ,2,1))) (#) ( rseq (2,( - 1),2,1)));

      coherence ;

      :: BASEL_1:def8

      func Basel-seq2 -> Real_Sequence equals (((( PI ^2 ) / 6) (#) ( rseq (2, 0 ,2,1))) (#) ( rseq (2,2,2,1)));

      coherence ;

    end

    theorem :: BASEL_1:31



     Th29: ( Basel-seq . n) = (1 / (n ^2 ))

    proof

      (( rseq ( 0 ,1,1, 0 )) . n) = (1 / n) by Lm16;



      hence ( Basel-seq . n) = ((1 / n) * (1 / n)) by VALUED_1: 5

      .= ((1 * 1) / (n * n)) by XCMPLX_1: 76

      .= (1 / (n ^2 ));

    end;

    theorem :: BASEL_1:32

    ( Basel-seq1 . n) = (((( PI ^2 ) / 6) * ((2 * n) / ((2 * n) + 1))) * (((2 * n) - 1) / ((2 * n) + 1)))

    proof



       A1: ((p (#) ( rseq (2, 0 ,2,1))) . n) = (p * (( rseq (2, 0 ,2,1)) . n)) by VALUED_1: 6;

      (( rseq (2, 0 ,2,1)) . n) = (((2 * n) + 0 ) / ((2 * n) + 1)) & (( rseq (2,( - 1),2,1)) . n) = (((2 * n) - 1) / ((2 * n) + 1)) by Th5;

      hence thesis by A1, VALUED_1: 5;

    end;

    theorem :: BASEL_1:33

    ( Basel-seq2 . n) = (((( PI ^2 ) / 6) * ((2 * n) / ((2 * n) + 1))) * (((2 * n) + 2) / ((2 * n) + 1)))

    proof



       A1: ((p (#) ( rseq (2, 0 ,2,1))) . n) = (p * (( rseq (2, 0 ,2,1)) . n)) by VALUED_1: 6;

      (( rseq (2, 0 ,2,1)) . n) = (((2 * n) + 0 ) / ((2 * n) + 1)) & (( rseq (2,2,2,1)) . n) = (((2 * n) + 2) / ((2 * n) + 1)) by Th5;

      hence thesis by A1, VALUED_1: 5;

    end;

    registration

      cluster Basel-seq -> convergent;

      coherence ;

      cluster Basel-seq1 -> convergent;

      coherence ;

      cluster Basel-seq2 -> convergent;

      coherence ;

    end

    theorem :: BASEL_1:34

    ( lim Basel-seq1 ) = (( PI ^2 ) / 6) = ( lim Basel-seq2 )

    proof

      ( lim (p (#) ( rseq (2, 0 ,2,1)))) = (p * ( lim ( rseq (2, 0 ,2,1)))) by SEQ_2: 8;

      hence ( lim Basel-seq1 ) = (( PI ^2 ) / 6) by Lm17, Lm18, SEQ_2: 15;

      ( lim (p (#) ( rseq (2, 0 ,2,1)))) = (p * ( lim ( rseq (2, 0 ,2,1)))) by SEQ_2: 8;

      hence thesis by Lm17, Lm19, SEQ_2: 15;

    end;

    theorem :: BASEL_1:35

    ( Sum (( sqr ( x_r-seq m)) " )) = (((((2 * m) + 1) ^2 ) / ( PI ^2 )) * ( Sum ( Basel-seq ,m)))

    proof

      set a = ( PI ^2 );

      set b = (((2 * m) + 1) ^2 );

      set B = Basel-seq ;

      set S = ( Shift ((B | ( Segm (m + 1))),1));

      set M = ( x_r-seq m);

      set G = (( sqr M) " );

      set F = ( <* 0 *> ^ G);



       A1: (B . 0 ) = (1 / ( 0 ^2 )) by Th29;



       A2: ( Sum (B,m)) = ( Sum S) by DBLSEQ_2: 49;



       A3: ( dom S) = ( Seg (m + 1)) by DBLSEQ_2: 45;



       A4: ( len G) = ( len ( sqr M)) by Lm3

      .= ( len M) by CARD_1:def 7

      .= m by Th19;



       A5: ( len F) = (( len <* 0 *>) + ( len G)) by FINSEQ_1: 22;



       A6: ( len <* 0 *>) = 1 by FINSEQ_1: 39;



       A7: F = ((b / a) (#) S)

      proof



        thus ( len F) = ( len S) by A4, A5, A6, A3, FINSEQ_1:def 3

        .= ( len ((b / a) (#) S)) by COMPLSP2: 3;

        let k such that

         A8: 1 <= k and

         A9: k <= ( len F);



         A10: (((b / a) (#) S) . k) = ((b / a) * (S . k)) by VALUED_1: 6;

        per cases by A8, XXREAL_0: 1;

          suppose

           A11: k = 1;

          1 <= (m + 1) by NAT_1: 11;

          then ( 0 + 1) in ( dom S) by A3;

          then (S . ( 0 + 1)) = (B . 0 ) by DBLSEQ_2: 47;

          hence (((b / a) (#) S) . k) = (F . k) by A1, A10, A11;

        end;

          suppose

           A12: 1 < k;

          reconsider s = (k - 1) as Nat by A8;



           A13: k = (s + 1);

          k in ( dom S) by A3, A4, A5, A6, A8, A9;



          then

           A14: (S . k) = (B . s) by A13, DBLSEQ_2: 47

          .= (1 / (s ^2 )) by Th29;



           A15: (( sqr M) . s) = ((M . s) ^2 ) by VALUED_1: 11;

          (1 - 1) < s by A12, XREAL_1: 8;

          then

           A16: 1 <= s by NAT_1: 14;

          s <= ((m + 1) - 1) by A4, A5, A6, A9, XREAL_1: 9;

          then

           A17: (M . s) = ((s * PI ) / ((2 * m) + 1)) by A16, Th19;



          thus (F . k) = (G . s) by A6, A9, A12, FINSEQ_1: 24

          .= ((( sqr M) . s) " ) by VALUED_1: 10

          .= ((((s * PI ) ^2 ) / (((2 * m) + 1) ^2 )) " ) by A15, A17, XCMPLX_1: 76

          .= (((((2 * m) + 1) ^2 ) * 1) / (( PI ^2 ) * ((k - 1) ^2 ))) by XCMPLX_1: 213

          .= ((b / a) * (S . k)) by A14, XCMPLX_1: 76

          .= (((b / a) (#) S) . k) by VALUED_1: 6;

        end;

      end;

      ( Sum F) = ( 0 + ( Sum G)) by RVSUM_1: 76;

      hence thesis by A2, A7, RVSUM_1: 87;

    end;