let k, m be Nat; :: thesis: ( 1 <= k & k <= m implies ((2 * m) + 1) * ((x_r-seq m) . k) = k * PI )
assume ( 1 <= k & k <= m ) ; :: thesis: ((2 * m) + 1) * ((x_r-seq m) . k) = k * PI
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 ((2 * m) + 1) * ((x_r-seq m) . k) = k * PI by A1; :: thesis: verum