theorem Th25: :: BASEL_1:27

for n being Nat holds x_r-seq n is one-to-one