let m be Nat; :: thesis: ( len (x_r-seq m) = m & ( for k being Nat st 1 <= k & k <= m holds
(x_r-seq m) . k = (k * PI) / ((2 * m) + 1) ) )
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; :: thesis: for k being Nat st 1 <= k & k <= m holds
(x_r-seq m) . k = (k * PI) / ((2 * m) + 1)
let k be Nat; :: thesis: ( 1 <= k & k <= m implies (x_r-seq m) . k = (k * PI) / ((2 * m) + 1) )
assume ( 1 <= k & k <= m ) ; :: thesis: (x_r-seq m) . k = (k * PI) / ((2 * m) + 1)
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 (x_r-seq m) . k = (k * PI) / ((2 * m) + 1) ; :: thesis: verum