let p be increasing FinSequence of REAL ; :: thesis: for n being Element of NAT st n <= len p holds
p /^ n is increasing FinSequence of REAL
let n be Element of NAT ; :: thesis: ( n <= len p implies p /^ n is increasing FinSequence of REAL )
assume A1: n <= len p ; :: thesis: p /^ n is increasing FinSequence of REAL
for i, j being Nat st i in dom (p /^ n) & j in dom (p /^ n) & i < j holds
(p /^ n) . i < (p /^ n) . j

proof

let i, j be Nat; :: thesis: ( i in dom (p /^ n) & j in dom (p /^ n) & i < j implies (p /^ n) . i < (p /^ n) . j )
assume that
A2: i in dom (p /^ n) and
A3: j in dom (p /^ n) and
A4: i < j ; :: thesis: (p /^ n) . i < (p /^ n) . j
A5: i + n < j + n by A4, XREAL_1:6;
A6: j in Seg (len (p /^ n)) by A3, FINSEQ_1:def 3;
then 1 <= j by FINSEQ_1:1;
then A7: 1 + n <= j + n by XREAL_1:6;
j <= len (p /^ n) by A6, FINSEQ_1:1;
then j <= (len p) - n by A1, RFINSEQ:def 1;
then A8: j + n <= len p by XREAL_1:19;
1 <= 1 + n by NAT_1:11;
then 1 <= j + n by A7, XXREAL_0:2;
then j + n in Seg (len p) by A8, FINSEQ_1:1;
then A9: j + n in dom p by FINSEQ_1:def 3;
A10: i in Seg (len (p /^ n)) by A2, FINSEQ_1:def 3;
then 1 <= i by FINSEQ_1:1;
then A11: 1 + n <= i + n by XREAL_1:6;
i <= len (p /^ n) by A10, FINSEQ_1:1;
then i <= (len p) - n by A1, RFINSEQ:def 1;
then A12: i + n <= len p by XREAL_1:19;
1 <= 1 + n by NAT_1:11;
then 1 <= i + n by A11, XXREAL_0:2;
then i + n in Seg (len p) by A12, FINSEQ_1:1;
then A13: i + n in dom p by FINSEQ_1:def 3;
A14: (p /^ n) . j = p . (j + n) by A1, A3, RFINSEQ:def 1;
(p /^ n) . i = p . (i + n) by A1, A2, RFINSEQ:def 1;
hence (p /^ n) . i < (p /^ n) . j by A14, A13, A9, A5, SEQM_3:def 1; :: thesis: verum

end;

hence p /^ n is increasing FinSequence of REAL by SEQM_3:def 1; :: thesis: verum