let k be Nat; :: thesis: 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 )

let R be Relation; :: thesis: 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 )

let p be RedSequence of R; :: thesis: ( k in dom p implies ex q being RedSequence of R st
( len q = k & q . 1 = p . 1 & q . (len q) = p . k ) )

assume A1: k in dom p ; :: thesis: ex q being RedSequence of R st
( len q = k & q . 1 = p . 1 & q . (len q) = p . k )

set q = p | k;
take p | k ; :: thesis: ( p | k is RedSequence of R & len (p | k) = k & (p | k) . 1 = p . 1 & (p | k) . (len (p | k)) = p . k )
A2: 1 <= k by ;
hence p | k is RedSequence of R by Th3; :: thesis: ( len (p | k) = k & (p | k) . 1 = p . 1 & (p | k) . (len (p | k)) = p . k )
k <= len p by ;
hence len (p | k) = k by FINSEQ_1:59; :: thesis: ( (p | k) . 1 = p . 1 & (p | k) . (len (p | k)) = p . k )
hence ( (p | k) . 1 = p . 1 & (p | k) . (len (p | k)) = p . k ) by ; :: thesis: verum