theorem Th4: :: REWRITE2:4

for k being Nat
for R being Relation
for p being RedSequence of R st k in dom p holds
ex q being RedSequence of R st
( len q = k & q . 1 = p . 1 & q . (len q) = p . k )