:: SEQM_3 semantic presentation

begin

          Lm1:  for n, m being Element of NAT st n < m holds
ex k being Element of NAT st m = (n + 1) + k
proof
let n, m be Element of NAT ; ::_thesis: ( n < m implies ex k being Element of NAT st m = (n + 1) + k )
assume A1: n < m ; ::_thesis: ex k being Element of NAT st m = (n + 1) + k
then consider k1 being Nat such that
A2: m = n + k1 by NAT_1:10;
 k1 <> 0 by A1, A2;
then consider n1 being Nat such that
A3: k1 = n1 + 1 by NAT_1:6;
reconsider n1 = n1 as Element of NAT by ORDINAL1:def_12;
take  n1 ; ::_thesis: m = (n + 1) + n1
thus  m = (n + 1) + n1 by A2, A3; ::_thesis: verum
end;

Lm2:  for seq being Real_Sequence holds
( ( ( for n being Element of NAT holds seq . n < seq . (n + 1) ) implies for n, k being Element of NAT holds seq . n < seq . ((n + 1) + k) ) & ( ( for n, k being Element of NAT holds seq . n < seq . ((n + 1) + k) ) implies for n, m being Element of NAT st n < m holds
seq . n < seq . m ) & ( ( for n, m being Element of NAT st n < m holds
seq . n < seq . m ) implies for n being Element of NAT holds seq . n < seq . (n + 1) ) )
proof
let seq be Real_Sequence; ::_thesis: ( ( ( for n being Element of NAT holds seq . n < seq . (n + 1) ) implies for n, k being Element of NAT holds seq . n < seq . ((n + 1) + k) ) & ( ( for n, k being Element of NAT holds seq . n < seq . ((n + 1) + k) ) implies for n, m being Element of NAT st n < m holds
seq . n < seq . m ) & ( ( for n, m being Element of NAT st n < m holds
seq . n < seq . m ) implies for n being Element of NAT holds seq . n < seq . (n + 1) ) )
thus  ( ( for n being Element of NAT holds seq . n < seq . (n + 1) ) implies for n, k being Element of NAT holds seq . n < seq . ((n + 1) + k) ) ::_thesis: ( ( ( for n, k being Element of NAT holds seq . n < seq . ((n + 1) + k) ) implies for n, m being Element of NAT st n < m holds
seq . n < seq . m ) & ( ( for n, m being Element of NAT st n < m holds
seq . n < seq . m ) implies for n being Element of NAT holds seq . n < seq . (n + 1) ) )
proof
assume A1: for n being Element of NAT holds seq . n < seq . (n + 1) ; ::_thesis: for n, k being Element of NAT holds seq . n < seq . ((n + 1) + k)
let n be Element of NAT ; ::_thesis: for k being Element of NAT holds seq . n < seq . ((n + 1) + k)
defpred S1[ Element of NAT ] means seq . n < seq . ((n + 1) + $1);
A2: now__::_thesis:_for_k_being_Element_of_NAT_st_S1[k]_holds_
S1[k_+_1]
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A3: S1[k] ; ::_thesis: S1[k + 1]
 seq . ((n + 1) + k) < seq . (((n + 1) + k) + 1) by A1;
hence  S1[k + 1] by A3, XXREAL_0:2; ::_thesis: verum
end;
A4: S1[ 0 ] by A1;
thus  for k being Element of NAT holds S1[k] from NAT_1:sch_1(A4, A2); ::_thesis: verum
end;
thus  ( ( for n, k being Element of NAT holds seq . n < seq . ((n + 1) + k) ) implies for n, m being Element of NAT st n < m holds
seq . n < seq . m ) ::_thesis: ( ( for n, m being Element of NAT st n < m holds
seq . n < seq . m ) implies for n being Element of NAT holds seq . n < seq . (n + 1) )
proof
assume A5: for n, k being Element of NAT holds seq . n < seq . ((n + 1) + k) ; ::_thesis: for n, m being Element of NAT st n < m holds
seq . n < seq . m
let n, m be Element of NAT ; ::_thesis: ( n < m implies seq . n < seq . m )
assume  n < m ; ::_thesis: seq . n < seq . m
then  ex k being Element of NAT st m = (n + 1) + k by Lm1;
hence  seq . n < seq . m by A5; ::_thesis: verum
end;
assume A6: for n, m being Element of NAT st n < m holds
seq . n < seq . m ; ::_thesis: for n being Element of NAT holds seq . n < seq . (n + 1)
let n be Element of NAT ; ::_thesis: seq . n < seq . (n + 1)
 n < n + 1 by NAT_1:13;
hence  seq . n < seq . (n + 1) by A6; ::_thesis: verum
end;

Lm3:  for seq being Real_Sequence holds
( ( ( for n being Element of NAT holds seq . (n + 1) < seq . n ) implies for n, k being Element of NAT holds seq . ((n + 1) + k) < seq . n ) & ( ( for n, k being Element of NAT holds seq . ((n + 1) + k) < seq . n ) implies for n, m being Element of NAT st n < m holds
seq . m < seq . n ) & ( ( for n, m being Element of NAT st n < m holds
seq . m < seq . n ) implies for n being Element of NAT holds seq . (n + 1) < seq . n ) )
proof
let seq be Real_Sequence; ::_thesis: ( ( ( for n being Element of NAT holds seq . (n + 1) < seq . n ) implies for n, k being Element of NAT holds seq . ((n + 1) + k) < seq . n ) & ( ( for n, k being Element of NAT holds seq . ((n + 1) + k) < seq . n ) implies for n, m being Element of NAT st n < m holds
seq . m < seq . n ) & ( ( for n, m being Element of NAT st n < m holds
seq . m < seq . n ) implies for n being Element of NAT holds seq . (n + 1) < seq . n ) )
thus  ( ( for n being Element of NAT holds seq . (n + 1) < seq . n ) implies for n, k being Element of NAT holds seq . ((n + 1) + k) < seq . n ) ::_thesis: ( ( ( for n, k being Element of NAT holds seq . ((n + 1) + k) < seq . n ) implies for n, m being Element of NAT st n < m holds
seq . m < seq . n ) & ( ( for n, m being Element of NAT st n < m holds
seq . m < seq . n ) implies for n being Element of NAT holds seq . (n + 1) < seq . n ) )
proof
assume A1: for n being Element of NAT holds seq . (n + 1) < seq . n ; ::_thesis: for n, k being Element of NAT holds seq . ((n + 1) + k) < seq . n
let n be Element of NAT ; ::_thesis: for k being Element of NAT holds seq . ((n + 1) + k) < seq . n
defpred S1[ Element of NAT ] means seq . ((n + 1) + $1) < seq . n;
A2: now__::_thesis:_for_k_being_Element_of_NAT_st_S1[k]_holds_
S1[k_+_1]
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A3: S1[k] ; ::_thesis: S1[k + 1]
 seq . (((n + 1) + k) + 1) < seq . ((n + 1) + k) by A1;
hence  S1[k + 1] by A3, XXREAL_0:2; ::_thesis: verum
end;
A4: S1[ 0 ] by A1;
thus  for k being Element of NAT holds S1[k] from NAT_1:sch_1(A4, A2); ::_thesis: verum
end;
thus  ( ( for n, k being Element of NAT holds seq . ((n + 1) + k) < seq . n ) implies for n, m being Element of NAT st n < m holds
seq . m < seq . n ) ::_thesis: ( ( for n, m being Element of NAT st n < m holds
seq . m < seq . n ) implies for n being Element of NAT holds seq . (n + 1) < seq . n )
proof
assume A5: for n, k being Element of NAT holds seq . ((n + 1) + k) < seq . n ; ::_thesis: for n, m being Element of NAT st n < m holds
seq . m < seq . n
let n, m be Element of NAT ; ::_thesis: ( n < m implies seq . m < seq . n )
assume  n < m ; ::_thesis: seq . m < seq . n
then  ex k being Element of NAT st m = (n + 1) + k by Lm1;
hence  seq . m < seq . n by A5; ::_thesis: verum
end;
assume A6: for n, m being Element of NAT st n < m holds
seq . m < seq . n ; ::_thesis: for n being Element of NAT holds seq . (n + 1) < seq . n
let n be Element of NAT ; ::_thesis: seq . (n + 1) < seq . n
 n < n + 1 by NAT_1:13;
hence  seq . (n + 1) < seq . n by A6; ::_thesis: verum
end;

Lm4:  for seq being Real_Sequence holds
( ( ( for n being Element of NAT holds seq . n <= seq . (n + 1) ) implies for n, k being Element of NAT holds seq . n <= seq . (n + k) ) & ( ( for n, k being Element of NAT holds seq . n <= seq . (n + k) ) implies for n, m being Element of NAT st n <= m holds
seq . n <= seq . m ) & ( ( for n, m being Element of NAT st n <= m holds
seq . n <= seq . m ) implies for n being Element of NAT holds seq . n <= seq . (n + 1) ) )
proof
let seq be Real_Sequence; ::_thesis: ( ( ( for n being Element of NAT holds seq . n <= seq . (n + 1) ) implies for n, k being Element of NAT holds seq . n <= seq . (n + k) ) & ( ( for n, k being Element of NAT holds seq . n <= seq . (n + k) ) implies for n, m being Element of NAT st n <= m holds
seq . n <= seq . m ) & ( ( for n, m being Element of NAT st n <= m holds
seq . n <= seq . m ) implies for n being Element of NAT holds seq . n <= seq . (n + 1) ) )
thus  ( ( for n being Element of NAT holds seq . n <= seq . (n + 1) ) implies for n, k being Element of NAT holds seq . n <= seq . (n + k) ) ::_thesis: ( ( ( for n, k being Element of NAT holds seq . n <= seq . (n + k) ) implies for n, m being Element of NAT st n <= m holds
seq . n <= seq . m ) & ( ( for n, m being Element of NAT st n <= m holds
seq . n <= seq . m ) implies for n being Element of NAT holds seq . n <= seq . (n + 1) ) )
proof
assume A1: for n being Element of NAT holds seq . n <= seq . (n + 1) ; ::_thesis: for n, k being Element of NAT holds seq . n <= seq . (n + k)
let n be Element of NAT ; ::_thesis: for k being Element of NAT holds seq . n <= seq . (n + k)
defpred S1[ Element of NAT ] means seq . n <= seq . (n + $1);
A2: now__::_thesis:_for_k_being_Element_of_NAT_st_S1[k]_holds_
S1[k_+_1]
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A3: S1[k] ; ::_thesis: S1[k + 1]
 seq . (n + k) <= seq . ((n + k) + 1) by A1;
hence  S1[k + 1] by A3, XXREAL_0:2; ::_thesis: verum
end;
A4: S1[ 0 ] ;
thus  for k being Element of NAT holds S1[k] from NAT_1:sch_1(A4, A2); ::_thesis: verum
end;
thus  ( ( for n, k being Element of NAT holds seq . n <= seq . (n + k) ) implies for n, m being Element of NAT st n <= m holds
seq . n <= seq . m ) ::_thesis: ( ( for n, m being Element of NAT st n <= m holds
seq . n <= seq . m ) implies for n being Element of NAT holds seq . n <= seq . (n + 1) )
proof
assume A5: for n, k being Element of NAT holds seq . n <= seq . (n + k) ; ::_thesis: for n, m being Element of NAT st n <= m holds
seq . n <= seq . m
let n, m be Element of NAT ; ::_thesis: ( n <= m implies seq . n <= seq . m )
assume  n <= m ; ::_thesis: seq . n <= seq . m
then consider k1 being Nat such that
A6: m = n + k1 by NAT_1:10;
 k1 in NAT by ORDINAL1:def_12;
hence  seq . n <= seq . m by A5, A6; ::_thesis: verum
end;
assume A7: for n, m being Element of NAT st n <= m holds
seq . n <= seq . m ; ::_thesis: for n being Element of NAT holds seq . n <= seq . (n + 1)
let n be Element of NAT ; ::_thesis: seq . n <= seq . (n + 1)
 n <= n + 1 by NAT_1:13;
hence  seq . n <= seq . (n + 1) by A7; ::_thesis: verum
end;

Lm5:  for seq being Real_Sequence holds
( ( ( for n being Element of NAT holds seq . (n + 1) <= seq . n ) implies for n, k being Element of NAT holds seq . (n + k) <= seq . n ) & ( ( for n, k being Element of NAT holds seq . (n + k) <= seq . n ) implies for n, m being Element of NAT st n <= m holds
seq . m <= seq . n ) & ( ( for n, m being Element of NAT st n <= m holds
seq . m <= seq . n ) implies for n being Element of NAT holds seq . (n + 1) <= seq . n ) )
proof
let seq be Real_Sequence; ::_thesis: ( ( ( for n being Element of NAT holds seq . (n + 1) <= seq . n ) implies for n, k being Element of NAT holds seq . (n + k) <= seq . n ) & ( ( for n, k being Element of NAT holds seq . (n + k) <= seq . n ) implies for n, m being Element of NAT st n <= m holds
seq . m <= seq . n ) & ( ( for n, m being Element of NAT st n <= m holds
seq . m <= seq . n ) implies for n being Element of NAT holds seq . (n + 1) <= seq . n ) )
thus  ( ( for n being Element of NAT holds seq . (n + 1) <= seq . n ) implies for n, k being Element of NAT holds seq . (n + k) <= seq . n ) ::_thesis: ( ( ( for n, k being Element of NAT holds seq . (n + k) <= seq . n ) implies for n, m being Element of NAT st n <= m holds
seq . m <= seq . n ) & ( ( for n, m being Element of NAT st n <= m holds
seq . m <= seq . n ) implies for n being Element of NAT holds seq . (n + 1) <= seq . n ) )
proof
assume A1: for n being Element of NAT holds seq . (n + 1) <= seq . n ; ::_thesis: for n, k being Element of NAT holds seq . (n + k) <= seq . n
let n be Element of NAT ; ::_thesis: for k being Element of NAT holds seq . (n + k) <= seq . n
defpred S1[ Element of NAT ] means seq . (n + $1) <= seq . n;
A2: now__::_thesis:_for_k_being_Element_of_NAT_st_S1[k]_holds_
S1[k_+_1]
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A3: S1[k] ; ::_thesis: S1[k + 1]
 seq . ((n + k) + 1) <= seq . (n + k) by A1;
hence  S1[k + 1] by A3, XXREAL_0:2; ::_thesis: verum
end;
A4: S1[ 0 ] ;
thus  for k being Element of NAT holds S1[k] from NAT_1:sch_1(A4, A2); ::_thesis: verum
end;
thus  ( ( for n, k being Element of NAT holds seq . (n + k) <= seq . n ) implies for n, m being Element of NAT st n <= m holds
seq . m <= seq . n ) ::_thesis: ( ( for n, m being Element of NAT st n <= m holds
seq . m <= seq . n ) implies for n being Element of NAT holds seq . (n + 1) <= seq . n )
proof
assume A5: for n, k being Element of NAT holds seq . (n + k) <= seq . n ; ::_thesis: for n, m being Element of NAT st n <= m holds
seq . m <= seq . n
let n, m be Element of NAT ; ::_thesis: ( n <= m implies seq . m <= seq . n )
assume  n <= m ; ::_thesis: seq . m <= seq . n
then consider k1 being Nat such that
A6: m = n + k1 by NAT_1:10;
 k1 in NAT by ORDINAL1:def_12;
hence  seq . m <= seq . n by A5, A6; ::_thesis: verum
end;
assume A7: for n, m being Element of NAT st n <= m holds
seq . m <= seq . n ; ::_thesis: for n being Element of NAT holds seq . (n + 1) <= seq . n
let n be Element of NAT ; ::_thesis: seq . (n + 1) <= seq . n
 n <= n + 1 by NAT_1:13;
hence  seq . (n + 1) <= seq . n by A7; ::_thesis: verum
end;


definition
let f be NAT -defined REAL -valued Function;
redefine attr f is increasing  means :Def1: :: SEQM_3:def 1
 for m, n being Element of NAT st m in dom f & n in dom f & m < n holds
f . m < f . n;
compatibility
 ( f is increasing iff for m, n being Element of NAT st m in dom f & n in dom f & m < n holds
f . m < f . n )
proof
thus  ( f is increasing implies for m, n being Element of NAT st m in dom f & n in dom f & m < n holds
f . m < f . n ) by VALUED_0:def_13; ::_thesis: ( ( for m, n being Element of NAT st m in dom f & n in dom f & m < n holds
f . m < f . n ) implies f is increasing )
assume A1: for m, n being Element of NAT st m in dom f & n in dom f & m < n holds
f . m < f . n ; ::_thesis: f is increasing
let e1 be ext-real number ; :: according to VALUED_0:def_13 ::_thesis: for b1 being set holds
( not e1 in dom f or not b1 in dom f or b1 <= e1 or not f . b1 <= f . e1 )
let e2 be ext-real number ; ::_thesis: ( not e1 in dom f or not e2 in dom f or e2 <= e1 or not f . e2 <= f . e1 )
 dom f c= NAT by RELAT_1:def_18;
hence  ( not e1 in dom f or not e2 in dom f or e2 <= e1 or not f . e2 <= f . e1 ) by A1; ::_thesis: verum
end;
redefine attr f is decreasing  means :Def2: :: SEQM_3:def 2
 for m, n being Element of NAT st m in dom f & n in dom f & m < n holds
f . m > f . n;
compatibility
 ( f is decreasing iff for m, n being Element of NAT st m in dom f & n in dom f & m < n holds
f . m > f . n )
proof
thus  ( f is decreasing implies for m, n being Element of NAT st m in dom f & n in dom f & m < n holds
f . m > f . n ) by VALUED_0:def_14; ::_thesis: ( ( for m, n being Element of NAT st m in dom f & n in dom f & m < n holds
f . m > f . n ) implies f is decreasing )
assume A2: for m, n being Element of NAT st m in dom f & n in dom f & m < n holds
f . m > f . n ; ::_thesis: f is decreasing
let e1 be ext-real number ; :: according to VALUED_0:def_14 ::_thesis: for b1 being set holds
( not e1 in dom f or not b1 in dom f or b1 <= e1 or not f . e1 <= f . b1 )
let e2 be ext-real number ; ::_thesis: ( not e1 in dom f or not e2 in dom f or e2 <= e1 or not f . e1 <= f . e2 )
 dom f c= NAT by RELAT_1:def_18;
hence  ( not e1 in dom f or not e2 in dom f or e2 <= e1 or not f . e1 <= f . e2 ) by A2; ::_thesis: verum
end;
redefine attr f is non-decreasing  means :Def3: :: SEQM_3:def 3
 for m, n being Element of NAT st m in dom f & n in dom f & m <= n holds
f . m <= f . n;
compatibility
 ( f is non-decreasing iff for m, n being Element of NAT st m in dom f & n in dom f & m <= n holds
f . m <= f . n )
proof
thus  ( f is non-decreasing implies for m, n being Element of NAT st m in dom f & n in dom f & m <= n holds
f . m <= f . n ) by VALUED_0:def_15; ::_thesis: ( ( for m, n being Element of NAT st m in dom f & n in dom f & m <= n holds
f . m <= f . n ) implies f is non-decreasing )
assume A3: for m, n being Element of NAT st m in dom f & n in dom f & m <= n holds
f . m <= f . n ; ::_thesis: f is non-decreasing
let e1 be ext-real number ; :: according to VALUED_0:def_15 ::_thesis: for b1 being set holds
( not e1 in dom f or not b1 in dom f or not e1 <= b1 or f . e1 <= f . b1 )
let e2 be ext-real number ; ::_thesis: ( not e1 in dom f or not e2 in dom f or not e1 <= e2 or f . e1 <= f . e2 )
 dom f c= NAT by RELAT_1:def_18;
hence  ( not e1 in dom f or not e2 in dom f or not e1 <= e2 or f . e1 <= f . e2 ) by A3; ::_thesis: verum
end;
redefine attr f is non-increasing  means :Def4: :: SEQM_3:def 4
 for m, n being Element of NAT st m in dom f & n in dom f & m <= n holds
f . m >= f . n;
compatibility
 ( f is non-increasing iff for m, n being Element of NAT st m in dom f & n in dom f & m <= n holds
f . m >= f . n )
proof
thus  ( f is non-increasing implies for m, n being Element of NAT st m in dom f & n in dom f & m <= n holds
f . m >= f . n ) by VALUED_0:def_16; ::_thesis: ( ( for m, n being Element of NAT st m in dom f & n in dom f & m <= n holds
f . m >= f . n ) implies f is non-increasing )
assume A4: for m, n being Element of NAT st m in dom f & n in dom f & m <= n holds
f . m >= f . n ; ::_thesis: f is non-increasing
let e1 be ext-real number ; :: according to VALUED_0:def_16 ::_thesis: for b1 being set holds
( not e1 in dom f or not b1 in dom f or not e1 <= b1 or f . b1 <= f . e1 )
let e2 be ext-real number ; ::_thesis: ( not e1 in dom f or not e2 in dom f or not e1 <= e2 or f . e2 <= f . e1 )
 dom f c= NAT by RELAT_1:def_18;
hence  ( not e1 in dom f or not e2 in dom f or not e1 <= e2 or f . e2 <= f . e1 ) by A4; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines increasing SEQM_3:def_1_:_
 for f being NAT -defined REAL -valued Function holds
( f is increasing iff for m, n being Element of NAT st m in dom f & n in dom f & m < n holds
f . m < f . n );

:: deftheorem Def2 defines decreasing SEQM_3:def_2_:_
 for f being NAT -defined REAL -valued Function holds
( f is decreasing iff for m, n being Element of NAT st m in dom f & n in dom f & m < n holds
f . m > f . n );

:: deftheorem Def3 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 Element of NAT st m in dom f & n in dom f & m <= n holds
f . m <= f . n );

:: deftheorem Def4 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 Element of NAT st m in dom f & n in dom f & m <= n holds
f . m >= f . n );

Lm6:  for f being Real_Sequence holds
( f is increasing iff for n being Element of NAT holds f . n < f . (n + 1) )
proof
let f be Real_Sequence; ::_thesis: ( f is increasing iff for n being Element of NAT holds f . n < f . (n + 1) )
thus  ( f is increasing implies for n being Element of NAT holds f . n < f . (n + 1) ) ::_thesis: ( ( for n being Element of NAT holds f . n < f . (n + 1) ) implies f is increasing )
proof
assume A1: f is increasing ; ::_thesis: for n being Element of NAT holds f . n < f . (n + 1)
let n be Element of NAT ; ::_thesis: f . n < f . (n + 1)
 ( dom f = NAT & n < n + 1 ) by FUNCT_2:def_1, NAT_1:13;
hence  f . n < f . (n + 1) by A1, Def1; ::_thesis: verum
end;
assume A2: for n being Element of NAT holds f . n < f . (n + 1) ; ::_thesis: f is increasing
let m be Element of NAT ; :: according to SEQM_3:def_1 ::_thesis: for n being Element of NAT st m in dom f & n in dom f & m < n holds
f . m < f . n
let n be Element of NAT ; ::_thesis: ( m in dom f & n in dom f & m < n implies f . m < f . n )
assume that
 m in dom f and
 n in dom f and
A3: m < n ; ::_thesis: f . m < f . n
 ex k being Element of NAT st n = (m + 1) + k by A3, Lm1;
hence  f . m < f . n by A2, Lm2; ::_thesis: verum
end;

Lm7:  for f being Real_Sequence holds
( f is decreasing iff for n being Element of NAT holds f . n > f . (n + 1) )
proof
let f be Real_Sequence; ::_thesis: ( f is decreasing iff for n being Element of NAT holds f . n > f . (n + 1) )
thus  ( f is decreasing implies for n being Element of NAT holds f . n > f . (n + 1) ) ::_thesis: ( ( for n being Element of NAT holds f . n > f . (n + 1) ) implies f is decreasing )
proof
assume A1: f is decreasing ; ::_thesis: for n being Element of NAT holds f . n > f . (n + 1)
let n be Element of NAT ; ::_thesis: f . n > f . (n + 1)
 ( dom f = NAT & n < n + 1 ) by FUNCT_2:def_1, NAT_1:13;
hence  f . n > f . (n + 1) by A1, Def2; ::_thesis: verum
end;
assume A2: for n being Element of NAT holds f . n > f . (n + 1) ; ::_thesis: f is decreasing
let m be Element of NAT ; :: according to SEQM_3:def_2 ::_thesis: for n being Element of NAT st m in dom f & n in dom f & m < n holds
f . m > f . n
let n be Element of NAT ; ::_thesis: ( m in dom f & n in dom f & m < n implies f . m > f . n )
assume that
 m in dom f and
 n in dom f and
A3: m < n ; ::_thesis: f . m > f . n
 ex k being Element of NAT st n = (m + 1) + k by A3, Lm1;
hence  f . m > f . n by A2, Lm3; ::_thesis: verum
end;

Lm8:  for f being Real_Sequence holds
( f is non-decreasing iff for n being Element of NAT holds f . n <= f . (n + 1) )
proof
let f be Real_Sequence; ::_thesis: ( f is non-decreasing iff for n being Element of NAT holds f . n <= f . (n + 1) )
thus  ( f is non-decreasing implies for n being Element of NAT holds f . n <= f . (n + 1) ) ::_thesis: ( ( for n being Element of NAT holds f . n <= f . (n + 1) ) implies f is non-decreasing )
proof
assume A1: f is non-decreasing ; ::_thesis: for n being Element of NAT holds f . n <= f . (n + 1)
let n be Element of NAT ; ::_thesis: f . n <= f . (n + 1)
 ( dom f = NAT & n < n + 1 ) by FUNCT_2:def_1, NAT_1:13;
hence  f . n <= f . (n + 1) by A1, Def3; ::_thesis: verum
end;
assume A2: for n being Element of NAT holds f . n <= f . (n + 1) ; ::_thesis: f is non-decreasing
let m be Element of NAT ; :: according to SEQM_3:def_3 ::_thesis: for n being Element of NAT st m in dom f & n in dom f & m <= n holds
f . m <= f . n
let n be Element of NAT ; ::_thesis: ( m in dom f & n in dom f & m <= n implies f . m <= f . n )
assume that
 m in dom f and
 n in dom f and
A3: m <= n ; ::_thesis: f . m <= f . n
consider k being Nat such that
A4: n = m + k by A3, NAT_1:10;
 k in NAT by ORDINAL1:def_12;
hence  f . m <= f . n by A2, A4, Lm4; ::_thesis: verum
end;

Lm9:  for f being Real_Sequence holds
( f is non-increasing iff for n being Element of NAT holds f . n >= f . (n + 1) )
proof
let f be Real_Sequence; ::_thesis: ( f is non-increasing iff for n being Element of NAT holds f . n >= f . (n + 1) )
thus  ( f is non-increasing implies for n being Element of NAT holds f . n >= f . (n + 1) ) ::_thesis: ( ( for n being Element of NAT holds f . n >= f . (n + 1) ) implies f is non-increasing )
proof
assume A1: f is non-increasing ; ::_thesis: for n being Element of NAT holds f . n >= f . (n + 1)
let n be Element of NAT ; ::_thesis: f . n >= f . (n + 1)
 ( dom f = NAT & n < n + 1 ) by FUNCT_2:def_1, NAT_1:13;
hence  f . n >= f . (n + 1) by A1, Def4; ::_thesis: verum
end;
assume A2: for n being Element of NAT holds f . n >= f . (n + 1) ; ::_thesis: f is non-increasing
let m be Element of NAT ; :: according to SEQM_3:def_4 ::_thesis: for n being Element of NAT st m in dom f & n in dom f & m <= n holds
f . m >= f . n
let n be Element of NAT ; ::_thesis: ( m in dom f & n in dom f & m <= n implies f . m >= f . n )
assume that
 m in dom f and
 n in dom f and
A3: m <= n ; ::_thesis: f . m >= f . n
consider k being Nat such that
A4: n = m + k by A3, NAT_1:10;
 k in NAT by ORDINAL1:def_12;
hence  f . m >= f . n by A2, A4, Lm5; ::_thesis: verum
end;

definition
let seq be Real_Sequence;
attrseq is monotone  means :Def5: :: SEQM_3:def 5
( seq is non-decreasing or seq is non-increasing );
end;

:: deftheorem Def5 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 ) );

theorem Th1: :: SEQM_3:1
for seq being Real_Sequence holds
( seq is increasing iff for n, m being Element of NAT st n < m holds
seq . n < seq . m )
proof
let seq be Real_Sequence; ::_thesis: ( seq is increasing iff for n, m being Element of NAT st n < m holds
seq . n < seq . m )
thus  ( seq is increasing implies for n, m being Element of NAT st n < m holds
seq . n < seq . m ) ::_thesis: ( ( for n, m being Element of NAT st n < m holds
seq . n < seq . m ) implies seq is increasing )
proof
assume  seq is increasing ; ::_thesis: for n, m being Element of NAT st n < m holds
seq . n < seq . m
then  for n being Element of NAT holds seq . n < seq . (n + 1) by Lm6;
then  for n, k being Element of NAT holds seq . n < seq . ((n + 1) + k) by Lm2;
hence  for n, m being Element of NAT st n < m holds
seq . n < seq . m by Lm2; ::_thesis: verum
end;
assume A1: for n, m being Element of NAT st n < m holds
seq . n < seq . m ; ::_thesis: seq is increasing
let n be Element of NAT ; :: according to SEQM_3:def_1 ::_thesis: for n being Element of NAT st n in dom seq & n in dom seq & n < n holds
seq . n < seq . n
let m be Element of NAT ; ::_thesis: ( n in dom seq & m in dom seq & n < m implies seq . n < seq . m )
assume that
 n in dom seq and
 m in dom seq and
A2: n < m ; ::_thesis: seq . n < seq . m
thus  seq . n < seq . m by A1, A2; ::_thesis: verum
end;

theorem :: SEQM_3:2
for seq being Real_Sequence holds
( seq is increasing iff for n, k being Element of NAT holds seq . n < seq . ((n + 1) + k) )
proof
let seq be Real_Sequence; ::_thesis: ( seq is increasing iff for n, k being Element of NAT holds seq . n < seq . ((n + 1) + k) )
thus  ( seq is increasing implies for n, k being Element of NAT holds seq . n < seq . ((n + 1) + k) ) ::_thesis: ( ( for n, k being Element of NAT holds seq . n < seq . ((n + 1) + k) ) implies seq is increasing )
proof
assume  seq is increasing ; ::_thesis: for n, k being Element of NAT holds seq . n < seq . ((n + 1) + k)
then  for n being Element of NAT holds seq . n < seq . (n + 1) by Lm6;
hence  for n, k being Element of NAT holds seq . n < seq . ((n + 1) + k) by Lm2; ::_thesis: verum
end;
assume  for n, k being Element of NAT holds seq . n < seq . ((n + 1) + k) ; ::_thesis: seq is increasing
then  for n, m being Element of NAT st n < m holds
seq . n < seq . m by Lm2;
hence  seq is increasing by Th1; ::_thesis: verum
end;

theorem Th3: :: SEQM_3:3
for seq being Real_Sequence holds
( seq is decreasing iff for n, k being Element of NAT holds seq . ((n + 1) + k) < seq . n )
proof
let seq be Real_Sequence; ::_thesis: ( seq is decreasing iff for n, k being Element of NAT holds seq . ((n + 1) + k) < seq . n )
thus  ( seq is decreasing implies for n, k being Element of NAT holds seq . ((n + 1) + k) < seq . n ) ::_thesis: ( ( for n, k being Element of NAT holds seq . ((n + 1) + k) < seq . n ) implies seq is decreasing )
proof
assume  seq is decreasing ; ::_thesis: for n, k being Element of NAT holds seq . ((n + 1) + k) < seq . n
then  for n being Element of NAT holds seq . (n + 1) < seq . n by Lm7;
hence  for n, k being Element of NAT holds seq . ((n + 1) + k) < seq . n by Lm3; ::_thesis: verum
end;
assume A1: for n, k being Element of NAT holds seq . ((n + 1) + k) < seq . n ; ::_thesis: seq is decreasing
let n be Element of NAT ; :: according to SEQM_3:def_2 ::_thesis: for n being Element of NAT st n in dom seq & n in dom seq & n < n holds
seq . n > seq . n
let m be Element of NAT ; ::_thesis: ( n in dom seq & m in dom seq & n < m implies seq . n > seq . m )
assume that
 n in dom seq and
 m in dom seq and
A2: n < m ; ::_thesis: seq . n > seq . m
thus  seq . n > seq . m by A1, A2, Lm3; ::_thesis: verum
end;

theorem Th4: :: SEQM_3:4
for seq being Real_Sequence holds
( seq is decreasing iff for n, m being Element of NAT st n < m holds
seq . m < seq . n )
proof
let seq be Real_Sequence; ::_thesis: ( seq is decreasing iff for n, m being Element of NAT st n < m holds
seq . m < seq . n )
thus  ( seq is decreasing implies for n, m being Element of NAT st n < m holds
seq . m < seq . n ) ::_thesis: ( ( for n, m being Element of NAT st n < m holds
seq . m < seq . n ) implies seq is decreasing )
proof
assume  seq is decreasing ; ::_thesis: for n, m being Element of NAT st n < m holds
seq . m < seq . n
then  for n, k being Element of NAT holds seq . ((n + 1) + k) < seq . n by Th3;
hence  for n, m being Element of NAT st n < m holds
seq . m < seq . n by Lm3; ::_thesis: verum
end;
assume A1: for n, m being Element of NAT st n < m holds
seq . m < seq . n ; ::_thesis: seq is decreasing
let n be Element of NAT ; :: according to SEQM_3:def_2 ::_thesis: for n being Element of NAT st n in dom seq & n in dom seq & n < n holds
seq . n > seq . n
let m be Element of NAT ; ::_thesis: ( n in dom seq & m in dom seq & n < m implies seq . n > seq . m )
assume that
 n in dom seq and
 m in dom seq and
A2: n < m ; ::_thesis: seq . n > seq . m
thus  seq . n > seq . m by A1, A2; ::_thesis: verum
end;

theorem Th5: :: SEQM_3:5
for seq being Real_Sequence holds
( seq is non-decreasing iff for n, k being Element of NAT holds seq . n <= seq . (n + k) )
proof
let seq be Real_Sequence; ::_thesis: ( seq is non-decreasing iff for n, k being Element of NAT holds seq . n <= seq . (n + k) )
thus  ( seq is non-decreasing implies for n, k being Element of NAT holds seq . n <= seq . (n + k) ) ::_thesis: ( ( for n, k being Element of NAT holds seq . n <= seq . (n + k) ) implies seq is non-decreasing )
proof
assume  seq is non-decreasing ; ::_thesis: for n, k being Element of NAT holds seq . n <= seq . (n + k)
then  for n being Element of NAT holds seq . n <= seq . (n + 1) by Lm8;
hence  for n, k being Element of NAT holds seq . n <= seq . (n + k) by Lm4; ::_thesis: verum
end;
assume  for n, k being Element of NAT holds seq . n <= seq . (n + k) ; ::_thesis: seq is non-decreasing
then  for n being Element of NAT holds seq . n <= seq . (n + 1) ;
hence  seq is non-decreasing by Lm8; ::_thesis: verum
end;

theorem Th6: :: SEQM_3:6
for seq being Real_Sequence holds
( seq is non-decreasing iff for n, m being Element of NAT st n <= m holds
seq . n <= seq . m )
proof
let seq be Real_Sequence; ::_thesis: ( seq is non-decreasing iff for n, m being Element of NAT st n <= m holds
seq . n <= seq . m )
thus  ( seq is non-decreasing implies for n, m being Element of NAT st n <= m holds
seq . n <= seq . m ) ::_thesis: ( ( for n, m being Element of NAT st n <= m holds
seq . n <= seq . m ) implies seq is non-decreasing )
proof
assume  seq is non-decreasing ; ::_thesis: for n, m being Element of NAT st n <= m holds
seq . n <= seq . m
then  for n, k being Element of NAT holds seq . n <= seq . (n + k) by Th5;
hence  for n, m being Element of NAT st n <= m holds
seq . n <= seq . m by Lm4; ::_thesis: verum
end;
assume A1: for n, m being Element of NAT st n <= m holds
seq . n <= seq . m ; ::_thesis: seq is non-decreasing
let n be Element of NAT ; :: according to SEQM_3:def_3 ::_thesis: for n being Element of NAT st n in dom seq & n in dom seq & n <= n holds
seq . n <= seq . n
let m be Element of NAT ; ::_thesis: ( n in dom seq & m in dom seq & n <= m implies seq . n <= seq . m )
assume that
 n in dom seq and
 m in dom seq and
A2: n <= m ; ::_thesis: seq . n <= seq . m
thus  seq . n <= seq . m by A1, A2; ::_thesis: verum
end;

theorem Th7: :: SEQM_3:7
for seq being Real_Sequence holds
( seq is non-increasing iff for n, k being Element of NAT holds seq . (n + k) <= seq . n )
proof
let seq be Real_Sequence; ::_thesis: ( seq is non-increasing iff for n, k being Element of NAT holds seq . (n + k) <= seq . n )
thus  ( seq is non-increasing implies for n, k being Element of NAT holds seq . (n + k) <= seq . n ) ::_thesis: ( ( for n, k being Element of NAT holds seq . (n + k) <= seq . n ) implies seq is non-increasing )
proof
assume  seq is non-increasing ; ::_thesis: for n, k being Element of NAT holds seq . (n + k) <= seq . n
then  for n being Element of NAT holds seq . (n + 1) <= seq . n by Lm9;
hence  for n, k being Element of NAT holds seq . (n + k) <= seq . n by Lm5; ::_thesis: verum
end;
assume  for n, k being Element of NAT holds seq . (n + k) <= seq . n ; ::_thesis: seq is non-increasing
then  for n being Element of NAT holds seq . (n + 1) <= seq . n ;
hence  seq is non-increasing by Lm9; ::_thesis: verum
end;

theorem Th8: :: SEQM_3:8
for seq being Real_Sequence holds
( seq is non-increasing iff for n, m being Element of NAT st n <= m holds
seq . m <= seq . n )
proof
let seq be Real_Sequence; ::_thesis: ( seq is non-increasing iff for n, m being Element of NAT st n <= m holds
seq . m <= seq . n )
thus  ( seq is non-increasing implies for n, m being Element of NAT st n <= m holds
seq . m <= seq . n ) ::_thesis: ( ( for n, m being Element of NAT st n <= m holds
seq . m <= seq . n ) implies seq is non-increasing )
proof
assume  seq is non-increasing ; ::_thesis: for n, m being Element of NAT st n <= m holds
seq . m <= seq . n
then  for n, k being Element of NAT holds seq . (n + k) <= seq . n by Th7;
hence  for n, m being Element of NAT st n <= m holds
seq . m <= seq . n by Lm5; ::_thesis: verum
end;
assume A1: for n, m being Element of NAT st n <= m holds
seq . m <= seq . n ; ::_thesis: seq is non-increasing
let n be Element of NAT ; :: according to SEQM_3:def_4 ::_thesis: for n being Element of NAT st n in dom seq & n in dom seq & n <= n holds
seq . n >= seq . n
let m be Element of NAT ; ::_thesis: ( n in dom seq & m in dom seq & n <= m implies seq . n >= seq . m )
assume that
 n in dom seq and
 m in dom seq and
A2: n <= m ; ::_thesis: seq . n >= seq . m
thus  seq . n >= seq . m by A1, A2; ::_thesis: verum
end;

theorem :: SEQM_3:9
for seq being Real_Sequence st seq is increasing holds
for n being Element of 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 Element of 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 Element of 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 Element of NAT holds seq . n <= seq . 0 by Th8;

registration
cluster Function-like constant  ->  non-decreasing non-increasing for Element of K19(K20(NAT,REAL));
coherence
 for b1 being PartFunc of NAT,REAL st b1 is constant holds
( b1 is non-decreasing & b1 is non-increasing )
proof
let f be PartFunc of NAT,REAL; ::_thesis: ( f is constant implies ( f is non-decreasing & f is non-increasing ) )
assume A1: f is constant ; ::_thesis: ( f is non-decreasing & f is non-increasing )
thus  f is non-decreasing ::_thesis: f is non-increasing
proof
let m be Element of NAT ; :: according to SEQM_3:def_3 ::_thesis: for n being Element of NAT st m in dom f & n in dom f & m <= n holds
f . m <= f . n
let n be Element of NAT ; ::_thesis: ( m in dom f & n in dom f & m <= n implies f . m <= f . n )
assume that
A2: ( m in dom f & n in dom f ) and
 m <= n ; ::_thesis: f . m <= f . n
thus  f . m <= f . n by A1, A2, FUNCT_1:def_10; ::_thesis: verum
end;
let m be Element of NAT ; :: according to SEQM_3:def_4 ::_thesis: for n being Element of NAT st m in dom f & n in dom f & m <= n holds
f . m >= f . n
let n be Element of NAT ; ::_thesis: ( m in dom f & n in dom f & m <= n implies f . m >= f . n )
assume that
A3: ( m in dom f & n in dom f ) and
 m <= n ; ::_thesis: f . m >= f . n
thus  f . m >= f . n by A1, A3, FUNCT_1:def_10; ::_thesis: verum
end;
cluster Function-like non-decreasing non-increasing  ->  constant for Element of K19(K20(NAT,REAL));
coherence
 for b1 being PartFunc of NAT,REAL st b1 is non-decreasing & b1 is non-increasing holds
b1 is constant
proof
let f be PartFunc of NAT,REAL; ::_thesis: ( f is non-decreasing & f is non-increasing implies f is constant )
assume A4: ( f is non-decreasing & f is non-increasing ) ; ::_thesis: f is constant
let x be set ; :: according to FUNCT_1:def_10 ::_thesis: for b1 being set holds
( not x in dom f or not b1 in dom f or f . x = f . b1 )
let y be set ; ::_thesis: ( not x in dom f or not y in dom f or f . x = f . y )
assume A5: ( x in dom f & y in dom f ) ; ::_thesis: f . x = f . y
 dom f c= NAT by RELAT_1:def_18;
then reconsider m = x, n = y as Element of NAT by A5;
 ( m <= n or n <= m ) ;
then  ( f . m <= f . n & f . n <= f . m ) by A4, A5, Def3, Def4;
hence  f . x = f . y by XXREAL_0:1; ::_thesis: verum
end;
end;

Lm10:  ( incl NAT is increasing & incl NAT is natural-valued )
proof
set seq = incl NAT;
now__::_thesis:_for_n_being_Element_of_NAT_holds_(incl_NAT)_._n_<_(incl_NAT)_._(n_+_1)
let n be Element of NAT ; ::_thesis: (incl NAT) . n < (incl NAT) . (n + 1)
 ( (incl NAT) . n = n & (incl NAT) . (n + 1) = n + 1 ) by FUNCT_1:18;
hence  (incl NAT) . n < (incl NAT) . (n + 1) by NAT_1:13; ::_thesis: verum
end;
hence  ( incl NAT is increasing & incl NAT is natural-valued ) by Lm6; ::_thesis: verum
end;

Lm11:  ( id NAT is increasing & id NAT is natural-valued )
;

registration
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 Element of K19(K20(NAT,REAL));
existence
 ex b1 being Real_Sequence st
( b1 is increasing & b1 is natural-valued ) by Lm10;
end;

registration
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 Element of K19(K20(NAT,NAT));
existence
 ex b1 being sequence of NAT st b1 is increasing by Lm11;
end;

Lm12:  for f being sequence of NAT holds
( f is increasing iff for n being Element of NAT holds f . n < f . (n + 1) )
proof
let f be sequence of NAT; ::_thesis: ( f is increasing iff for n being Element of NAT holds f . n < f . (n + 1) )
reconsider f = f as Real_Sequence by FUNCT_2:7;
 ( f is increasing iff for n being Element of NAT holds f . n < f . (n + 1) ) by Lm6;
hence  ( f is increasing iff for n being Element of NAT holds f . n < f . (n + 1) ) ; ::_thesis: verum
end;

theorem :: SEQM_3:13
for seq being Real_Sequence holds
( seq is sequence of NAT iff for n being Element of NAT holds seq . n is Element of NAT )
proof
let seq be Real_Sequence; ::_thesis: ( seq is sequence of NAT iff for n being Element of NAT holds seq . n is Element of NAT )
thus  ( seq is sequence of NAT implies for n being Element of NAT holds seq . n is Element of NAT ) ::_thesis: ( ( for n being Element of NAT holds seq . n is Element of NAT ) implies seq is sequence of NAT )
proof
assume  seq is sequence of NAT ; ::_thesis: for n being Element of NAT holds seq . n is Element of NAT
then A1: rng seq c= NAT by VALUED_0:def_6;
let n be Element of NAT ; ::_thesis: seq . n is Element of NAT
 n in NAT ;
then  n in dom seq by FUNCT_2:def_1;
then  seq . n in rng seq by FUNCT_1:def_3;
hence  seq . n is Element of NAT by A1; ::_thesis: verum
end;
assume A2: for n being Element of NAT holds seq . n is Element of NAT ; ::_thesis: seq is sequence of NAT
 rng seq c= NAT
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng seq or x in NAT )
assume  x in rng seq ; ::_thesis: x in NAT
then consider y being set  such that
A3: y in dom seq and
A4: x = seq . y by FUNCT_1:def_3;
reconsider y = y as Element of NAT by A3, FUNCT_2:def_1;
 x = seq . y by A4;
then  x is Element of NAT by A2;
hence  x in NAT ; ::_thesis: verum
end;
hence  seq is sequence of NAT by FUNCT_2:6; ::_thesis: verum
end;

registration
let Nseq be increasing sequence of NAT;
let k be Element of NAT ;
clusterNseq ^\ k ->  ext-real-valued natural-valued increasing for ext-real-valued Function;
coherence
 for b1 being ext-real-valued Function st b1 = Nseq ^\ k holds
( b1 is increasing & b1 is natural-valued )
proof
now__::_thesis:_for_n_being_Element_of_NAT_holds_(Nseq_^\_k)_._n_<_(Nseq_^\_k)_._(n_+_1)
let n be Element of NAT ; ::_thesis: (Nseq ^\ k) . n < (Nseq ^\ k) . (n + 1)
 Nseq . (n + k) < Nseq . ((n + k) + 1) by Lm12;
then  (Nseq ^\ k) . n < Nseq . ((n + 1) + k) by NAT_1:def_3;
hence  (Nseq ^\ k) . n < (Nseq ^\ k) . (n + 1) by NAT_1:def_3; ::_thesis: verum
end;
hence  for b1 being ext-real-valued Function st b1 = Nseq ^\ k holds
( b1 is increasing & b1 is natural-valued ) by Lm12; ::_thesis: verum
end;
end;

definition
let f be Real_Sequence;
redefine attr f is increasing  means :: SEQM_3:def 6
 for n being Element of NAT holds f . n < f . (n + 1);
compatibility
 ( f is increasing iff for n being Element of NAT holds f . n < f . (n + 1) ) by Lm6;
redefine attr f is decreasing  means :: SEQM_3:def 7
 for n being Element of NAT holds f . n > f . (n + 1);
compatibility
 ( f is decreasing iff for n being Element of NAT holds f . n > f . (n + 1) ) by Lm7;
redefine attr f is non-decreasing  means :: SEQM_3:def 8
 for n being Element of NAT holds f . n <= f . (n + 1);
compatibility
 ( f is non-decreasing iff for n being Element of NAT holds f . n <= f . (n + 1) ) by Lm8;
redefine attr f is non-increasing  means :: SEQM_3:def 9
 for n being Element of NAT holds f . n >= f . (n + 1);
compatibility
 ( f is non-increasing iff for n being Element of NAT holds f . n >= f . (n + 1) ) by Lm9;
end;

:: deftheorem  defines increasing SEQM_3:def_6_:_
 for f being Real_Sequence holds
( f is increasing iff for n being Element of 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 Element of 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 Element of 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 Element of NAT holds f . n >= f . (n + 1) );

theorem :: SEQM_3:14
for Nseq being increasing sequence of NAT
for n being Element of NAT holds n <= Nseq . n
proof
let Nseq be increasing sequence of NAT; ::_thesis: for n being Element of NAT holds n <= Nseq . n
defpred S1[ Element of NAT ] means $1 <= Nseq . $1;
A1: now__::_thesis:_for_k_being_Element_of_NAT_st_S1[k]_holds_
S1[k_+_1]
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A2: S1[k] ; ::_thesis: S1[k + 1]
 Nseq . k < Nseq . (k + 1) by Lm12;
then  k < Nseq . (k + 1) by A2, XXREAL_0:2;
hence  S1[k + 1] by NAT_1:13; ::_thesis: verum
end;
A3: S1[ 0 ] ;
thus  for k being Element of NAT holds S1[k] from NAT_1:sch_1(A3, A1); ::_thesis: verum
end;

registration
let s be Real_Sequence;
let k be Nat;
clusters ^\ k ->  real-valued ;
coherence
 s ^\ k is real-valued ;
end;

theorem Th15: :: SEQM_3:15
for k being Element of NAT
for seq, seq1 being Real_Sequence holds (seq + seq1) ^\ k = (seq ^\ k) + (seq1 ^\ k)
proof
let k be Element of NAT ; ::_thesis: for seq, seq1 being Real_Sequence holds (seq + seq1) ^\ k = (seq ^\ k) + (seq1 ^\ k)
let seq, seq1 be Real_Sequence; ::_thesis: (seq + seq1) ^\ k = (seq ^\ k) + (seq1 ^\ k)
now__::_thesis:_for_n_being_Element_of_NAT_holds_((seq_+_seq1)_^\_k)_._n_=_((seq_^\_k)_+_(seq1_^\_k))_._n
let n be Element of NAT ; ::_thesis: ((seq + seq1) ^\ k) . n = ((seq ^\ k) + (seq1 ^\ k)) . n
thus ((seq + seq1) ^\ k) . n = (seq + seq1) . (n + k) by NAT_1:def_3
.= (seq . (n + k)) + (seq1 . (n + k)) by SEQ_1:7
.= ((seq ^\ k) . n) + (seq1 . (n + k)) by NAT_1:def_3
.= ((seq ^\ k) . n) + ((seq1 ^\ k) . n) by NAT_1:def_3
.= ((seq ^\ k) + (seq1 ^\ k)) . n by SEQ_1:7 ; ::_thesis: verum
end;
hence  (seq + seq1) ^\ k = (seq ^\ k) + (seq1 ^\ k) by FUNCT_2:63; ::_thesis: verum
end;

theorem Th16: :: SEQM_3:16
for k being Element of NAT
for seq being Real_Sequence holds (- seq) ^\ k = - (seq ^\ k)
proof
let k be Element of NAT ; ::_thesis: for seq being Real_Sequence holds (- seq) ^\ k = - (seq ^\ k)
let seq be Real_Sequence; ::_thesis: (- seq) ^\ k = - (seq ^\ k)
now__::_thesis:_for_n_being_Element_of_NAT_holds_((-_seq)_^\_k)_._n_=_(-_(seq_^\_k))_._n
let n be Element of NAT ; ::_thesis: ((- seq) ^\ k) . n = (- (seq ^\ k)) . n
thus ((- seq) ^\ k) . n = (- seq) . (n + k) by NAT_1:def_3
.= - (seq . (n + k)) by SEQ_1:10
.= - ((seq ^\ k) . n) by NAT_1:def_3
.= (- (seq ^\ k)) . n by SEQ_1:10 ; ::_thesis: verum
end;
hence  (- seq) ^\ k = - (seq ^\ k) by FUNCT_2:63; ::_thesis: verum
end;

theorem :: SEQM_3:17
for k being Element of NAT
for seq, seq1 being Real_Sequence holds (seq - seq1) ^\ k = (seq ^\ k) - (seq1 ^\ k)
proof
let k be Element of NAT ; ::_thesis: for seq, seq1 being Real_Sequence holds (seq - seq1) ^\ k = (seq ^\ k) - (seq1 ^\ k)
let seq, seq1 be Real_Sequence; ::_thesis: (seq - seq1) ^\ k = (seq ^\ k) - (seq1 ^\ k)
thus (seq - seq1) ^\ k = (seq ^\ k) + ((- seq1) ^\ k) by Th15
.= (seq ^\ k) - (seq1 ^\ k) by Th16 ; ::_thesis: verum
end;

theorem Th18: :: SEQM_3:18
for k being Element of NAT
for seq being Real_Sequence holds (seq ") ^\ k = (seq ^\ k) "
proof
let k be Element of NAT ; ::_thesis: for seq being Real_Sequence holds (seq ") ^\ k = (seq ^\ k) "
let seq be Real_Sequence; ::_thesis: (seq ") ^\ k = (seq ^\ k) "
now__::_thesis:_for_n_being_Element_of_NAT_holds_((seq_")_^\_k)_._n_=_((seq_^\_k)_")_._n
let n be Element of NAT ; ::_thesis: ((seq ") ^\ k) . n = ((seq ^\ k) ") . n
thus ((seq ") ^\ k) . n = (seq ") . (n + k) by NAT_1:def_3
.= (seq . (n + k)) " by VALUED_1:10
.= ((seq ^\ k) . n) " by NAT_1:def_3
.= ((seq ^\ k) ") . n by VALUED_1:10 ; ::_thesis: verum
end;
hence  (seq ") ^\ k = (seq ^\ k) " by FUNCT_2:63; ::_thesis: verum
end;

theorem Th19: :: SEQM_3:19
for k being Element of NAT
for seq, seq1 being Real_Sequence holds (seq (#) seq1) ^\ k = (seq ^\ k) (#) (seq1 ^\ k)
proof
let k be Element of NAT ; ::_thesis: for seq, seq1 being Real_Sequence holds (seq (#) seq1) ^\ k = (seq ^\ k) (#) (seq1 ^\ k)
let seq, seq1 be Real_Sequence; ::_thesis: (seq (#) seq1) ^\ k = (seq ^\ k) (#) (seq1 ^\ k)
now__::_thesis:_for_n_being_Element_of_NAT_holds_((seq_(#)_seq1)_^\_k)_._n_=_((seq_^\_k)_(#)_(seq1_^\_k))_._n
let n be Element of NAT ; ::_thesis: ((seq (#) seq1) ^\ k) . n = ((seq ^\ k) (#) (seq1 ^\ k)) . n
thus ((seq (#) seq1) ^\ k) . n = (seq (#) seq1) . (n + k) by NAT_1:def_3
.= (seq . (n + k)) * (seq1 . (n + k)) by SEQ_1:8
.= ((seq ^\ k) . n) * (seq1 . (n + k)) by NAT_1:def_3
.= ((seq ^\ k) . n) * ((seq1 ^\ k) . n) by NAT_1:def_3
.= ((seq ^\ k) (#) (seq1 ^\ k)) . n by SEQ_1:8 ; ::_thesis: verum
end;
hence  (seq (#) seq1) ^\ k = (seq ^\ k) (#) (seq1 ^\ k) by FUNCT_2:63; ::_thesis: verum
end;

theorem :: SEQM_3:20
for k being Element of NAT
for seq, seq1 being Real_Sequence holds (seq /" seq1) ^\ k = (seq ^\ k) /" (seq1 ^\ k)
proof
let k be Element of NAT ; ::_thesis: for seq, seq1 being Real_Sequence holds (seq /" seq1) ^\ k = (seq ^\ k) /" (seq1 ^\ k)
let seq, seq1 be Real_Sequence; ::_thesis: (seq /" seq1) ^\ k = (seq ^\ k) /" (seq1 ^\ k)
thus (seq /" seq1) ^\ k = (seq ^\ k) (#) ((seq1 ") ^\ k) by Th19
.= (seq ^\ k) /" (seq1 ^\ k) by Th18 ; ::_thesis: verum
end;

theorem :: SEQM_3:21
for k being Element of NAT
for r being real number
for seq being Real_Sequence holds (r (#) seq) ^\ k = r (#) (seq ^\ k)
proof
let k be Element of NAT ; ::_thesis: for r being real number
for seq being Real_Sequence holds (r (#) seq) ^\ k = r (#) (seq ^\ k)
let r be real number ; ::_thesis: for seq being Real_Sequence holds (r (#) seq) ^\ k = r (#) (seq ^\ k)
let seq be Real_Sequence; ::_thesis: (r (#) seq) ^\ k = r (#) (seq ^\ k)
now__::_thesis:_for_n_being_Element_of_NAT_holds_((r_(#)_seq)_^\_k)_._n_=_(r_(#)_(seq_^\_k))_._n
let n be Element of NAT ; ::_thesis: ((r (#) seq) ^\ k) . n = (r (#) (seq ^\ k)) . n
thus ((r (#) seq) ^\ k) . n = (r (#) seq) . (n + k) by NAT_1:def_3
.= r * (seq . (n + k)) by SEQ_1:9
.= r * ((seq ^\ k) . n) by NAT_1:def_3
.= (r (#) (seq ^\ k)) . n by SEQ_1:9 ; ::_thesis: verum
end;
hence  (r (#) seq) ^\ k = r (#) (seq ^\ k) by FUNCT_2:63; ::_thesis: verum
end;

theorem :: SEQM_3:22
for seq, seq1 being Real_Sequence st seq is increasing & seq1 is subsequence of seq holds
seq1 is increasing
proof
let seq, seq1 be Real_Sequence; ::_thesis: ( seq is increasing & seq1 is subsequence of seq implies seq1 is increasing )
assume that
A1: seq is increasing and
A2: seq1 is subsequence of seq ; ::_thesis: seq1 is increasing
let n be Element of NAT ; :: according to SEQM_3:def_6 ::_thesis: seq1 . n < seq1 . (n + 1)
consider Nseq being increasing sequence of NAT such that
A3: seq1 = seq * Nseq by A2, VALUED_0:def_17;
 Nseq . n < Nseq . (n + 1) by Lm12;
then  seq . (Nseq . n) < seq . (Nseq . (n + 1)) by A1, Th1;
then  (seq * Nseq) . n < seq . (Nseq . (n + 1)) by FUNCT_2:15;
hence  seq1 . n < seq1 . (n + 1) by A3, FUNCT_2:15; ::_thesis: verum
end;

theorem :: SEQM_3:23
for seq, seq1 being Real_Sequence st seq is decreasing & seq1 is subsequence of seq holds
seq1 is decreasing
proof
let seq, seq1 be Real_Sequence; ::_thesis: ( seq is decreasing & seq1 is subsequence of seq implies seq1 is decreasing )
assume that
A1: seq is decreasing and
A2: seq1 is subsequence of seq ; ::_thesis: seq1 is decreasing
let n be Element of NAT ; :: according to SEQM_3:def_7 ::_thesis: seq1 . n > seq1 . (n + 1)
consider Nseq being increasing sequence of NAT such that
A3: seq1 = seq * Nseq by A2, VALUED_0:def_17;
 Nseq . n < Nseq . (n + 1) by Lm12;
then  seq . (Nseq . (n + 1)) < seq . (Nseq . n) by A1, Th4;
then  (seq * Nseq) . (n + 1) < seq . (Nseq . n) by FUNCT_2:15;
hence  seq1 . n > seq1 . (n + 1) by A3, FUNCT_2:15; ::_thesis: verum
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
proof
let seq, seq1 be Real_Sequence; ::_thesis: ( seq is non-decreasing & seq1 is subsequence of seq implies seq1 is non-decreasing )
assume that
A1: seq is non-decreasing and
A2: seq1 is subsequence of seq ; ::_thesis: seq1 is non-decreasing
let n be Element of NAT ; :: according to SEQM_3:def_8 ::_thesis: seq1 . n <= seq1 . (n + 1)
consider Nseq being increasing sequence of NAT such that
A3: seq1 = seq * Nseq by A2, VALUED_0:def_17;
 Nseq . n <= Nseq . (n + 1) by Lm12;
then  seq . (Nseq . n) <= seq . (Nseq . (n + 1)) by A1, Th6;
then  (seq * Nseq) . n <= seq . (Nseq . (n + 1)) by FUNCT_2:15;
hence  seq1 . n <= seq1 . (n + 1) by A3, FUNCT_2:15; ::_thesis: verum
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
proof
let seq, seq1 be Real_Sequence; ::_thesis: ( seq is non-increasing & seq1 is subsequence of seq implies seq1 is non-increasing )
assume that
A1: seq is non-increasing and
A2: seq1 is subsequence of seq ; ::_thesis: seq1 is non-increasing
let n be Element of NAT ; :: according to SEQM_3:def_9 ::_thesis: seq1 . n >= seq1 . (n + 1)
consider Nseq being increasing sequence of NAT such that
A3: seq1 = seq * Nseq by A2, VALUED_0:def_17;
 Nseq . n <= Nseq . (n + 1) by Lm12;
then  seq . (Nseq . (n + 1)) <= seq . (Nseq . n) by A1, Th8;
then  (seq * Nseq) . (n + 1) <= seq . (Nseq . n) by FUNCT_2:15;
hence  seq1 . n >= seq1 . (n + 1) by A3, FUNCT_2:15; ::_thesis: verum
end;

theorem :: SEQM_3:26
for seq, seq1 being Real_Sequence st seq is monotone & seq1 is subsequence of seq holds
seq1 is monotone
proof
let seq, seq1 be Real_Sequence; ::_thesis: ( seq is monotone & seq1 is subsequence of seq implies seq1 is monotone )
assume that
A1: seq is monotone and
A2: seq1 is subsequence of seq ; ::_thesis: seq1 is monotone
A3: now__::_thesis:_(_seq_is_non-increasing_implies_seq1_is_monotone_)
assume  seq is non-increasing ; ::_thesis: seq1 is monotone
then  seq1 is non-increasing by A2, Th25;
hence  seq1 is monotone by Def5; ::_thesis: verum
end;
now__::_thesis:_(_seq_is_non-decreasing_implies_seq1_is_monotone_)
assume  seq is non-decreasing ; ::_thesis: seq1 is monotone
then  seq1 is non-decreasing by A2, Th24;
hence  seq1 is monotone by Def5; ::_thesis: verum
end;
hence  seq1 is monotone by A1, A3, Def5; ::_thesis: verum
end;

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
proof
let seq, seq1 be Real_Sequence; ::_thesis: ( seq is bounded_above & seq1 is subsequence of seq implies seq1 is bounded_above )
assume that
A1: seq is bounded_above and
A2: seq1 is subsequence of seq ; ::_thesis: seq1 is bounded_above
consider r1 being real number  such that
A3: for n being Element of NAT holds seq . n < r1 by A1, SEQ_2:def_3;
consider Nseq being increasing sequence of NAT such that
A4: seq1 = seq * Nseq by A2, VALUED_0:def_17;
take r = r1; :: according to SEQ_2:def_3 ::_thesis: for b1 being Element of NAT holds not r <= seq1 . b1
let n be Element of NAT ; ::_thesis: not r <= seq1 . n
 seq1 . n = seq . (Nseq . n) by A4, FUNCT_2:15;
hence  seq1 . n < r by A3; ::_thesis: verum
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
proof
let seq, seq1 be Real_Sequence; ::_thesis: ( seq is bounded_below & seq1 is subsequence of seq implies seq1 is bounded_below )
assume that
A1: seq is bounded_below and
A2: seq1 is subsequence of seq ; ::_thesis: seq1 is bounded_below
consider r1 being real number  such that
A3: for n being Element of NAT holds r1 < seq . n by A1, SEQ_2:def_4;
consider Nseq being increasing sequence of NAT such that
A4: seq1 = seq * Nseq by A2, VALUED_0:def_17;
take r = r1; :: according to SEQ_2:def_4 ::_thesis: for b1 being Element of NAT holds not seq1 . b1 <= r
let n be Element of NAT ; ::_thesis: not seq1 . n <= r
 seq1 . n = seq . (Nseq . n) by A4, FUNCT_2:15;
hence  r < seq1 . n by A3; ::_thesis: verum
end;

theorem :: SEQM_3:29
for seq, seq1 being Real_Sequence st seq is bounded & seq1 is subsequence of seq holds
seq1 is bounded
proof
let seq, seq1 be Real_Sequence; ::_thesis: ( seq is bounded & seq1 is subsequence of seq implies seq1 is bounded )
assume A1: ( seq is bounded & seq1 is subsequence of seq ) ; ::_thesis: seq1 is bounded
hence  seq1 is bounded_above by Th27; :: according to SEQ_2:def_8 ::_thesis: seq1 is bounded_below
thus  seq1 is bounded_below by A1, Th28; ::_thesis: verum
end;

theorem :: SEQM_3:30
for r being real number
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
let r be real number ; ::_thesis: 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 ) )
let seq be Real_Sequence; ::_thesis: ( ( 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 ) )
thus  ( seq is increasing & 0 < r implies r (#) seq is increasing ) ::_thesis: ( ( 0 = r implies r (#) seq is constant ) & ( seq is increasing & r < 0 implies r (#) seq is decreasing ) )
proof
assume that
A1: seq is increasing and
A2: 0 < r ; ::_thesis: r (#) seq is increasing
let n be Element of NAT ; :: according to SEQM_3:def_6 ::_thesis: (r (#) seq) . n < (r (#) seq) . (n + 1)
 seq . n < seq . (n + 1) by A1, Lm6;
then  r * (seq . n) < r * (seq . (n + 1)) by A2, XREAL_1:68;
then  (r (#) seq) . n < r * (seq . (n + 1)) by SEQ_1:9;
hence  (r (#) seq) . n < (r (#) seq) . (n + 1) by SEQ_1:9; ::_thesis: verum
end;
thus  ( 0 = r implies r (#) seq is constant ) ::_thesis: ( seq is increasing & r < 0 implies r (#) seq is decreasing )
proof
assume A3: 0 = r ; ::_thesis: r (#) seq is constant
now__::_thesis:_for_n_being_Nat_holds_(r_(#)_seq)_._n_=_(r_(#)_seq)_._(n_+_1)
let n be Nat; ::_thesis: (r (#) seq) . n = (r (#) seq) . (n + 1)
 ( n in NAT & r * (seq . n) = r * (seq . (n + 1)) ) by A3, ORDINAL1:def_12;
then  (r (#) seq) . n = r * (seq . (n + 1)) by SEQ_1:9;
hence  (r (#) seq) . n = (r (#) seq) . (n + 1) by SEQ_1:9; ::_thesis: verum
end;
hence  r (#) seq is constant by VALUED_0:25; ::_thesis: verum
end;
assume that
A4: seq is increasing and
A5: r < 0 ; ::_thesis: r (#) seq is decreasing
let n be Element of NAT ; :: according to SEQM_3:def_7 ::_thesis: (r (#) seq) . n > (r (#) seq) . (n + 1)
 seq . n < seq . (n + 1) by A4, Lm6;
then  r * (seq . (n + 1)) < r * (seq . n) by A5, XREAL_1:69;
then  (r (#) seq) . (n + 1) < r * (seq . n) by SEQ_1:9;
hence  (r (#) seq) . n > (r (#) seq) . (n + 1) by SEQ_1:9; ::_thesis: verum
end;

theorem :: SEQM_3:31
for r being real number
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
let r be real number ; ::_thesis: 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 ) )
let seq be Real_Sequence; ::_thesis: ( ( seq is decreasing & 0 < r implies r (#) seq is decreasing ) & ( seq is decreasing & r < 0 implies r (#) seq is increasing ) )
thus  ( seq is decreasing & 0 < r implies r (#) seq is decreasing ) ::_thesis: ( seq is decreasing & r < 0 implies r (#) seq is increasing )
proof
assume that
A1: seq is decreasing and
A2: 0 < r ; ::_thesis: r (#) seq is decreasing
let n be Element of NAT ; :: according to SEQM_3:def_7 ::_thesis: (r (#) seq) . n > (r (#) seq) . (n + 1)
 seq . (n + 1) < seq . n by A1, Lm7;
then  r * (seq . (n + 1)) < r * (seq . n) by A2, XREAL_1:68;
then  (r (#) seq) . (n + 1) < r * (seq . n) by SEQ_1:9;
hence  (r (#) seq) . n > (r (#) seq) . (n + 1) by SEQ_1:9; ::_thesis: verum
end;
assume that
A3: seq is decreasing and
A4: r < 0 ; ::_thesis: r (#) seq is increasing
let n be Element of NAT ; :: according to SEQM_3:def_6 ::_thesis: (r (#) seq) . n < (r (#) seq) . (n + 1)
 seq . (n + 1) < seq . n by A3, Lm7;
then  r * (seq . n) < r * (seq . (n + 1)) by A4, XREAL_1:69;
then  (r (#) seq) . n < r * (seq . (n + 1)) by SEQ_1:9;
hence  (r (#) seq) . n < (r (#) seq) . (n + 1) by SEQ_1:9; ::_thesis: verum
end;

theorem :: SEQM_3:32
for r being real number
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
let r be real number ; ::_thesis: 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 ) )
let seq be Real_Sequence; ::_thesis: ( ( seq is non-decreasing & 0 <= r implies r (#) seq is non-decreasing ) & ( seq is non-decreasing & r <= 0 implies r (#) seq is non-increasing ) )
thus  ( seq is non-decreasing & 0 <= r implies r (#) seq is non-decreasing ) ::_thesis: ( seq is non-decreasing & r <= 0 implies r (#) seq is non-increasing )
proof
assume that
A1: seq is non-decreasing and
A2: 0 <= r ; ::_thesis: r (#) seq is non-decreasing
let n be Element of NAT ; :: according to SEQM_3:def_8 ::_thesis: (r (#) seq) . n <= (r (#) seq) . (n + 1)
 seq . n <= seq . (n + 1) by A1, Lm8;
then  r * (seq . n) <= r * (seq . (n + 1)) by A2, XREAL_1:64;
then  (r (#) seq) . n <= r * (seq . (n + 1)) by SEQ_1:9;
hence  (r (#) seq) . n <= (r (#) seq) . (n + 1) by SEQ_1:9; ::_thesis: verum
end;
assume that
A3: seq is non-decreasing and
A4: r <= 0 ; ::_thesis: r (#) seq is non-increasing
let n be Element of NAT ; :: according to SEQM_3:def_9 ::_thesis: (r (#) seq) . n >= (r (#) seq) . (n + 1)
 seq . n <= seq . (n + 1) by A3, Lm8;
then  r * (seq . (n + 1)) <= r * (seq . n) by A4, XREAL_1:65;
then  (r (#) seq) . (n + 1) <= r * (seq . n) by SEQ_1:9;
hence  (r (#) seq) . n >= (r (#) seq) . (n + 1) by SEQ_1:9; ::_thesis: verum
end;

theorem :: SEQM_3:33
for r being real number
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
let r be real number ; ::_thesis: 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 ) )
let seq be Real_Sequence; ::_thesis: ( ( seq is non-increasing & 0 <= r implies r (#) seq is non-increasing ) & ( seq is non-increasing & r <= 0 implies r (#) seq is non-decreasing ) )
thus  ( seq is non-increasing & 0 <= r implies r (#) seq is non-increasing ) ::_thesis: ( seq is non-increasing & r <= 0 implies r (#) seq is non-decreasing )
proof
assume that
A1: seq is non-increasing and
A2: 0 <= r ; ::_thesis: r (#) seq is non-increasing
let n be Element of NAT ; :: according to SEQM_3:def_9 ::_thesis: (r (#) seq) . n >= (r (#) seq) . (n + 1)
 seq . (n + 1) <= seq . n by A1, Lm9;
then  r * (seq . (n + 1)) <= r * (seq . n) by A2, XREAL_1:64;
then  (r (#) seq) . (n + 1) <= r * (seq . n) by SEQ_1:9;
hence  (r (#) seq) . n >= (r (#) seq) . (n + 1) by SEQ_1:9; ::_thesis: verum
end;
assume that
A3: seq is non-increasing and
A4: r <= 0 ; ::_thesis: r (#) seq is non-decreasing
let n be Element of NAT ; :: according to SEQM_3:def_8 ::_thesis: (r (#) seq) . n <= (r (#) seq) . (n + 1)
 seq . (n + 1) <= seq . n by A3, Lm9;
then  r * (seq . n) <= r * (seq . (n + 1)) by A4, XREAL_1:65;
then  (r (#) seq) . n <= r * (seq . (n + 1)) by SEQ_1:9;
hence  (r (#) seq) . n <= (r (#) seq) . (n + 1) by SEQ_1:9; ::_thesis: verum
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 ) )
proof
let seq, seq1 be Real_Sequence; ::_thesis: ( ( 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 ) )
thus  ( seq is increasing & seq1 is increasing implies seq + seq1 is increasing ) ::_thesis: ( ( 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
assume A1: ( seq is increasing & seq1 is increasing ) ; ::_thesis: seq + seq1 is increasing
let n be Element of NAT ; :: according to SEQM_3:def_6 ::_thesis: (seq + seq1) . n < (seq + seq1) . (n + 1)
 ( seq . n < seq . (n + 1) & seq1 . n < seq1 . (n + 1) ) by A1, Lm6;
then  (seq . n) + (seq1 . n) < (seq . (n + 1)) + (seq1 . (n + 1)) by XREAL_1:8;
then  (seq + seq1) . n < (seq . (n + 1)) + (seq1 . (n + 1)) by SEQ_1:7;
hence  (seq + seq1) . n < (seq + seq1) . (n + 1) by SEQ_1:7; ::_thesis: verum
end;
thus  ( seq is decreasing & seq1 is decreasing implies seq + seq1 is decreasing ) ::_thesis: ( ( 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
assume A2: ( seq is decreasing & seq1 is decreasing ) ; ::_thesis: seq + seq1 is decreasing
let n be Element of NAT ; :: according to SEQM_3:def_7 ::_thesis: (seq + seq1) . n > (seq + seq1) . (n + 1)
 ( seq . (n + 1) < seq . n & seq1 . (n + 1) < seq1 . n ) by A2, Lm7;
then  (seq . (n + 1)) + (seq1 . (n + 1)) < (seq . n) + (seq1 . n) by XREAL_1:8;
then  (seq + seq1) . (n + 1) < (seq . n) + (seq1 . n) by SEQ_1:7;
hence  (seq + seq1) . n > (seq + seq1) . (n + 1) by SEQ_1:7; ::_thesis: verum
end;
thus  ( seq is non-decreasing & seq1 is non-decreasing implies seq + seq1 is non-decreasing ) ::_thesis: ( seq is non-increasing & seq1 is non-increasing implies seq + seq1 is non-increasing )
proof
assume A3: ( seq is non-decreasing & seq1 is non-decreasing ) ; ::_thesis: seq + seq1 is non-decreasing
let n be Element of NAT ; :: according to SEQM_3:def_8 ::_thesis: (seq + seq1) . n <= (seq + seq1) . (n + 1)
 ( seq . n <= seq . (n + 1) & seq1 . n <= seq1 . (n + 1) ) by A3, Lm8;
then  (seq . n) + (seq1 . n) <= (seq . (n + 1)) + (seq1 . (n + 1)) by XREAL_1:7;
then  (seq + seq1) . n <= (seq . (n + 1)) + (seq1 . (n + 1)) by SEQ_1:7;
hence  (seq + seq1) . n <= (seq + seq1) . (n + 1) by SEQ_1:7; ::_thesis: verum
end;
assume A4: ( seq is non-increasing & seq1 is non-increasing ) ; ::_thesis: seq + seq1 is non-increasing
let n be Element of NAT ; :: according to SEQM_3:def_9 ::_thesis: (seq + seq1) . n >= (seq + seq1) . (n + 1)
 ( seq . (n + 1) <= seq . n & seq1 . (n + 1) <= seq1 . n ) by A4, Lm9;
then  (seq . (n + 1)) + (seq1 . (n + 1)) <= (seq . n) + (seq1 . n) by XREAL_1:7;
then  (seq + seq1) . (n + 1) <= (seq . n) + (seq1 . n) by SEQ_1:7;
hence  (seq + seq1) . n >= (seq + seq1) . (n + 1) by SEQ_1:7; ::_thesis: verum
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 ) )
proof
let seq, seq1 be Real_Sequence; ::_thesis: ( ( 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 ) )
thus  ( seq is increasing & seq1 is constant implies seq + seq1 is increasing ) ::_thesis: ( ( 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
assume that
A1: seq is increasing and
A2: seq1 is constant ; ::_thesis: seq + seq1 is increasing
let n be Element of NAT ; :: according to SEQM_3:def_6 ::_thesis: (seq + seq1) . n < (seq + seq1) . (n + 1)
consider r1 being Real such that
A3: for n being Nat holds seq1 . n = r1 by A2, VALUED_0:def_18;
 seq . n < seq . (n + 1) by A1, Lm6;
then  (seq . n) + r1 < (seq . (n + 1)) + r1 by XREAL_1:6;
then  (seq . n) + (seq1 . n) < (seq . (n + 1)) + r1 by A3;
then  (seq . n) + (seq1 . n) < (seq . (n + 1)) + (seq1 . (n + 1)) by A3;
then  (seq + seq1) . n < (seq . (n + 1)) + (seq1 . (n + 1)) by SEQ_1:7;
hence  (seq + seq1) . n < (seq + seq1) . (n + 1) by SEQ_1:7; ::_thesis: verum
end;
thus  ( seq is decreasing & seq1 is constant implies seq + seq1 is decreasing ) ::_thesis: ( ( 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
assume that
A4: seq is decreasing and
A5: seq1 is constant ; ::_thesis: seq + seq1 is decreasing
let n be Element of NAT ; :: according to SEQM_3:def_7 ::_thesis: (seq + seq1) . n > (seq + seq1) . (n + 1)
consider r1 being Real such that
A6: for n being Nat holds seq1 . n = r1 by A5, VALUED_0:def_18;
 seq . (n + 1) < seq . n by A4, Lm7;
then  (seq . (n + 1)) + r1 < (seq . n) + r1 by XREAL_1:6;
then  (seq . (n + 1)) + (seq1 . (n + 1)) < (seq . n) + r1 by A6;
then  (seq . (n + 1)) + (seq1 . (n + 1)) < (seq . n) + (seq1 . n) by A6;
then  (seq + seq1) . (n + 1) < (seq . n) + (seq1 . n) by SEQ_1:7;
hence  (seq + seq1) . n > (seq + seq1) . (n + 1) by SEQ_1:7; ::_thesis: verum
end;
thus  ( seq is non-decreasing & seq1 is constant implies seq + seq1 is non-decreasing ) by Th34; ::_thesis: ( seq is non-increasing & seq1 is constant implies seq + seq1 is non-increasing )
assume  ( seq is non-increasing & seq1 is constant ) ; ::_thesis: seq + seq1 is non-increasing
hence  seq + seq1 is non-increasing by Th34; ::_thesis: verum
end;

theorem Th36: :: SEQM_3:36
for r being real number
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
let r be real number ; ::_thesis: 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 ) )
let seq be Real_Sequence; ::_thesis: ( ( 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 ) )
thus  ( seq is bounded_above & 0 < r implies r (#) seq is bounded_above ) ; ::_thesis: ( ( 0 = r implies r (#) seq is bounded ) & ( seq is bounded_above & r < 0 implies r (#) seq is bounded_below ) )
thus  ( 0 = r implies r (#) seq is bounded ) ::_thesis: ( seq is bounded_above & r < 0 implies r (#) seq is bounded_below )
proof
assume A1: 0 = r ; ::_thesis: r (#) seq is bounded
now__::_thesis:_for_n_being_Element_of_NAT_holds_(r_(#)_seq)_._n_<_1
let n be Element of NAT ; ::_thesis: (r (#) seq) . n < 1
 (r (#) seq) . n = 0 * (seq . n) by A1, SEQ_1:9;
hence  (r (#) seq) . n < 1 ; ::_thesis: verum
end;
hence  r (#) seq is bounded_above by SEQ_2:def_3; :: according to SEQ_2:def_8 ::_thesis: r (#) seq is bounded_below
take p = - 1; :: according to SEQ_2:def_4 ::_thesis: for b1 being Element of NAT holds not (r (#) seq) . b1 <= p
let n be Element of NAT ; ::_thesis: not (r (#) seq) . n <= p
 ( - 1 < 0 & r * (seq . n) = 0 ) by A1;
hence  p < (r (#) seq) . n by SEQ_1:9; ::_thesis: verum
end;
assume that
A2: seq is bounded_above and
A3: r < 0 ; ::_thesis: r (#) seq is bounded_below
consider r1 being real number  such that
A4: for n being Element of NAT holds seq . n < r1 by A2, SEQ_2:def_3;
take p = r * (abs r1); :: according to SEQ_2:def_4 ::_thesis: for b1 being Element of NAT holds not (r (#) seq) . b1 <= p
let n be Element of NAT ; ::_thesis: not (r (#) seq) . n <= p
 r1 <= abs r1 by ABSVALUE:4;
then  seq . n < abs r1 by A4, XXREAL_0:2;
then  r * (abs r1) < r * (seq . n) by A3, XREAL_1:69;
hence  p < (r (#) seq) . n by SEQ_1:9; ::_thesis: verum
end;

theorem :: SEQM_3:37
for seq being Real_Sequence holds
( ( seq is bounded implies for r being real number 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
let seq be Real_Sequence; ::_thesis: ( ( seq is bounded implies for r being real number 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 ) )
thus  ( seq is bounded implies for r being real number holds r (#) seq is bounded ) ::_thesis: ( ( seq is bounded implies - seq is bounded ) & ( seq is bounded implies abs seq is bounded ) & ( abs seq is bounded implies seq is bounded ) )
proof
assume A1: seq is bounded ; ::_thesis: for r being real number holds r (#) seq is bounded
let r be real number ; ::_thesis: r (#) seq is bounded
percases ( 0 < r or 0 = r or r < 0 ) ;
suppose 0 < r ; ::_thesis: r (#) seq is bounded
hence  r (#) seq is bounded by A1; ::_thesis: verum
end;
suppose 0 = r ; ::_thesis: r (#) seq is bounded
hence  r (#) seq is bounded by Th36; ::_thesis: verum
end;
suppose r < 0 ; ::_thesis: r (#) seq is bounded
hence  r (#) seq is bounded by A1; ::_thesis: verum
end;
end;
end;
thus  ( seq is bounded implies - seq is bounded ) ; ::_thesis: ( ( seq is bounded implies abs seq is bounded ) & ( abs seq is bounded implies seq is bounded ) )
thus  ( seq is bounded implies abs seq is bounded ) ; ::_thesis: ( abs seq is bounded implies seq is bounded )
assume  abs seq is bounded ; ::_thesis: seq is bounded
then consider r being real number  such that
A2: 0 < r and
A3: for n being Element of NAT holds abs ((abs seq) . n) < r by SEQ_2:3;
now__::_thesis:_for_n_being_Element_of_NAT_holds_abs_(seq_._n)_<_r
let n be Element of NAT ; ::_thesis: abs (seq . n) < r
abs ((abs seq) . n) = abs (abs (seq . n)) by SEQ_1:12
.= abs (seq . n) ;
hence  abs (seq . n) < r by A3; ::_thesis: verum
end;
hence  seq is bounded by A2, SEQ_2:3; ::_thesis: verum
end;

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
proof
let seq, seq1 be Real_Sequence; ::_thesis: ( seq is bounded_above & seq1 is non-increasing implies seq + seq1 is bounded_above )
assume that
A1: seq is bounded_above and
A2: seq1 is non-increasing ; ::_thesis: seq + seq1 is bounded_above
consider r1 being real number  such that
A3: for n being Element of NAT holds seq . n < r1 by A1, SEQ_2:def_3;
take r = r1 + (seq1 . 0); :: according to SEQ_2:def_3 ::_thesis: for b1 being Element of NAT holds not r <= (seq + seq1) . b1
let n be Element of NAT ; ::_thesis: not r <= (seq + seq1) . n
 seq1 . n <= seq1 . 0 by A2, Th12;
then  (seq . n) + (seq1 . n) < r1 + (seq1 . 0) by A3, XREAL_1:8;
hence  (seq + seq1) . n < r by SEQ_1:7; ::_thesis: verum
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
proof
let seq, seq1 be Real_Sequence; ::_thesis: ( seq is bounded_below & seq1 is non-decreasing implies seq + seq1 is bounded_below )
assume that
A1: seq is bounded_below and
A2: seq1 is non-decreasing ; ::_thesis: seq + seq1 is bounded_below
consider r1 being real number  such that
A3: for n being Element of NAT holds r1 < seq . n by A1, SEQ_2:def_4;
take r = r1 + (seq1 . 0); :: according to SEQ_2:def_4 ::_thesis: for b1 being Element of NAT holds not (seq + seq1) . b1 <= r
let n be Element of NAT ; ::_thesis: not (seq + seq1) . n <= r
 seq1 . 0 <= seq1 . n by A2, Th11;
then  r1 + (seq1 . 0) < (seq . n) + (seq1 . n) by A3, XREAL_1:8;
hence  r < (seq + seq1) . n by SEQ_1:7; ::_thesis: verum
end;

theorem :: SEQM_3:40
( incl NAT is increasing & incl NAT is natural-valued ) by Lm10;

registration
cluster  ->  natural-valued for FinSequence of NAT ;
coherence
 for b1 being FinSequence of NAT holds b1 is natural-valued ;
end;

begin


theorem Th41: :: SEQM_3:41
for r, s being Real holds
( abs (r - s) = 1 iff ( ( r > s & r = s + 1 ) or ( r < s & s = r + 1 ) ) )
proof
let r, s be Real; ::_thesis: ( abs (r - s) = 1 iff ( ( r > s & r = s + 1 ) or ( r < s & s = r + 1 ) ) )
thus  ( not abs (r - s) = 1 or ( r > s & r = s + 1 ) or ( r < s & s = r + 1 ) ) ::_thesis: ( ( ( r > s & r = s + 1 ) or ( r < s & s = r + 1 ) ) implies abs (r - s) = 1 )
proof
assume A1: abs (r - s) = 1 ; ::_thesis: ( ( r > s & r = s + 1 ) or ( r < s & s = r + 1 ) )
now__::_thesis:_(_(_r_>_s_&_(_(_r_>_s_&_r_=_s_+_1_)_or_(_r_<_s_&_s_=_r_+_1_)_)_)_or_(_r_=_s_&_contradiction_)_or_(_r_<_s_&_(_(_r_>_s_&_r_=_s_+_1_)_or_(_r_<_s_&_s_=_r_+_1_)_)_)_)
percases ( r > s or r = s or r < s ) by XXREAL_0:1;
caseA2: r > s ; ::_thesis: ( ( r > s & r = s + 1 ) or ( r < s & s = r + 1 ) )
then  0 < r - s by XREAL_1:50;
then  r - s = 1 by A1, ABSVALUE:def_1;
hence  ( ( r > s & r = s + 1 ) or ( r < s & s = r + 1 ) ) by A2; ::_thesis: verum
end;
case r = s ; ::_thesis: contradiction
hence  contradiction by A1, ABSVALUE:2; ::_thesis: verum
end;
caseA3: r < s ; ::_thesis: ( ( r > s & r = s + 1 ) or ( r < s & s = r + 1 ) )
then A4: 0 < s - r by XREAL_1:50;
1 = abs (- (r - s)) by A1, COMPLEX1:52
.= s - r by A4, ABSVALUE:def_1 ;
hence  ( ( r > s & r = s + 1 ) or ( r < s & s = r + 1 ) ) by A3; ::_thesis: verum
end;
end;
end;
hence  ( ( r > s & r = s + 1 ) or ( r < s & s = r + 1 ) ) ; ::_thesis: verum
end;
assume A5: ( ( r > s & r = s + 1 ) or ( r < s & s = r + 1 ) ) ; ::_thesis: abs (r - s) = 1
percases ( ( r > s & r = s + 1 ) or ( s > r & s = r + 1 ) ) by A5;
suppose ( r > s & r = s + 1 ) ; ::_thesis: abs (r - s) = 1
hence  abs (r - s) = 1 by ABSVALUE:def_1; ::_thesis: verum
end;
supposeA6: ( s > r & s = r + 1 ) ; ::_thesis: abs (r - s) = 1
thus  abs (r - s) = abs (- (r - s)) by COMPLEX1:52
.= 1 by A6, ABSVALUE:def_1 ; ::_thesis: verum
end;
end;
end;

theorem :: SEQM_3:42
for i, j, n, m being Element of NAT holds
( (abs (i - j)) + (abs (n - m)) = 1 iff ( ( abs (i - j) = 1 & n = m ) or ( abs (n - m) = 1 & i = j ) ) )
proof
let i, j, n, m be Element of NAT ; ::_thesis: ( (abs (i - j)) + (abs (n - m)) = 1 iff ( ( abs (i - j) = 1 & n = m ) or ( abs (n - m) = 1 & i = j ) ) )
thus  ( not (abs (i - j)) + (abs (n - m)) = 1 or ( abs (i - j) = 1 & n = m ) or ( abs (n - m) = 1 & i = j ) ) ::_thesis: ( ( ( abs (i - j) = 1 & n = m ) or ( abs (n - m) = 1 & i = j ) ) implies (abs (i - j)) + (abs (n - m)) = 1 )
proof
assume A1: (abs (i - j)) + (abs (n - m)) = 1 ; ::_thesis: ( ( abs (i - j) = 1 & n = m ) or ( abs (n - m) = 1 & i = j ) )
now__::_thesis:_(_(_abs_(i_-_j)_=_1_&_n_=_m_)_or_(_abs_(n_-_m)_=_1_&_i_=_j_)_)
percases ( n = m or n <> m ) ;
supposeA2: n = m ; ::_thesis: ( ( abs (i - j) = 1 & n = m ) or ( abs (n - m) = 1 & i = j ) )
then 1 = (abs (i - j)) + 0 by A1, ABSVALUE:2
.= abs (i - j) ;
hence  ( ( abs (i - j) = 1 & n = m ) or ( abs (n - m) = 1 & i = j ) ) by A2; ::_thesis: verum
end;
supposeA3: n <> m ; ::_thesis: ( ( abs (i - j) = 1 & n = m ) or ( abs (n - m) = 1 & i = j ) )
now__::_thesis:_(_(_abs_(i_-_j)_=_1_&_n_=_m_)_or_(_abs_(n_-_m)_=_1_&_i_=_j_)_)
percases ( n < m or n > m ) by A3, XXREAL_0:1;
supposeA4: n < m ; ::_thesis: ( ( abs (i - j) = 1 & n = m ) or ( abs (n - m) = 1 & i = j ) )
then reconsider l = m - n as Element of NAT by INT_1:5;
 0 < l by A4, XREAL_1:50;
then A5: 0 + 1 <= l by NAT_1:13;
A6: abs (- (m - n)) = abs l by COMPLEX1:52;
then A7: abs (n - m) = abs l ;
A8: abs l = l by ABSVALUE:def_1;
then A9: l <= 1 by A1, A6, COMPLEX1:46, XREAL_1:31;
then  l = 1 by A5, XXREAL_0:1;
then  i - j = 0 by A1, A8, A7, ABSVALUE:2;
hence  ( ( abs (i - j) = 1 & n = m ) or ( abs (n - m) = 1 & i = j ) ) by A6, A5, A8, A9, XXREAL_0:1; ::_thesis: verum
end;
supposeA10: n > m ; ::_thesis: ( ( abs (i - j) = 1 & n = m ) or ( abs (n - m) = 1 & i = j ) )
then reconsider l = n - m as Element of NAT by INT_1:5;
 0 < l by A10, XREAL_1:50;
then A11: 0 + 1 <= l by NAT_1:13;
A12: abs (n - m) = l by ABSVALUE:def_1;
then A13: l <= 1 by A1, COMPLEX1:46, XREAL_1:31;
then  l = 1 by A11, XXREAL_0:1;
then  i - j = 0 by A1, A12, ABSVALUE:2;
hence  ( ( abs (i - j) = 1 & n = m ) or ( abs (n - m) = 1 & i = j ) ) by A11, A12, A13, XXREAL_0:1; ::_thesis: verum
end;
end;
end;
hence  ( ( abs (i - j) = 1 & n = m ) or ( abs (n - m) = 1 & i = j ) ) ; ::_thesis: verum
end;
end;
end;
hence  ( ( abs (i - j) = 1 & n = m ) or ( abs (n - m) = 1 & i = j ) ) ; ::_thesis: verum
end;
assume A14: ( ( abs (i - j) = 1 & n = m ) or ( abs (n - m) = 1 & i = j ) ) ; ::_thesis: (abs (i - j)) + (abs (n - m)) = 1
now__::_thesis:_(abs_(i_-_j))_+_(abs_(n_-_m))_=_1
percases ( ( abs (i - j) = 1 & n = m ) or ( abs (n - m) = 1 & i = j ) ) by A14;
supposeA15: ( abs (i - j) = 1 & n = m ) ; ::_thesis: (abs (i - j)) + (abs (n - m)) = 1
then  abs (n - m) = 0 by ABSVALUE:2;
hence  (abs (i - j)) + (abs (n - m)) = 1 by A15; ::_thesis: verum
end;
supposeA16: ( abs (n - m) = 1 & i = j ) ; ::_thesis: (abs (i - j)) + (abs (n - m)) = 1
then  abs (i - j) = 0 by ABSVALUE:2;
hence  (abs (i - j)) + (abs (n - m)) = 1 by A16; ::_thesis: verum
end;
end;
end;
hence  (abs (i - j)) + (abs (n - m)) = 1 ; ::_thesis: verum
end;

theorem :: SEQM_3:43
for n being Element of NAT holds
( n > 1 iff ex m being Element of NAT st
( n = m + 1 & m > 0 ) )
proof
let n be Element of NAT ; ::_thesis: ( n > 1 iff ex m being Element of NAT st
( n = m + 1 & m > 0 ) )
thus  ( n > 1 implies ex m being Element of NAT st
( n = m + 1 & m > 0 ) ) ::_thesis: ( ex m being Element of NAT st
( n = m + 1 & m > 0 ) implies n > 1 )
proof
assume A1: 1 < n ; ::_thesis: ex m being Element of NAT st
( n = m + 1 & m > 0 )
then consider m being Nat such that
A2: n = m + 1 by NAT_1:6;
reconsider m = m as Element of NAT by ORDINAL1:def_12;
take  m ; ::_thesis: ( n = m + 1 & m > 0 )
 m <> 0 by A1, A2;
hence  ( n = m + 1 & m > 0 ) by A2; ::_thesis: verum
end;
given m being Element of NAT  such that A3: ( n = m + 1 & m > 0 ) ; ::_thesis: n > 1
 0 + 1 < n by A3, XREAL_1:6;
hence  n > 1 ; ::_thesis: verum
end;

theorem :: SEQM_3:44
for f being FinSequence
for n, m, k being Element of 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
let f be FinSequence; ::_thesis: for n, m, k being Element of 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)
let n, m, k be Element of NAT ; ::_thesis: ( len f = m + 1 & n in dom f & k in Seg m & not (Del (f,n)) . k = f . k implies (Del (f,n)) . k = f . (k + 1) )
assume that
A1: ( len f = m + 1 & n in dom f ) and
A2: k in Seg m ; ::_thesis: ( (Del (f,n)) . k = f . k or (Del (f,n)) . k = f . (k + 1) )
set X = (dom f) \ {n};
A3: dom f = Seg (len f) by FINSEQ_1:def_3;
then A4: ( n <= k & k <= m implies (Sgm ((dom f) \ {n})) . k = k + 1 ) by A1, A2, FINSEQ_3:108;
 (dom f) \ {n} c= Seg (len f) by A3, XBOOLE_1:36;
then  rng (Sgm ((dom f) \ {n})) = (dom f) \ {n} by FINSEQ_1:def_13;
then A5: dom (f * (Sgm ((dom f) \ {n}))) = dom (Sgm ((dom f) \ {n})) by RELAT_1:27, XBOOLE_1:36;
A6: ( dom (Sgm ((dom f) \ {n})) = Seg (len (Sgm ((dom f) \ {n}))) & Del (f,n) = f * (Sgm ((dom f) \ {n})) ) by FINSEQ_1:def_3, FINSEQ_3:def_2;
A7: len (Sgm ((dom f) \ {n})) = m by A1, A3, FINSEQ_3:107;
 ( 1 <= k & k < n implies (Sgm ((dom f) \ {n})) . k = k ) by A1, A2, A3, FINSEQ_3:108;
hence  ( (Del (f,n)) . k = f . k or (Del (f,n)) . k = f . (k + 1) ) by A2, A6, A5, A7, A4, FINSEQ_3:25, FUNCT_1:12; ::_thesis: verum
end;

definition
let f be FinSequence;
redefine attr f is constant  means :: SEQM_3:def 10
 for n, m being Element of NAT st n in dom f & m in dom f holds
f . n = f . m;
compatibility
 ( f is constant iff for n, m being Element of NAT st n in dom f & m in dom f holds
f . n = f . m )
proof
thus  ( f is constant implies for n, m being Element of NAT st n in dom f & m in dom f holds
f . n = f . m ) by FUNCT_1:def_10; ::_thesis: ( ( for n, m being Element of NAT st n in dom f & m in dom f holds
f . n = f . m ) implies f is constant )
assume A1: for n, m being Element of NAT st n in dom f & m in dom f holds
f . n = f . m ; ::_thesis: f is constant
let n, m be set ; :: according to FUNCT_1:def_10 ::_thesis: ( not n in dom f or not m in dom f or f . n = f . m )
assume  ( n in dom f & m in dom f ) ; ::_thesis: f . n = f . m
hence  f . n = f . m by A1; ::_thesis: verum
end;
end;

:: deftheorem  defines constant SEQM_3:def_10_:_
 for f being FinSequence holds
( f is constant iff for n, m being Element of NAT st n in dom f & m in dom f holds
f . n = f . m );

registration
cluster  ->  real-valued for FinSequence of REAL ;
coherence
 for b1 being FinSequence of REAL holds b1 is real-valued ;
end;

registration
cluster Relation-like NAT -defined REAL -valued Function-like non empty complex-valued ext-real-valued real-valued increasing V54() FinSequence-like FinSubsequence-like for FinSequence of REAL ;
existence
 ex b1 being FinSequence of REAL st
( not b1 is empty & b1 is increasing )
proof
take v = <*0*>; ::_thesis: ( not v is empty & v is increasing )
thus  not v is empty ; ::_thesis: v is increasing
let n be Element of NAT ; :: according to SEQM_3:def_1 ::_thesis: for n being Element of NAT st n in dom v & n in dom v & n < n holds
v . n < v . n
let m be Element of NAT ; ::_thesis: ( n in dom v & m in dom v & n < m implies v . n < v . m )
assume that
A1: n in dom v and
A2: m in dom v ; ::_thesis: ( not n < m or v . n < v . m )
A3: dom <*0*> = {1} by FINSEQ_1:2, FINSEQ_1:38;
then  n = 1 by A1, TARSKI:def_1;
hence  ( not n < m or v . n < v . m ) by A3, A2, TARSKI:def_1; ::_thesis: verum
end;
end;

registration
cluster Relation-like NAT -defined REAL -valued Function-like constant complex-valued ext-real-valued real-valued V54() FinSequence-like FinSubsequence-like for FinSequence of REAL ;
existence
 ex b1 being FinSequence of REAL st b1 is constant
proof
take v = <*> REAL; ::_thesis: v is constant
let n be Element of NAT ; :: according to SEQM_3:def_10 ::_thesis: for m being Element of NAT st n in dom v & m in dom v holds
v . n = v . m
let m be Element of NAT ; ::_thesis: ( n in dom v & m in dom v implies v . n = v . m )
assume that
 n in dom v and
 m in dom v ; ::_thesis: v . n = v . m
thus  v . n = v . m ; ::_thesis: verum
end;
end;

theorem Th45: :: SEQM_3:45
for v being FinSequence of REAL
for n, i, m being Element of NAT st v <> {} & rng v c= Seg n & v . (len v) = n & ( for k being Element of NAT st 1 <= k & k <= (len v) - 1 holds
for r, s being Real st r = v . k & s = v . (k + 1) & not abs (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 Element of NAT st k in dom v & v . k = i holds
k <= m ) holds
( m + 1 in dom v & v . (m + 1) = i + 1 )
proof
let v be FinSequence of REAL ; ::_thesis: for n, i, m being Element of NAT st v <> {} & rng v c= Seg n & v . (len v) = n & ( for k being Element of NAT st 1 <= k & k <= (len v) - 1 holds
for r, s being Real st r = v . k & s = v . (k + 1) & not abs (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 Element of NAT st k in dom v & v . k = i holds
k <= m ) holds
( m + 1 in dom v & v . (m + 1) = i + 1 )
let n, i, m be Element of NAT ; ::_thesis: ( v <> {} & rng v c= Seg n & v . (len v) = n & ( for k being Element of NAT st 1 <= k & k <= (len v) - 1 holds
for r, s being Real st r = v . k & s = v . (k + 1) & not abs (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 Element of NAT st k in dom v & v . k = i holds
k <= m ) implies ( m + 1 in dom v & v . (m + 1) = i + 1 ) )
assume that
A1: v <> {} and
A2: rng v c= Seg n and
A3: v . (len v) = n and
A4: for k being Element of NAT st 1 <= k & k <= (len v) - 1 holds
for r, s being Real st r = v . k & s = v . (k + 1) & not abs (r - s) = 1 holds
r = s and
A5: i in Seg n and
A6: i + 1 in Seg n and
A7: m in dom v and
A8: v . m = i and
A9: for k being Element of NAT st k in dom v & v . k = i holds
k <= m ; ::_thesis: ( m + 1 in dom v & v . (m + 1) = i + 1 )
A10: m <= len v by A7, FINSEQ_3:25;
 0 + 1 <= len v by A1, NAT_1:13;
then A11: len v in dom v by FINSEQ_3:25;
reconsider r = v . (m + 1) as Real ;
A12: i <= n by A5, FINSEQ_1:1;
A13: 1 <= m by A7, FINSEQ_3:25;
A14: i + 1 <= n by A6, FINSEQ_1:1;
A15: now__::_thesis:_m_+_1_in_dom_v
assume  not m + 1 in dom v ; ::_thesis: contradiction
then  ( 1 > m + 1 or m + 1 > len v ) by FINSEQ_3:25;
then A16: len v <= m by NAT_1:11, NAT_1:13;
 i < n by A14, NAT_1:13;
hence  contradiction by A3, A8, A10, A16, XXREAL_0:1; ::_thesis: verum
end;
then A17: m + 1 <= len v by FINSEQ_3:25;
then A18: m < len v by NAT_1:13;
A19: m <= (len v) - 1 by A17, XREAL_1:19;
now__::_thesis:_(_(_abs_(i_-_r)_=_1_&_m_+_1_in_dom_v_&_v_._(m_+_1)_=_i_+_1_)_or_(_i_=_r_&_contradiction_)_)
percases ( abs (i - r) = 1 or i = r ) by A4, A8, A13, A19;
caseA20: abs (i - r) = 1 ; ::_thesis: ( m + 1 in dom v & v . (m + 1) = i + 1 )
now__::_thesis:_(_(_i_>_r_&_i_=_r_+_1_&_contradiction_)_or_(_i_<_r_&_r_=_i_+_1_&_m_+_1_in_dom_v_&_v_._(m_+_1)_=_i_+_1_)_)
percases ( ( i > r & i = r + 1 ) or ( i < r & r = i + 1 ) ) by A20, Th41;
caseA21: ( i > r & i = r + 1 ) ; ::_thesis: contradiction
defpred S1[ set ] means  for k being Element of NAT
for r being Real st k = $1 & k > 0 & m + k in dom v & r = v . (m + k) holds
r < i;
A22: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A23: S1[k] ; ::_thesis: S1[k + 1]
let j be Element of NAT ; ::_thesis: for r being Real st j = k + 1 & j > 0 & m + j in dom v & r = v . (m + j) holds
r < i
let s be Real; ::_thesis: ( j = k + 1 & j > 0 & m + j in dom v & s = v . (m + j) implies s < i )
assume that
A24: j = k + 1 and
A25: j > 0 and
A26: m + j in dom v and
A27: s = v . (m + j) ; ::_thesis: s < i
now__::_thesis:_s_<_i
percases ( k = 0 or k <> 0 ) ;
suppose k = 0 ; ::_thesis: s < i
hence  s < i by A21, A24, A27; ::_thesis: verum
end;
supposeA28: k <> 0 ; ::_thesis: s < i
A29: m + k <= (m + k) + 1 by NAT_1:11;
 m <= m + k by NAT_1:11;
then A30: 1 <= m + k by A13, XXREAL_0:2;
A31: m + (k + 1) <= len v by A24, A26, FINSEQ_3:25;
then  m + k <= len v by A29, XXREAL_0:2;
then A32: m + k in dom v by A30, FINSEQ_3:25;
then  v . (m + k) in rng v by FUNCT_1:def_3;
then  v . (m + k) in Seg n by A2;
then reconsider r1 = v . (m + k) as Element of NAT ;
A33: r1 < i by A23, A28, A32;
A34: m + k <= (len v) - 1 by A29, A31, XREAL_1:19;
now__::_thesis:_s_<_i
percases ( abs (r1 - s) = 1 or r1 = s ) by A4, A24, A27, A29, A30, A34;
supposeA35: abs (r1 - s) = 1 ; ::_thesis: s < i
now__::_thesis:_s_<_i
percases ( ( r1 > s & r1 = s + 1 ) or ( r1 < s & s = r1 + 1 ) ) by A35, Th41;
suppose ( r1 > s & r1 = s + 1 ) ; ::_thesis: s < i
hence  s < i by A33, XXREAL_0:2; ::_thesis: verum
end;
suppose ( r1 < s & s = r1 + 1 ) ; ::_thesis: s < i
then A36: s <= i by A33, NAT_1:13;
now__::_thesis:_(_(_s_<_i_&_s_<_i_)_or_(_s_=_i_&_contradiction_)_)
percases ( s < i or s = i ) by A36, XXREAL_0:1;
case s < i ; ::_thesis: s < i
hence  s < i ; ::_thesis: verum
end;
case s = i ; ::_thesis: contradiction
then  m + j <= m by A9, A26, A27;
then  j <= m - m by XREAL_1:19;
hence  contradiction by A25; ::_thesis: verum
end;
end;
end;
hence  s < i ; ::_thesis: verum
end;
end;
end;
hence  s < i ; ::_thesis: verum
end;
suppose r1 = s ; ::_thesis: s < i
hence  s < i by A23, A28, A32; ::_thesis: verum
end;
end;
end;
hence  s < i ; ::_thesis: verum
end;
end;
end;
hence  s < i ; ::_thesis: verum
end;
reconsider l = (len v) - m as Element of NAT by A18, INT_1:5;
A37: ( 0 < (len v) - m & m + l = len v ) by A17, XREAL_1:19;
A38: S1[ 0 ] ;
 for k being Element of NAT holds S1[k] from NAT_1:sch_1(A38, A22);
hence  contradiction by A3, A11, A12, A37; ::_thesis: verum
end;
case ( i < r & r = i + 1 ) ; ::_thesis: ( m + 1 in dom v & v . (m + 1) = i + 1 )
hence  ( m + 1 in dom v & v . (m + 1) = i + 1 ) by A15; ::_thesis: verum
end;
end;
end;
hence  ( m + 1 in dom v & v . (m + 1) = i + 1 ) ; ::_thesis: verum
end;
case i = r ; ::_thesis: contradiction
then  m + 1 <= m by A9, A15;
then  1 <= m - m by XREAL_1:19;
then  1 <= 0 ;
hence  contradiction ; ::_thesis: verum
end;
end;
end;
hence  ( m + 1 in dom v & v . (m + 1) = i + 1 ) ; ::_thesis: verum
end;

theorem :: SEQM_3:46
for v being FinSequence of REAL
for n being Element of NAT st v <> {} & rng v c= Seg n & v . 1 = 1 & v . (len v) = n & ( for k being Element of NAT st 1 <= k & k <= (len v) - 1 holds
for r, s being Real st r = v . k & s = v . (k + 1) & not abs (r - s) = 1 holds
r = s ) holds
( ( for i being Element of NAT st i in Seg n holds
ex k being Element of NAT st
( k in dom v & v . k = i ) ) & ( for m, k, i being Element of NAT
for r being Real st m in dom v & v . m = i & ( for j being Element of 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
let v be FinSequence of REAL ; ::_thesis: for n being Element of NAT st v <> {} & rng v c= Seg n & v . 1 = 1 & v . (len v) = n & ( for k being Element of NAT st 1 <= k & k <= (len v) - 1 holds
for r, s being Real st r = v . k & s = v . (k + 1) & not abs (r - s) = 1 holds
r = s ) holds
( ( for i being Element of NAT st i in Seg n holds
ex k being Element of NAT st
( k in dom v & v . k = i ) ) & ( for m, k, i being Element of NAT
for r being Real st m in dom v & v . m = i & ( for j being Element of NAT st j in dom v & v . j = i holds
j <= m ) & m < k & k in dom v & r = v . k holds
i < r ) )
let n be Element of NAT ; ::_thesis: ( v <> {} & rng v c= Seg n & v . 1 = 1 & v . (len v) = n & ( for k being Element of NAT st 1 <= k & k <= (len v) - 1 holds
for r, s being Real st r = v . k & s = v . (k + 1) & not abs (r - s) = 1 holds
r = s ) implies ( ( for i being Element of NAT st i in Seg n holds
ex k being Element of NAT st
( k in dom v & v . k = i ) ) & ( for m, k, i being Element of NAT
for r being Real st m in dom v & v . m = i & ( for j being Element of NAT st j in dom v & v . j = i holds
j <= m ) & m < k & k in dom v & r = v . k holds
i < r ) ) )
assume that
A1: v <> {} and
A2: rng v c= Seg n and
A3: v . 1 = 1 and
A4: v . (len v) = n and
A5: for k being Element of NAT st 1 <= k & k <= (len v) - 1 holds
for r, s being Real st r = v . k & s = v . (k + 1) & not abs (r - s) = 1 holds
r = s ; ::_thesis: ( ( for i being Element of NAT st i in Seg n holds
ex k being Element of NAT st
( k in dom v & v . k = i ) ) & ( for m, k, i being Element of NAT
for r being Real st m in dom v & v . m = i & ( for j being Element of NAT st j in dom v & v . j = i holds
j <= m ) & m < k & k in dom v & r = v . k holds
i < r ) )
defpred S1[ Element of NAT ] means ( $1 in Seg n implies ex k being Element of NAT st
( k in dom v & v . k = $1 ) );
A6: 0 + 1 <= len v by A1, NAT_1:13;
then A7: len v in dom v by FINSEQ_3:25;
A8: for i being Element of NAT st S1[i] holds
S1[i + 1]
proof
let i be Element of NAT ; ::_thesis: ( S1[i] implies S1[i + 1] )
assume A9: ( i in Seg n implies ex k being Element of NAT st
( k in dom v & v . k = i ) ) ; ::_thesis: S1[i + 1]
assume A10: i + 1 in Seg n ; ::_thesis: ex k being Element of NAT st
( k in dom v & v . k = i + 1 )
now__::_thesis:_ex_k_being_Element_of_NAT_st_
(_k_in_dom_v_&_v_._k_=_i_+_1_)
percases ( i = 0 or i <> 0 ) ;
supposeA11: i = 0 ; ::_thesis: ex k being Element of NAT st
( k in dom v & v . k = i + 1 )
take k = 1; ::_thesis: ( k in dom v & v . k = i + 1 )
thus  ( k in dom v & v . k = i + 1 ) by A3, A6, A11, FINSEQ_3:25; ::_thesis: verum
end;
supposeA12: i <> 0 ; ::_thesis: ex k being Element of NAT st
( k in dom v & v . k = i + 1 )
defpred S2[ set ] means ( $1 in dom v & v . $1 = i );
A13: for k being Nat st S2[k] holds
k <= len v by FINSEQ_3:25;
 i + 1 <= n by A10, FINSEQ_1:1;
then A14: i <= n by NAT_1:13;
A15: 0 + 1 <= i by A12, NAT_1:13;
then A16: ex k being Nat st S2[k] by A9, A14, FINSEQ_1:1;
consider m being Nat such that
A17: ( S2[m] & ( for k being Nat st S2[k] holds
k <= m ) ) from NAT_1:sch_6(A13, A16);
A18: for k being Element of NAT st S2[k] holds
k <= m by A17;
reconsider m = m as Element of NAT by ORDINAL1:def_12;
take k = m + 1; ::_thesis: ( k in dom v & v . k = i + 1 )
 i in Seg n by A15, A14, FINSEQ_1:1;
hence  ( k in dom v & v . k = i + 1 ) by A1, A2, A4, A5, A10, A17, A18, Th45; ::_thesis: verum
end;
end;
end;
hence  ex k being Element of NAT st
( k in dom v & v . k = i + 1 ) ; ::_thesis: verum
end;
A19: S1[ 0 ] by FINSEQ_1:1;
thus  for i being Element of NAT holds S1[i] from NAT_1:sch_1(A19, A8); ::_thesis: for m, k, i being Element of NAT
for r being Real st m in dom v & v . m = i & ( for j being Element of NAT st j in dom v & v . j = i holds
j <= m ) & m < k & k in dom v & r = v . k holds
i < r
let m, k, i be Element of NAT ; ::_thesis: for r being Real st m in dom v & v . m = i & ( for j being Element of NAT st j in dom v & v . j = i holds
j <= m ) & m < k & k in dom v & r = v . k holds
i < r
let r be Real; ::_thesis: ( m in dom v & v . m = i & ( for j being Element of NAT st j in dom v & v . j = i holds
j <= m ) & m < k & k in dom v & r = v . k implies i < r )
assume that
A20: m in dom v and
A21: v . m = i and
A22: for j being Element of NAT st j in dom v & v . j = i holds
j <= m and
A23: m < k and
A24: k in dom v and
A25: r = v . k ; ::_thesis: i < r
A26: ( m <= len v & k <= len v ) by A20, A24, FINSEQ_3:25;
A27: 1 <= m by A20, FINSEQ_3:25;
A28: i in rng v by A20, A21, FUNCT_1:def_3;
then A29: i <= n by A2, FINSEQ_1:1;
now__::_thesis:_i_<_r
percases ( i = n or i <> n ) ;
suppose i = n ; ::_thesis: i < r
then  len v <= m by A4, A7, A22;
hence  i < r by A23, A26, XXREAL_0:1; ::_thesis: verum
end;
supposeA30: i <> n ; ::_thesis: i < r
defpred S2[ set ] means  for j being Element of NAT
for s being Real st j = $1 & j > 0 & m + j in dom v & s = v . (m + j) holds
i < s;
 i < n by A29, A30, XXREAL_0:1;
then  ( 1 <= i + 1 & i + 1 <= n ) by NAT_1:11, NAT_1:13;
then  i + 1 in Seg n by FINSEQ_1:1;
then A31: v . (m + 1) = i + 1 by A1, A2, A4, A5, A20, A21, A22, A28, Th45;
A32: for k being Element of NAT st S2[k] holds
S2[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S2[k] implies S2[k + 1] )
assume A33: S2[k] ; ::_thesis: S2[k + 1]
let j be Element of NAT ; ::_thesis: for s being Real st j = k + 1 & j > 0 & m + j in dom v & s = v . (m + j) holds
i < s
let s be Real; ::_thesis: ( j = k + 1 & j > 0 & m + j in dom v & s = v . (m + j) implies i < s )
assume that
A34: j = k + 1 and
A35: j > 0 and
A36: m + j in dom v and
A37: s = v . (m + j) ; ::_thesis: i < s
percases ( k = 0 or k <> 0 ) ;
suppose k = 0 ; ::_thesis: i < s
hence  i < s by A31, A34, A37, NAT_1:13; ::_thesis: verum
end;
supposeA38: k <> 0 ; ::_thesis: i < s
 m <= m + k by NAT_1:11;
then A39: 1 <= m + k by A27, XXREAL_0:2;
 s in rng v by A36, A37, FUNCT_1:def_3;
then  s in Seg n by A2;
then reconsider s1 = s as Element of NAT ;
A40: m + (k + 1) <= len v by A34, A36, FINSEQ_3:25;
 m + k <= (m + k) + 1 by NAT_1:11;
then  m + k <= len v by A40, XXREAL_0:2;
then A41: m + k in dom v by A39, FINSEQ_3:25;
then  v . (m + k) in rng v by FUNCT_1:def_3;
then  v . (m + k) in Seg n by A2;
then reconsider r1 = v . (m + k) as Element of NAT ;
A42: i < r1 by A33, A38, A41;
A43: (m + k) + 1 = m + (k + 1) ;
then A44: m + k <= (len v) - 1 by A40, XREAL_1:19;
now__::_thesis:_i_<_s
percases ( abs (r1 - s) = 1 or r1 = s ) by A5, A34, A37, A43, A39, A44;
supposeA45: abs (r1 - s) = 1 ; ::_thesis: i < s
now__::_thesis:_i_<_s
percases ( ( r1 > s & r1 = s + 1 ) or ( r1 < s & s = r1 + 1 ) ) by A45, Th41;
suppose ( r1 > s & r1 = s + 1 ) ; ::_thesis: i < s
then A46: i <= s1 by A42, NAT_1:13;
now__::_thesis:_(_(_i_<_s_&_i_<_s_)_or_(_s_=_i_&_contradiction_)_)
percases ( i < s or s = i ) by A46, XXREAL_0:1;
case i < s ; ::_thesis: i < s
hence  i < s ; ::_thesis: verum
end;
case s = i ; ::_thesis: contradiction
then  m + j <= m by A22, A36, A37;
then  j <= m - m by XREAL_1:19;
hence  contradiction by A35; ::_thesis: verum
end;
end;
end;
hence  i < s ; ::_thesis: verum
end;
suppose ( r1 < s & s = r1 + 1 ) ; ::_thesis: i < s
hence  i < s by A42, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
hence  i < s ; ::_thesis: verum
end;
suppose r1 = s ; ::_thesis: i < s
hence  i < s by A33, A38, A41; ::_thesis: verum
end;
end;
end;
hence  i < s ; ::_thesis: verum
end;
end;
end;
reconsider l = k - m as Element of NAT by A23, INT_1:5;
A47: ( 0 < k - m & m + l = k ) by A23, XREAL_1:50;
A48: S2[ 0 ] ;
 for k being Element of NAT holds S2[k] from NAT_1:sch_1(A48, A32);
hence  i < r by A24, A25, A47; ::_thesis: verum
end;
end;
end;
hence  i < r ; ::_thesis: verum
end;