theorem Th3: :: REWRITE2:3

for k being Nat
for R being Relation
for p being RedSequence of R st k >= 1 holds
p | k is RedSequence of R