theorem Th8: :: REWRITE1:8

for R being Relation
for p, q being RedSequence of R st p . (len p) = q . 1 holds
p $^ q is RedSequence of R