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 A1, FINSEQ_3:27;
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 A1, FINSEQ_3:27;
hence len (p | k) = k by FINSEQ_1:80; :: 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 A2, FINSEQ_3:121; :: thesis: verum