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

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 )
;

end;

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

hence p | k is RedSequence of R by A3, REWRITE1:def 2; :: thesis: verum

end;

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

len (p | k) > 0
by A1, A2, FINSEQ_1:59;[((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;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

hence p | k is RedSequence of R by A3, REWRITE1:def 2; :: thesis: verum