let n be Nat; :: thesis: x_r-seq n is one-to-one
set f = x_r-seq n;
let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in dom (x_r-seq n) or not x2 in dom (x_r-seq n) or not (x_r-seq n) . x1 = (x_r-seq n) . x2 or x1 = x2 )
assume A1: ( x1 in dom (x_r-seq n) & x2 in dom (x_r-seq n) & (x_r-seq n) . x1 = (x_r-seq n) . x2 ) ; :: thesis: x1 = x2
reconsider x1 = x1, x2 = x2 as Nat by A1;
len (x_r-seq n) = n by Th19;
then ( 1 <= x1 & x1 <= n & 1 <= x2 & x2 <= n ) by A1, FINSEQ_3:25;
then A2: ( (x_r-seq n) . x1 = (x1 * PI) / ((2 * n) + 1) & (x_r-seq n) . x2 = (x2 * PI) / ((2 * n) + 1) ) by Th19;
x1 * PI = x2 * PI by A1, A2, XCMPLX_1:53;
hence x1 = x2 by XCMPLX_1:5; :: thesis: verum