let p be increasing FinSequence of REAL ; for n being Element of NAT st n <= len p holds
p /^ n is increasing FinSequence of REAL
let n be Element of NAT ; ( n <= len p implies p /^ n is increasing FinSequence of REAL )
assume A1:
n <= len p
; 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;
( 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
;
(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;
verum
end;
hence
p /^ n is increasing FinSequence of REAL
by SEQM_3:def 1; verum