let k be Nat; :: thesis: for R being Relation
for p being RedSequence of R st k >= 1 holds
p | k is RedSequence of R
let R be Relation; :: thesis: for p being RedSequence of R st k >= 1 holds
p | k is RedSequence of R
let p be RedSequence of R; :: thesis: ( k >= 1 implies p | k is RedSequence of R )
assume A1: k >= 1 ; :: thesis: p | k is RedSequence of R

per cases ( k >= len p or k < len p ) ;

suppose k >= len p ; :: thesis: p | k is RedSequence of R

hence p | k is RedSequence of R by FINSEQ_1:58; :: thesis: verum

end;

suppose A2: k < len p ; :: thesis: p | k is RedSequence of R

A3: now :: thesis: for i being Nat st i in dom (p | k) & i + 1 in dom (p | k) holds
[((p | k) . i),((p | k) . (i + 1))] in R

A4: dom (p | k) c= dom p by RELAT_1:60;
let i be Nat; :: thesis: ( i in dom (p | k) & i + 1 in dom (p | k) implies [((p | k) . i),((p | k) . (i + 1))] in R )
assume A5: ( i in dom (p | k) & i + 1 in dom (p | k) ) ; :: thesis: [((p | k) . i),((p | k) . (i + 1))] in R
( (p | k) . i = p . i & (p | k) . (i + 1) = p . (i + 1) ) by A5, FUNCT_1:47;
hence [((p | k) . i),((p | k) . (i + 1))] in R by A5, A4, REWRITE1:def 2; :: thesis: verum

end;

len (p | k) > 0 by A1, A2, FINSEQ_1:59;
hence p | k is RedSequence of R by A3, REWRITE1:def 2; :: thesis: verum

end;

end;