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 Element of 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
Element of
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:
(p /^ n) . i = p . (i + n)
by A1, A2, RFINSEQ:def 2;
A6:
(p /^ n) . j = p . (j + n)
by A1, A3, RFINSEQ:def 2;
i in Seg (len (p /^ n))
by A2, FINSEQ_1:def 3;
then
( 1
<= i &
i <= len (p /^ n) )
by FINSEQ_1:3;
then A7:
( 1
+ n <= i + n &
i <= (len p) - n )
by A1, RFINSEQ:def 2, XREAL_1:8;
1
<= 1
+ n
by NAT_1:11;
then
( 1
<= i + n &
i + n <= len p )
by A7, XREAL_1:21, XXREAL_0:2;
then
i + n in Seg (len p)
by FINSEQ_1:3;
then A8:
i + n in dom p
by FINSEQ_1:def 3;
j in Seg (len (p /^ n))
by A3, FINSEQ_1:def 3;
then
( 1
<= j &
j <= len (p /^ n) )
by FINSEQ_1:3;
then
( 1
<= j &
j <= (len p) - n )
by A1, RFINSEQ:def 2;
then A9:
( 1
+ n <= j + n &
j + n <= len p )
by XREAL_1:8, XREAL_1:21;
1
<= 1
+ n
by NAT_1:11;
then
( 1
<= j + n &
j + n <= len p )
by A9, XXREAL_0:2;
then
j + n in Seg (len p)
by FINSEQ_1:3;
then A10:
j + n in dom p
by FINSEQ_1:def 3;
i + n < j + n
by A4, XREAL_1:8;
hence
(p /^ n) . i < (p /^ n) . j
by A5, A6, A8, A10, SEQM_3:def 1;
:: thesis: verum
end;
hence
p /^ n is increasing FinSequence of REAL
by SEQM_3:def 1; :: thesis: verum