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 ;
hence [((p | k) . i),((p | k) . (i + 1))] in R by ; :: thesis: verum
end;
len (p | k) > 0 by ;
hence p | k is RedSequence of R by ; :: thesis: verum
end;
end;