theorem Th5: :: REWRITE3:5

for R being Relation
for P being RedSequence of R st len P > 1 holds
ex Q being RedSequence of R st
( <*(P . 1)*> ^ Q = P & (len Q) + 1 = len P )