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:25;

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:25;

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 A2, FINSEQ_3:112; :: thesis: verum

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:25;

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:25;

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 A2, FINSEQ_3:112; :: thesis: verum