:: by Jaros{\l}aw Kotowicz

::

:: Received November 23, 1989

:: Copyright (c) 1990-2018 Association of Mizar Users

Lm1: for n, m being Nat st n < m holds

ex k being Nat st m = (n + 1) + k

proof end;

Lm2: for seq being Real_Sequence holds

( ( ( for n being Nat holds seq . n < seq . (n + 1) ) implies for n, k being Nat holds seq . n < seq . ((n + 1) + k) ) & ( ( for n, k being Nat holds seq . n < seq . ((n + 1) + k) ) implies for n, m being Nat st n < m holds

seq . n < seq . m ) & ( ( for n, m being Nat st n < m holds

seq . n < seq . m ) implies for n being Nat holds seq . n < seq . (n + 1) ) )

proof end;

Lm3: for seq being Real_Sequence holds

( ( ( for n being Nat holds seq . (n + 1) < seq . n ) implies for n, k being Nat holds seq . ((n + 1) + k) < seq . n ) & ( ( for n, k being Nat holds seq . ((n + 1) + k) < seq . n ) implies for n, m being Nat st n < m holds

seq . m < seq . n ) & ( ( for n, m being Nat st n < m holds

seq . m < seq . n ) implies for n being Nat holds seq . (n + 1) < seq . n ) )

proof end;

Lm4: for seq being Real_Sequence holds

( ( ( for n being Nat holds seq . n <= seq . (n + 1) ) implies for n, k being Nat holds seq . n <= seq . (n + k) ) & ( ( for n, k being Nat holds seq . n <= seq . (n + k) ) implies for n, m being Nat st n <= m holds

seq . n <= seq . m ) & ( ( for n, m being Nat st n <= m holds

seq . n <= seq . m ) implies for n being Nat holds seq . n <= seq . (n + 1) ) )

proof end;

Lm5: for seq being Real_Sequence holds

( ( ( for n being Nat holds seq . (n + 1) <= seq . n ) implies for n, k being Nat holds seq . (n + k) <= seq . n ) & ( ( for n, k being Nat holds seq . (n + k) <= seq . n ) implies for n, m being Nat st n <= m holds

seq . m <= seq . n ) & ( ( for n, m being Nat st n <= m holds

seq . m <= seq . n ) implies for n being Nat holds seq . (n + 1) <= seq . n ) )

proof end;

definition

let f be NAT -defined real-valued Function;

( f is increasing iff for m, n being Nat st m in dom f & n in dom f & m < n holds

f . m < f . n ) ;

( f is decreasing iff for m, n being Nat st m in dom f & n in dom f & m < n holds

f . m > f . n ) ;

( f is non-decreasing iff for m, n being Nat st m in dom f & n in dom f & m <= n holds

f . m <= f . n ) ;

( f is non-increasing iff for m, n being Nat st m in dom f & n in dom f & m <= n holds

f . m >= f . n ) ;

end;
redefine attr f is increasing means :: SEQM_3:def 1

for m, n being Nat st m in dom f & n in dom f & m < n holds

f . m < f . n;

compatibility for m, n being Nat st m in dom f & n in dom f & m < n holds

f . m < f . n;

( f is increasing iff for m, n being Nat st m in dom f & n in dom f & m < n holds

f . m < f . n ) ;

redefine attr f is decreasing means :: SEQM_3:def 2

for m, n being Nat st m in dom f & n in dom f & m < n holds

f . m > f . n;

compatibility for m, n being Nat st m in dom f & n in dom f & m < n holds

f . m > f . n;

( f is decreasing iff for m, n being Nat st m in dom f & n in dom f & m < n holds

f . m > f . n ) ;

redefine attr f is non-decreasing means :: SEQM_3:def 3

for m, n being Nat st m in dom f & n in dom f & m <= n holds

f . m <= f . n;

compatibility for m, n being Nat st m in dom f & n in dom f & m <= n holds

f . m <= f . n;

( f is non-decreasing iff for m, n being Nat st m in dom f & n in dom f & m <= n holds

f . m <= f . n ) ;

redefine attr f is non-increasing means :: SEQM_3:def 4

for m, n being Nat st m in dom f & n in dom f & m <= n holds

f . m >= f . n;

compatibility for m, n being Nat st m in dom f & n in dom f & m <= n holds

f . m >= f . n;

( f is non-increasing iff for m, n being Nat st m in dom f & n in dom f & m <= n holds

f . m >= f . n ) ;

:: deftheorem defines increasing SEQM_3:def 1 :

for f being NAT -defined real-valued Function holds

( f is increasing iff for m, n being Nat st m in dom f & n in dom f & m < n holds

f . m < f . n );

for f being NAT -defined real-valued Function holds

( f is increasing iff for m, n being Nat st m in dom f & n in dom f & m < n holds

f . m < f . n );

:: deftheorem defines decreasing SEQM_3:def 2 :

for f being NAT -defined real-valued Function holds

( f is decreasing iff for m, n being Nat st m in dom f & n in dom f & m < n holds

f . m > f . n );

for f being NAT -defined real-valued Function holds

( f is decreasing iff for m, n being Nat st m in dom f & n in dom f & m < n holds

f . m > f . n );

:: deftheorem defines non-decreasing SEQM_3:def 3 :

for f being NAT -defined real-valued Function holds

( f is non-decreasing iff for m, n being Nat st m in dom f & n in dom f & m <= n holds

f . m <= f . n );

for f being NAT -defined real-valued Function holds

( f is non-decreasing iff for m, n being Nat st m in dom f & n in dom f & m <= n holds

f . m <= f . n );

:: deftheorem defines non-increasing SEQM_3:def 4 :

for f being NAT -defined real-valued Function holds

( f is non-increasing iff for m, n being Nat st m in dom f & n in dom f & m <= n holds

f . m >= f . n );

for f being NAT -defined real-valued Function holds

( f is non-increasing iff for m, n being Nat st m in dom f & n in dom f & m <= n holds

f . m >= f . n );

:: deftheorem defines monotone SEQM_3:def 5 :

for seq being Real_Sequence holds

( seq is monotone iff ( seq is non-decreasing or seq is non-increasing ) );

for seq being Real_Sequence holds

( seq is monotone iff ( seq is non-decreasing or seq is non-increasing ) );

theorem Th1: :: SEQM_3:1

for seq being Real_Sequence holds

( seq is increasing iff for n, m being Nat st n < m holds

seq . n < seq . m )

( seq is increasing iff for n, m being Nat st n < m holds

seq . n < seq . m )

proof end;

theorem :: SEQM_3:2

for seq being Real_Sequence holds

( seq is increasing iff for n, k being Nat holds seq . n < seq . ((n + 1) + k) ) by Lm2;

( seq is increasing iff for n, k being Nat holds seq . n < seq . ((n + 1) + k) ) by Lm2;

theorem Th3: :: SEQM_3:3

for seq being Real_Sequence holds

( seq is decreasing iff for n, k being Nat holds seq . ((n + 1) + k) < seq . n ) by Lm3;

( seq is decreasing iff for n, k being Nat holds seq . ((n + 1) + k) < seq . n ) by Lm3;

theorem Th4: :: SEQM_3:4

for seq being Real_Sequence holds

( seq is decreasing iff for n, m being Nat st n < m holds

seq . m < seq . n )

( seq is decreasing iff for n, m being Nat st n < m holds

seq . m < seq . n )

proof end;

theorem Th5: :: SEQM_3:5

for seq being Real_Sequence holds

( seq is non-decreasing iff for n, k being Nat holds seq . n <= seq . (n + k) ) by Lm4;

( seq is non-decreasing iff for n, k being Nat holds seq . n <= seq . (n + k) ) by Lm4;

theorem Th6: :: SEQM_3:6

for seq being Real_Sequence holds

( seq is non-decreasing iff for n, m being Nat st n <= m holds

seq . n <= seq . m )

( seq is non-decreasing iff for n, m being Nat st n <= m holds

seq . n <= seq . m )

proof end;

theorem Th7: :: SEQM_3:7

for seq being Real_Sequence holds

( seq is non-increasing iff for n, k being Nat holds seq . (n + k) <= seq . n ) by Lm5;

( seq is non-increasing iff for n, k being Nat holds seq . (n + k) <= seq . n ) by Lm5;

theorem Th8: :: SEQM_3:8

for seq being Real_Sequence holds

( seq is non-increasing iff for n, m being Nat st n <= m holds

seq . m <= seq . n )

( seq is non-increasing iff for n, m being Nat st n <= m holds

seq . m <= seq . n )

proof end;

theorem :: SEQM_3:9

for seq being Real_Sequence st seq is increasing holds

for n being Nat st 0 < n holds

seq . 0 < seq . n by Th1;

for n being Nat st 0 < n holds

seq . 0 < seq . n by Th1;

theorem :: SEQM_3:10

for seq being Real_Sequence st seq is decreasing holds

for n being Nat st 0 < n holds

seq . n < seq . 0 by Th4;

for n being Nat st 0 < n holds

seq . n < seq . 0 by Th4;

theorem Th11: :: SEQM_3:11

for seq being Real_Sequence st seq is non-decreasing holds

for n being Nat holds seq . 0 <= seq . n by Th6;

for n being Nat holds seq . 0 <= seq . n by Th6;

theorem Th12: :: SEQM_3:12

for seq being Real_Sequence st seq is non-increasing holds

for n being Nat holds seq . n <= seq . 0 by Th8;

for n being Nat holds seq . n <= seq . 0 by Th8;

registration

coherence

for b_{1} being PartFunc of NAT,REAL st b_{1} is constant holds

( b_{1} is non-decreasing & b_{1} is non-increasing )
;

coherence

for b_{1} being PartFunc of NAT,REAL st b_{1} is non-decreasing & b_{1} is non-increasing holds

b_{1} is constant

end;
for b

( b

coherence

for b

b

proof end;

Lm6: ( id NAT is increasing & id NAT is natural-valued )

;

registration

ex b_{1} being Real_Sequence st

( b_{1} is increasing & b_{1} is natural-valued )
end;

cluster Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued natural-valued increasing for Real_Sequence;

existence ex b

( b

proof end;

registration

ex b_{1} being sequence of NAT st b_{1} is increasing
by Lm6;

end;

cluster Relation-like NAT -defined NAT -valued Function-like non empty total V18( NAT , NAT ) complex-valued ext-real-valued real-valued natural-valued increasing for sequence of ;

existence ex b

Lm7: for f being sequence of NAT holds

( f is increasing iff for n being Nat holds f . n < f . (n + 1) )

;

theorem :: SEQM_3:13

for seq being Real_Sequence holds

( seq is sequence of NAT iff for n being Nat holds seq . n is Element of NAT )

( seq is sequence of NAT iff for n being Nat holds seq . n is Element of NAT )

proof end;

registration

let Nseq be increasing sequence of NAT;

let k be Nat;

coherence

for b_{1} being ext-real-valued Function st b_{1} = Nseq ^\ k holds

( b_{1} is increasing & b_{1} is natural-valued )

end;
let k be Nat;

coherence

for b

( b

proof end;

definition

let f be Real_Sequence;

compatibility

( f is increasing iff for n being Nat holds f . n < f . (n + 1) ) ;

compatibility

( f is decreasing iff for n being Nat holds f . n > f . (n + 1) ) ;

compatibility

( f is non-decreasing iff for n being Nat holds f . n <= f . (n + 1) ) ;

compatibility

( f is non-increasing iff for n being Nat holds f . n >= f . (n + 1) ) ;

end;
compatibility

( f is increasing iff for n being Nat holds f . n < f . (n + 1) ) ;

compatibility

( f is decreasing iff for n being Nat holds f . n > f . (n + 1) ) ;

compatibility

( f is non-decreasing iff for n being Nat holds f . n <= f . (n + 1) ) ;

compatibility

( f is non-increasing iff for n being Nat holds f . n >= f . (n + 1) ) ;

:: deftheorem defines increasing SEQM_3:def 6 :

for f being Real_Sequence holds

( f is increasing iff for n being Nat holds f . n < f . (n + 1) );

for f being Real_Sequence holds

( f is increasing iff for n being Nat holds f . n < f . (n + 1) );

:: deftheorem defines decreasing SEQM_3:def 7 :

for f being Real_Sequence holds

( f is decreasing iff for n being Nat holds f . n > f . (n + 1) );

for f being Real_Sequence holds

( f is decreasing iff for n being Nat holds f . n > f . (n + 1) );

:: deftheorem defines non-decreasing SEQM_3:def 8 :

for f being Real_Sequence holds

( f is non-decreasing iff for n being Nat holds f . n <= f . (n + 1) );

for f being Real_Sequence holds

( f is non-decreasing iff for n being Nat holds f . n <= f . (n + 1) );

:: deftheorem defines non-increasing SEQM_3:def 9 :

for f being Real_Sequence holds

( f is non-increasing iff for n being Nat holds f . n >= f . (n + 1) );

for f being Real_Sequence holds

( f is non-increasing iff for n being Nat holds f . n >= f . (n + 1) );

theorem Th15: :: SEQM_3:15

for k being Nat

for seq, seq1 being Real_Sequence holds (seq + seq1) ^\ k = (seq ^\ k) + (seq1 ^\ k)

for seq, seq1 being Real_Sequence holds (seq + seq1) ^\ k = (seq ^\ k) + (seq1 ^\ k)

proof end;

theorem :: SEQM_3:17

for k being Nat

for seq, seq1 being Real_Sequence holds (seq - seq1) ^\ k = (seq ^\ k) - (seq1 ^\ k)

for seq, seq1 being Real_Sequence holds (seq - seq1) ^\ k = (seq ^\ k) - (seq1 ^\ k)

proof end;

theorem Th19: :: SEQM_3:19

for k being Nat

for seq, seq1 being Real_Sequence holds (seq (#) seq1) ^\ k = (seq ^\ k) (#) (seq1 ^\ k)

for seq, seq1 being Real_Sequence holds (seq (#) seq1) ^\ k = (seq ^\ k) (#) (seq1 ^\ k)

proof end;

theorem :: SEQM_3:20

for k being Nat

for seq, seq1 being Real_Sequence holds (seq /" seq1) ^\ k = (seq ^\ k) /" (seq1 ^\ k)

for seq, seq1 being Real_Sequence holds (seq /" seq1) ^\ k = (seq ^\ k) /" (seq1 ^\ k)

proof end;

theorem :: SEQM_3:21

for k being Nat

for r being Real

for seq being Real_Sequence holds (r (#) seq) ^\ k = r (#) (seq ^\ k)

for r being Real

for seq being Real_Sequence holds (r (#) seq) ^\ k = r (#) (seq ^\ k)

proof end;

::

:: SUBSEQUENCES OF MONOTONE SEQUENCE

:: SUBSEQUENCE OF BOUNDED SEQUENCE

::

:: SUBSEQUENCES OF MONOTONE SEQUENCE

:: SUBSEQUENCE OF BOUNDED SEQUENCE

::

theorem :: SEQM_3:22

for seq, seq1 being Real_Sequence st seq is increasing & seq1 is subsequence of seq holds

seq1 is increasing

seq1 is increasing

proof end;

theorem :: SEQM_3:23

for seq, seq1 being Real_Sequence st seq is decreasing & seq1 is subsequence of seq holds

seq1 is decreasing

seq1 is decreasing

proof end;

theorem Th24: :: SEQM_3:24

for seq, seq1 being Real_Sequence st seq is non-decreasing & seq1 is subsequence of seq holds

seq1 is non-decreasing

seq1 is non-decreasing

proof end;

theorem Th25: :: SEQM_3:25

for seq, seq1 being Real_Sequence st seq is non-increasing & seq1 is subsequence of seq holds

seq1 is non-increasing

seq1 is non-increasing

proof end;

theorem :: SEQM_3:26

for seq, seq1 being Real_Sequence st seq is monotone & seq1 is subsequence of seq holds

seq1 is monotone by Th25, Th24;

seq1 is monotone by Th25, Th24;

theorem Th27: :: SEQM_3:27

for seq, seq1 being Real_Sequence st seq is bounded_above & seq1 is subsequence of seq holds

seq1 is bounded_above

seq1 is bounded_above

proof end;

theorem Th28: :: SEQM_3:28

for seq, seq1 being Real_Sequence st seq is bounded_below & seq1 is subsequence of seq holds

seq1 is bounded_below

seq1 is bounded_below

proof end;

theorem :: SEQM_3:29

for seq, seq1 being Real_Sequence st seq is bounded & seq1 is subsequence of seq holds

seq1 is bounded by Th27, Th28;

seq1 is bounded by Th27, Th28;

::

:: OPERATIONS ON MONOTONE SEQUENCES

::

:: OPERATIONS ON MONOTONE SEQUENCES

::

theorem :: SEQM_3:30

for r being Real

for seq being Real_Sequence holds

( ( seq is increasing & 0 < r implies r (#) seq is increasing ) & ( 0 = r implies r (#) seq is constant ) & ( seq is increasing & r < 0 implies r (#) seq is decreasing ) )

for seq being Real_Sequence holds

( ( seq is increasing & 0 < r implies r (#) seq is increasing ) & ( 0 = r implies r (#) seq is constant ) & ( seq is increasing & r < 0 implies r (#) seq is decreasing ) )

proof end;

theorem :: SEQM_3:31

for r being Real

for seq being Real_Sequence holds

( ( seq is decreasing & 0 < r implies r (#) seq is decreasing ) & ( seq is decreasing & r < 0 implies r (#) seq is increasing ) )

for seq being Real_Sequence holds

( ( seq is decreasing & 0 < r implies r (#) seq is decreasing ) & ( seq is decreasing & r < 0 implies r (#) seq is increasing ) )

proof end;

theorem :: SEQM_3:32

for r being Real

for seq being Real_Sequence holds

( ( seq is non-decreasing & 0 <= r implies r (#) seq is non-decreasing ) & ( seq is non-decreasing & r <= 0 implies r (#) seq is non-increasing ) )

for seq being Real_Sequence holds

( ( seq is non-decreasing & 0 <= r implies r (#) seq is non-decreasing ) & ( seq is non-decreasing & r <= 0 implies r (#) seq is non-increasing ) )

proof end;

theorem :: SEQM_3:33

for r being Real

for seq being Real_Sequence holds

( ( seq is non-increasing & 0 <= r implies r (#) seq is non-increasing ) & ( seq is non-increasing & r <= 0 implies r (#) seq is non-decreasing ) )

for seq being Real_Sequence holds

( ( seq is non-increasing & 0 <= r implies r (#) seq is non-increasing ) & ( seq is non-increasing & r <= 0 implies r (#) seq is non-decreasing ) )

proof end;

theorem Th34: :: SEQM_3:34

for seq, seq1 being Real_Sequence holds

( ( seq is increasing & seq1 is increasing implies seq + seq1 is increasing ) & ( seq is decreasing & seq1 is decreasing implies seq + seq1 is decreasing ) & ( seq is non-decreasing & seq1 is non-decreasing implies seq + seq1 is non-decreasing ) & ( seq is non-increasing & seq1 is non-increasing implies seq + seq1 is non-increasing ) )

( ( seq is increasing & seq1 is increasing implies seq + seq1 is increasing ) & ( seq is decreasing & seq1 is decreasing implies seq + seq1 is decreasing ) & ( seq is non-decreasing & seq1 is non-decreasing implies seq + seq1 is non-decreasing ) & ( seq is non-increasing & seq1 is non-increasing implies seq + seq1 is non-increasing ) )

proof end;

theorem :: SEQM_3:35

for seq, seq1 being Real_Sequence holds

( ( seq is increasing & seq1 is constant implies seq + seq1 is increasing ) & ( seq is decreasing & seq1 is constant implies seq + seq1 is decreasing ) & ( seq is non-decreasing & seq1 is constant implies seq + seq1 is non-decreasing ) & ( seq is non-increasing & seq1 is constant implies seq + seq1 is non-increasing ) )

( ( seq is increasing & seq1 is constant implies seq + seq1 is increasing ) & ( seq is decreasing & seq1 is constant implies seq + seq1 is decreasing ) & ( seq is non-decreasing & seq1 is constant implies seq + seq1 is non-decreasing ) & ( seq is non-increasing & seq1 is constant implies seq + seq1 is non-increasing ) )

proof end;

::

:: OPERATIONS ON BOUNDED SEQUENCES

::

:: OPERATIONS ON BOUNDED SEQUENCES

::

theorem Th36: :: SEQM_3:36

for r being Real

for seq being Real_Sequence holds

( ( seq is bounded_above & 0 < r implies r (#) seq is bounded_above ) & ( 0 = r implies r (#) seq is bounded ) & ( seq is bounded_above & r < 0 implies r (#) seq is bounded_below ) )

for seq being Real_Sequence holds

( ( seq is bounded_above & 0 < r implies r (#) seq is bounded_above ) & ( 0 = r implies r (#) seq is bounded ) & ( seq is bounded_above & r < 0 implies r (#) seq is bounded_below ) )

proof end;

theorem :: SEQM_3:37

for seq being Real_Sequence holds

( ( seq is bounded implies for r being Real holds r (#) seq is bounded ) & ( seq is bounded implies - seq is bounded ) & ( seq is bounded implies abs seq is bounded ) & ( abs seq is bounded implies seq is bounded ) )

( ( seq is bounded implies for r being Real holds r (#) seq is bounded ) & ( seq is bounded implies - seq is bounded ) & ( seq is bounded implies abs seq is bounded ) & ( abs seq is bounded implies seq is bounded ) )

proof end;

::

:: OPERATIONS ON BOUNDED & MONOTONE SEQUENCES

::

:: OPERATIONS ON BOUNDED & MONOTONE SEQUENCES

::

theorem :: SEQM_3:38

for seq, seq1 being Real_Sequence st seq is bounded_above & seq1 is non-increasing holds

seq + seq1 is bounded_above

seq + seq1 is bounded_above

proof end;

theorem :: SEQM_3:39

for seq, seq1 being Real_Sequence st seq is bounded_below & seq1 is non-decreasing holds

seq + seq1 is bounded_below

seq + seq1 is bounded_below

proof end;

:::theorem

::: incl NAT is increasing natural-valued by Lm10;

::: incl NAT is increasing natural-valued by Lm10;

::$CT

theorem Th40: :: SEQM_3:41

for r, s being Real holds

( |.(r - s).| = 1 iff ( ( r > s & r = s + 1 ) or ( r < s & s = r + 1 ) ) )

( |.(r - s).| = 1 iff ( ( r > s & r = s + 1 ) or ( r < s & s = r + 1 ) ) )

proof end;

theorem :: SEQM_3:42

for n, m, i, j being Nat holds

( |.(i - j).| + |.(n - m).| = 1 iff ( ( |.(i - j).| = 1 & n = m ) or ( |.(n - m).| = 1 & i = j ) ) )

( |.(i - j).| + |.(n - m).| = 1 iff ( ( |.(i - j).| = 1 & n = m ) or ( |.(n - m).| = 1 & i = j ) ) )

proof end;

theorem :: SEQM_3:44

for f being FinSequence

for n, m, k being Nat st len f = m + 1 & n in dom f & k in Seg m & not (Del (f,n)) . k = f . k holds

(Del (f,n)) . k = f . (k + 1)

for n, m, k being Nat st len f = m + 1 & n in dom f & k in Seg m & not (Del (f,n)) . k = f . k holds

(Del (f,n)) . k = f . (k + 1)

proof end;

definition

let f be FinSequence;

( f is constant iff for n, m being Nat st n in dom f & m in dom f holds

f . n = f . m ) ;

end;
redefine attr f is constant means :: SEQM_3:def 10

for n, m being Nat st n in dom f & m in dom f holds

f . n = f . m;

compatibility for n, m being Nat st n in dom f & m in dom f holds

f . n = f . m;

( f is constant iff for n, m being Nat st n in dom f & m in dom f holds

f . n = f . m ) ;

:: deftheorem defines constant SEQM_3:def 10 :

for f being FinSequence holds

( f is constant iff for n, m being Nat st n in dom f & m in dom f holds

f . n = f . m );

for f being FinSequence holds

( f is constant iff for n, m being Nat st n in dom f & m in dom f holds

f . n = f . m );

registration

ex b_{1} being FinSequence of REAL st

( not b_{1} is empty & b_{1} is increasing )
end;

cluster Relation-like NAT -defined REAL -valued Function-like non empty complex-valued ext-real-valued real-valued increasing V61() FinSequence-like FinSubsequence-like for of ;

existence ex b

( not b

proof end;

registration

ex b_{1} being FinSequence of REAL st b_{1} is constant
end;

cluster Relation-like NAT -defined REAL -valued Function-like constant complex-valued ext-real-valued real-valued V61() FinSequence-like FinSubsequence-like for of ;

existence ex b

proof end;

theorem Th44: :: SEQM_3:45

for v being FinSequence of REAL

for n, m, i being Nat st v <> {} & rng v c= Seg n & v . (len v) = n & ( for k being Nat st 1 <= k & k <= (len v) - 1 holds

for r, s being Real st r = v . k & s = v . (k + 1) & not |.(r - s).| = 1 holds

r = s ) & i in Seg n & i + 1 in Seg n & m in dom v & v . m = i & ( for k being Nat st k in dom v & v . k = i holds

k <= m ) holds

( m + 1 in dom v & v . (m + 1) = i + 1 )

for n, m, i being Nat st v <> {} & rng v c= Seg n & v . (len v) = n & ( for k being Nat st 1 <= k & k <= (len v) - 1 holds

for r, s being Real st r = v . k & s = v . (k + 1) & not |.(r - s).| = 1 holds

r = s ) & i in Seg n & i + 1 in Seg n & m in dom v & v . m = i & ( for k being Nat st k in dom v & v . k = i holds

k <= m ) holds

( m + 1 in dom v & v . (m + 1) = i + 1 )

proof end;

theorem :: SEQM_3:46

for v being FinSequence of REAL

for n being Nat st v <> {} & rng v c= Seg n & v . 1 = 1 & v . (len v) = n & ( for k being Nat st 1 <= k & k <= (len v) - 1 holds

for r, s being Real st r = v . k & s = v . (k + 1) & not |.(r - s).| = 1 holds

r = s ) holds

( ( for i being Nat st i in Seg n holds

ex k being Nat st

( k in dom v & v . k = i ) ) & ( for m, k, i being Nat

for r being Real st m in dom v & v . m = i & ( for j being Nat st j in dom v & v . j = i holds

j <= m ) & m < k & k in dom v & r = v . k holds

i < r ) )

for n being Nat st v <> {} & rng v c= Seg n & v . 1 = 1 & v . (len v) = n & ( for k being Nat st 1 <= k & k <= (len v) - 1 holds

for r, s being Real st r = v . k & s = v . (k + 1) & not |.(r - s).| = 1 holds

r = s ) holds

( ( for i being Nat st i in Seg n holds

ex k being Nat st

( k in dom v & v . k = i ) ) & ( for m, k, i being Nat

for r being Real st m in dom v & v . m = i & ( for j being Nat st j in dom v & v . j = i holds

j <= m ) & m < k & k in dom v & r = v . k holds

i < r ) )

proof end;

:: PROPORTIES OF MONOTONE AND CONSTANT SEQUENCES

::