let m be Nat; :: thesis: Sum ((sqr (x_r-seq m)) ") = ((((2 * m) + 1) ^2) / (PI ^2)) * (Sum (Basel-seq,m))
set a = PI ^2 ;
set b = ((2 * m) + 1) ^2 ;
set B = Basel-seq ;
set S = Shift ((Basel-seq | (Segm (m + 1))),1);
set M = x_r-seq m;
set G = (sqr (x_r-seq m)) " ;
set F = <*0*> ^ ((sqr (x_r-seq m)) ");
A1: Basel-seq . 0 = 1 / (0 ^2) by Th29;
A2: Sum (Basel-seq,m) = Sum (Shift ((Basel-seq | (Segm (m + 1))),1)) by DBLSEQ_2:49;
A3: dom (Shift ((Basel-seq | (Segm (m + 1))),1)) = Seg (m + 1) by DBLSEQ_2:45;
A4: len ((sqr (x_r-seq m)) ") = len (sqr (x_r-seq m)) by Lm3
.= len (x_r-seq m) by CARD_1:def 7
.= m by Th19 ;
A5: len (<*0*> ^ ((sqr (x_r-seq m)) ")) = (len <*0*>) + (len ((sqr (x_r-seq m)) ")) by FINSEQ_1:22;
A6: len <*0*> = 1 by FINSEQ_1:39;
A7: <*0*> ^ ((sqr (x_r-seq m)) ") = ((((2 * m) + 1) ^2) / (PI ^2)) (#) (Shift ((Basel-seq | (Segm (m + 1))),1))

proof

thus len (<*0*> ^ ((sqr (x_r-seq m)) ")) = len (Shift ((Basel-seq | (Segm (m + 1))),1)) by A4, A5, A6, A3, FINSEQ_1:def 3
.= len (((((2 * m) + 1) ^2) / (PI ^2)) (#) (Shift ((Basel-seq | (Segm (m + 1))),1))) by COMPLSP2:3 ; :: according to FINSEQ_1:def 18 :: thesis: for b₁ being set holds
( not 1 <= b₁ or not b₁ <= len (<*0*> ^ ((sqr (x_r-seq m)) ")) or (<*0*> ^ ((sqr (x_r-seq m)) ")) . b₁ = (((((2 * m) + 1) ^2) / (PI ^2)) (#) (Shift ((Basel-seq | (Segm (m + 1))),1))) . b₁ )
let k be Nat; :: thesis: ( not 1 <= k or not k <= len (<*0*> ^ ((sqr (x_r-seq m)) ")) or (<*0*> ^ ((sqr (x_r-seq m)) ")) . k = (((((2 * m) + 1) ^2) / (PI ^2)) (#) (Shift ((Basel-seq | (Segm (m + 1))),1))) . k )
assume that
A8: 1 <= k and
A9: k <= len (<*0*> ^ ((sqr (x_r-seq m)) ")) ; :: thesis: (<*0*> ^ ((sqr (x_r-seq m)) ")) . k = (((((2 * m) + 1) ^2) / (PI ^2)) (#) (Shift ((Basel-seq | (Segm (m + 1))),1))) . k
A10: (((((2 * m) + 1) ^2) / (PI ^2)) (#) (Shift ((Basel-seq | (Segm (m + 1))),1))) . k = ((((2 * m) + 1) ^2) / (PI ^2)) * ((Shift ((Basel-seq | (Segm (m + 1))),1)) . k) by VALUED_1:6;

per cases ( k = 1 or 1 < k ) by A8, XXREAL_0:1;

suppose A11: k = 1 ; :: thesis: (<*0*> ^ ((sqr (x_r-seq m)) ")) . k = (((((2 * m) + 1) ^2) / (PI ^2)) (#) (Shift ((Basel-seq | (Segm (m + 1))),1))) . k

1 <= m + 1 by NAT_1:11;
then 0 + 1 in dom (Shift ((Basel-seq | (Segm (m + 1))),1)) by A3;
then (Shift ((Basel-seq | (Segm (m + 1))),1)) . (0 + 1) = Basel-seq . 0 by DBLSEQ_2:47;
hence (((((2 * m) + 1) ^2) / (PI ^2)) (#) (Shift ((Basel-seq | (Segm (m + 1))),1))) . k = (<*0*> ^ ((sqr (x_r-seq m)) ")) . k by A1, A10, A11; :: thesis: verum

end;

suppose A12: 1 < k ; :: thesis: (<*0*> ^ ((sqr (x_r-seq m)) ")) . k = (((((2 * m) + 1) ^2) / (PI ^2)) (#) (Shift ((Basel-seq | (Segm (m + 1))),1))) . k

reconsider s = k - 1 as Nat by A8;
A13: k = s + 1 ;
k in dom (Shift ((Basel-seq | (Segm (m + 1))),1)) by A3, A4, A5, A6, A8, A9;
then A14: (Shift ((Basel-seq | (Segm (m + 1))),1)) . k = Basel-seq . s by A13, DBLSEQ_2:47
.= 1 / (s ^2) by Th29 ;
A15: (sqr (x_r-seq m)) . s = ((x_r-seq 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: (x_r-seq m) . s = (s * PI) / ((2 * m) + 1) by A16, Th19;
thus (<*0*> ^ ((sqr (x_r-seq m)) ")) . k = ((sqr (x_r-seq m)) ") . s by A6, A9, A12, FINSEQ_1:24
.= ((sqr (x_r-seq 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
.= ((((2 * m) + 1) ^2) / (PI ^2)) * ((Shift ((Basel-seq | (Segm (m + 1))),1)) . k) by A14, XCMPLX_1:76
.= (((((2 * m) + 1) ^2) / (PI ^2)) (#) (Shift ((Basel-seq | (Segm (m + 1))),1))) . k by VALUED_1:6 ; :: thesis: verum

end;

end;

end;

Sum (<*0*> ^ ((sqr (x_r-seq m)) ")) = 0 + (Sum ((sqr (x_r-seq m)) ")) by RVSUM_1:76;
hence Sum ((sqr (x_r-seq m)) ") = ((((2 * m) + 1) ^2) / (PI ^2)) * (Sum (Basel-seq,m)) by A2, A7, RVSUM_1:87; :: thesis: verum