for R being Relation
for P being RedSequence of R st len P > 1 holds
ex Q being RedSequence of R st
( (len Q) + 1 = len P & ( for k being Nat st k in dom Q holds
Q . k = P . (k + 1) ) )