:: Convergent Real Sequences. Upper and Lower Bound of Sets of Real Numbers
:: by Jaros{\l}aw Kotowicz
::
:: Received November 23, 1989
:: Copyright (c) 1990-2012 Association of Mizar Users


begin

theorem Th1: :: SEQ_4:1
for X, Y being Subset of REAL st ( for r, p being real number st r in X & p in Y holds
r < p ) holds
ex g being real number st
for r, p being real number st r in X &amp; p in Y holds
( r <= g &amp; g <= p )
proofend;

theorem Th2: :: SEQ_4:2
for p being real number
for X being Subset of REAL st 0 < p &amp; ex r being real number st r in X &amp; ( for r being real number st r in X holds
r + p in X ) holds
for g being real number ex r being real number st
( r in X &amp; g < r )
proofend;

theorem Th3: :: SEQ_4:3
for r being real number ex n being Element of NAT st r < n
proofend;

theorem :: SEQ_4:4
for X being Subset of REAL holds
( X is real-bounded iff ex s being real number st
( 0 < s &amp; ( for r being real number st r in X holds
abs r < s ) ) )
proofend;

definition
let r be real number ;
:: original:{
redefine func{r} ->  Subset of REAL;
coherence
 {r} is Subset of REAL
proofend;
end;

theorem Th5: :: SEQ_4:5
for X being real-membered set st not X is empty &amp; X is bounded_above holds
ex g being real number st
( ( for r being real number st r in X holds
r <= g ) &amp; ( for s being real number st 0 < s holds
ex r being real number st
( r in X &amp; g - s < r ) ) )
proofend;

theorem Th6: :: SEQ_4:6
for g1, g2 being real number
for X being real-membered set st ( for r being real number st r in X holds
r <= g1 ) &amp; ( for s being real number st 0 < s holds
ex r being real number st
( r in X &amp; g1 - s < r ) ) &amp; ( for r being real number st r in X holds
r <= g2 ) &amp; ( for s being real number st 0 < s holds
ex r being real number st
( r in X &amp; g2 - s < r ) ) holds
g1 = g2
proofend;

theorem Th7: :: SEQ_4:7
for X being real-membered set st not X is empty &amp; X is bounded_below holds
ex g being real number st
( ( for r being real number st r in X holds
g <= r ) &amp; ( for s being real number st 0 < s holds
ex r being real number st
( r in X &amp; r < g + s ) ) )
proofend;

theorem Th8: :: SEQ_4:8
for g1, g2 being real number
for X being real-membered set st ( for r being real number st r in X holds
g1 <= r ) &amp; ( for s being real number st 0 < s holds
ex r being real number st
( r in X &amp; r < g1 + s ) ) &amp; ( for r being real number st r in X holds
g2 <= r ) &amp; ( for s being real number st 0 < s holds
ex r being real number st
( r in X &amp; r < g2 + s ) ) holds
g1 = g2
proofend;

definition
let X be real-membered set ;
assume A1: ( not X is empty &amp; X is bounded_above ) ;
func upper_bound X ->  real number  means :Def1: :: SEQ_4:def 1
( ( for r being real number st r in X holds
r <= it ) &amp; ( for s being real number st 0 < s holds
ex r being real number st
( r in X &amp; it - s < r ) ) );
existence
 ex b1 being real number st
( ( for r being real number st r in X holds
r <= b1 ) &amp; ( for s being real number st 0 < s holds
ex r being real number st
( r in X &amp; b1 - s < r ) ) ) by A1, Th5;
uniqueness
 for b1, b2 being real number st ( for r being real number st r in X holds
r <= b1 ) &amp; ( for s being real number st 0 < s holds
ex r being real number st
( r in X &amp; b1 - s < r ) ) &amp; ( for r being real number st r in X holds
r <= b2 ) &amp; ( for s being real number st 0 < s holds
ex r being real number st
( r in X &amp; b2 - s < r ) ) holds
b1 = b2 by Th6;
end;

:: deftheorem Def1 defines upper_bound SEQ_4:def_1_:_
 for X being real-membered set st not X is empty &amp; X is bounded_above holds
for b2 being real number holds
( b2 = upper_bound X iff ( ( for r being real number st r in X holds
r <= b2 ) &amp; ( for s being real number st 0 < s holds
ex r being real number st
( r in X &amp; b2 - s < r ) ) ) );

definition
let X be real-membered set ;
assume A1: ( not X is empty &amp; X is bounded_below ) ;
func lower_bound X ->  real number  means :Def2: :: SEQ_4:def 2
( ( for r being real number st r in X holds
it <= r ) &amp; ( for s being real number st 0 < s holds
ex r being real number st
( r in X &amp; r < it + s ) ) );
existence
 ex b1 being real number st
( ( for r being real number st r in X holds
b1 <= r ) &amp; ( for s being real number st 0 < s holds
ex r being real number st
( r in X &amp; r < b1 + s ) ) ) by A1, Th7;
uniqueness
 for b1, b2 being real number st ( for r being real number st r in X holds
b1 <= r ) &amp; ( for s being real number st 0 < s holds
ex r being real number st
( r in X &amp; r < b1 + s ) ) &amp; ( for r being real number st r in X holds
b2 <= r ) &amp; ( for s being real number st 0 < s holds
ex r being real number st
( r in X &amp; r < b2 + s ) ) holds
b1 = b2 by Th8;
end;

:: deftheorem Def2 defines lower_bound SEQ_4:def_2_:_
 for X being real-membered set st not X is empty &amp; X is bounded_below holds
for b2 being real number holds
( b2 = lower_bound X iff ( ( for r being real number st r in X holds
b2 <= r ) &amp; ( for s being real number st 0 < s holds
ex r being real number st
( r in X &amp; r < b2 + s ) ) ) );

Lm1:  for r being real number
for X being non empty real-membered set st ( for s being real number st s in X holds
s >= r ) &amp; ( for t being real number st ( for s being real number st s in X holds
s >= t ) holds
r >= t ) holds
r = lower_bound X
proofend;

Lm2:  for X being non empty real-membered set
for r being real number st ( for s being real number st s in X holds
s <= r ) &amp; ( for t being real number st ( for s being real number st s in X holds
s <= t ) holds
r <= t ) holds
r = upper_bound X
proofend;

registration
let X be non empty real-membered bounded_below set ;
identify lower_bound X with  inf X;
compatibility
 lower_bound X = inf X
proofend;
end;

registration
let X be non empty real-membered bounded_above set ;
identify upper_bound X with  sup X;
compatibility
 upper_bound X = sup X
proofend;
end;

definition
let X be Subset of REAL;
:: original:upper_bound
redefine func upper_bound X ->  Real;
coherence
 upper_bound X is Real by XREAL_0:def_1;
:: original:lower_bound
redefine func lower_bound X ->  Real;
coherence
 lower_bound X is Real by XREAL_0:def_1;
end;

theorem Th9: :: SEQ_4:9
for r being real number holds
( lower_bound {r} = r &amp; upper_bound {r} = r ) by XXREAL_2:11, XXREAL_2:13;

theorem Th10: :: SEQ_4:10
for r being real number holds lower_bound {r} = upper_bound {r}
proofend;

theorem :: SEQ_4:11
for X being Subset of REAL st X is real-bounded &amp; not X is empty holds
lower_bound X <= upper_bound X
proofend;

theorem :: SEQ_4:12
for X being Subset of REAL st X is real-bounded &amp; not X is empty holds
( ex r, p being real number st
( r in X &amp; p in X &amp; p <> r ) iff lower_bound X < upper_bound X )
proofend;

::
:: Theorems about the Convergence and the Limit
::
theorem Th13: :: SEQ_4:13
for seq being Real_Sequence st seq is convergent holds
abs seq is convergent
proofend;

registration
let seq be convergent Real_Sequence;
cluster|.seq.| ->  convergent for Real_Sequence;
coherence
 for b1 being Real_Sequence st b1 = abs seq holds
b1 is convergent by Th13;
end;

theorem :: SEQ_4:14
for seq being Real_Sequence st seq is convergent holds
lim (abs seq) = abs (lim seq)
proofend;

theorem :: SEQ_4:15
for seq being Real_Sequence st abs seq is convergent &amp; lim (abs seq) = 0 holds
( seq is convergent &amp; lim seq = 0 )
proofend;

theorem Th16: :: SEQ_4:16
for seq1, seq being Real_Sequence st seq1 is subsequence of seq &amp; seq is convergent holds
seq1 is convergent
proofend;

theorem Th17: :: SEQ_4:17
for seq1, seq being Real_Sequence st seq1 is subsequence of seq &amp; seq is convergent holds
lim seq1 = lim seq
proofend;

theorem Th18: :: SEQ_4:18
for seq, seq1 being Real_Sequence st seq is convergent &amp; ex k being Element of NAT st
for n being Element of NAT st k <= n holds
seq1 . n = seq . n holds
seq1 is convergent
proofend;

theorem :: SEQ_4:19
for seq, seq1 being Real_Sequence st seq is convergent &amp; ex k being Element of NAT st
for n being Element of NAT st k <= n holds
seq1 . n = seq . n holds
lim seq = lim seq1
proofend;

registration
cluster Function-like constant V18( NAT , REAL )  ->  convergent for Element of bool [:NAT,REAL:];
coherence
 for b1 being Real_Sequence st b1 is constant holds
b1 is convergent ;
end;

registration
cluster Relation-like NAT -defined REAL -valued Function-like constant non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued for Element of bool [:NAT,REAL:];
existence
 ex b1 being Real_Sequence st b1 is constant
proofend;
end;

registration
let seq be convergent Real_Sequence;
let k be Element of NAT ;
clusterseq ^\ k ->  convergent for Real_Sequence;
coherence
 for b1 being Real_Sequence st b1 = seq ^\ k holds
b1 is convergent by Th16;
end;

theorem :: SEQ_4:20
for k being Element of NAT
for seq being Real_Sequence st seq is convergent holds
lim (seq ^\ k) = lim seq by Th17;

theorem Th21: :: SEQ_4:21
for k being Element of NAT
for seq being Real_Sequence st seq ^\ k is convergent holds
seq is convergent
proofend;

theorem :: SEQ_4:22
for k being Element of NAT
for seq being Real_Sequence st seq ^\ k is convergent holds
lim seq = lim (seq ^\ k)
proofend;

theorem Th23: :: SEQ_4:23
for seq being Real_Sequence st seq is convergent &amp; lim seq <> 0 holds
ex k being Element of NAT st seq ^\ k is non-zero
proofend;

theorem :: SEQ_4:24
for seq being Real_Sequence st seq is convergent &amp; lim seq <> 0 holds
ex seq1 being Real_Sequence st
( seq1 is subsequence of seq &amp; seq1 is non-zero )
proofend;

theorem Th25: :: SEQ_4:25
for r being real number
for seq being Real_Sequence st seq is constant &amp; ( r in rng seq or ex n being Element of NAT st seq . n = r ) holds
lim seq = r
proofend;

theorem :: SEQ_4:26
for seq being Real_Sequence st seq is constant holds
for n being Element of NAT holds lim seq = seq . n by Th25;

theorem :: SEQ_4:27
for seq being Real_Sequence st seq is convergent &amp; lim seq <> 0 holds
for seq1 being Real_Sequence st seq1 is subsequence of seq &amp; seq1 is non-zero holds
lim (seq1 ") = (lim seq) "
proofend;

theorem Th28: :: SEQ_4:28
for r being real number
for seq being Real_Sequence st 0 <= r &amp; ( for n being Element of NAT holds seq . n = 1 / (n + r) ) holds
seq is convergent
proofend;

theorem Th29: :: SEQ_4:29
for r being real number
for seq being Real_Sequence st 0 <= r &amp; ( for n being Element of NAT holds seq . n = 1 / (n + r) ) holds
lim seq = 0
proofend;

theorem :: SEQ_4:30
for seq being Real_Sequence st ( for n being Element of NAT holds seq . n = 1 / (n + 1) ) holds
( seq is convergent &amp; lim seq = 0 ) by Th28, Th29;

theorem :: SEQ_4:31
for r, g being real number
for seq being Real_Sequence st 0 <= r &amp; ( for n being Element of NAT holds seq . n = g / (n + r) ) holds
( seq is convergent &amp; lim seq = 0 )
proofend;

theorem Th32: :: SEQ_4:32
for r being real number
for seq being Real_Sequence st 0 <= r &amp; ( for n being Element of NAT holds seq . n = 1 / ((n * n) + r) ) holds
seq is convergent
proofend;

theorem Th33: :: SEQ_4:33
for r being real number
for seq being Real_Sequence st 0 <= r &amp; ( for n being Element of NAT holds seq . n = 1 / ((n * n) + r) ) holds
lim seq = 0
proofend;

theorem :: SEQ_4:34
for seq being Real_Sequence st ( for n being Element of NAT holds seq . n = 1 / ((n * n) + 1) ) holds
( seq is convergent &amp; lim seq = 0 ) by Th32, Th33;

theorem :: SEQ_4:35
for r, g being real number
for seq being Real_Sequence st 0 <= r &amp; ( for n being Element of NAT holds seq . n = g / ((n * n) + r) ) holds
( seq is convergent &amp; lim seq = 0 )
proofend;

registration
cluster Function-like V18( NAT , REAL ) V41() bounded_above  ->  convergent for Element of bool [:NAT,REAL:];
coherence
 for b1 being Real_Sequence st b1 is V41() &amp; b1 is bounded_above holds
b1 is convergent
proofend;
end;

registration
cluster Function-like V18( NAT , REAL ) V42() bounded_below  ->  convergent for Element of bool [:NAT,REAL:];
coherence
 for b1 being Real_Sequence st b1 is V42() &amp; b1 is bounded_below holds
b1 is convergent
proofend;
end;

registration
cluster Function-like V18( NAT , REAL ) monotone bounded  ->  convergent for Element of bool [:NAT,REAL:];
coherence
 for b1 being Real_Sequence st b1 is monotone &amp; b1 is bounded holds
b1 is convergent
proofend;
end;

theorem Th36: :: SEQ_4:36
for seq being Real_Sequence st seq is monotone &amp; seq is bounded holds
seq is convergent ;

theorem :: SEQ_4:37
for seq being Real_Sequence st seq is bounded_above &amp; seq is V41() holds
for n being Element of NAT holds seq . n <= lim seq
proofend;

theorem :: SEQ_4:38
for seq being Real_Sequence st seq is bounded_below &amp; seq is V42() holds
for n being Element of NAT holds lim seq <= seq . n
proofend;

theorem Th39: :: SEQ_4:39
for seq being Real_Sequence ex Nseq being V39() sequence of NAT st seq * Nseq is monotone
proofend;

:: [WP: ] Bolzano-Weierstrass_Theorem_(1_dimension)
theorem Th40: :: SEQ_4:40
for seq being Real_Sequence st seq is bounded holds
ex seq1 being Real_Sequence st
( seq1 is subsequence of seq &amp; seq1 is convergent )
proofend;

:: [WP: ] Cauchy_sequence
theorem :: SEQ_4:41
for seq being Real_Sequence holds
( seq is convergent iff for s being real number st 0 < s holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - (seq . n)) < s )
proofend;

theorem :: SEQ_4:42
for seq, seq1 being Real_Sequence st seq is constant &amp; seq1 is convergent holds
( lim (seq + seq1) = (seq . 0) + (lim seq1) &amp; lim (seq - seq1) = (seq . 0) - (lim seq1) &amp; lim (seq1 - seq) = (lim seq1) - (seq . 0) &amp; lim (seq (#) seq1) = (seq . 0) * (lim seq1) )
proofend;

begin

:: from PSCOMP_1
theorem Th43: :: SEQ_4:43
for X being non empty real-membered set
for t being real number st ( for s being real number st s in X holds
s >= t ) holds
lower_bound X >= t
proofend;

theorem Th44: :: SEQ_4:44
for r being real number
for X being non empty real-membered set st ( for s being real number st s in X holds
s >= r ) &amp; ( for t being real number st ( for s being real number st s in X holds
s >= t ) holds
r >= t ) holds
r = lower_bound X by Lm1;

theorem Th45: :: SEQ_4:45
for X being non empty real-membered set
for r, t being real number st ( for s being real number st s in X holds
s <= t ) holds
upper_bound X <= t
proofend;

theorem Th46: :: SEQ_4:46
for X being non empty real-membered set
for r being real number st ( for s being real number st s in X holds
s <= r ) &amp; ( for t being real number st ( for s being real number st s in X holds
s <= t ) holds
r <= t ) holds
r = upper_bound X by Lm2;

theorem :: SEQ_4:47
for X being non empty real-membered set
for Y being real-membered set st X c= Y &amp; Y is bounded_below holds
lower_bound Y <= lower_bound X
proofend;

theorem :: SEQ_4:48
for X being non empty real-membered set
for Y being real-membered set st X c= Y &amp; Y is bounded_above holds
upper_bound X <= upper_bound Y
proofend;

:: from CQC_SIM1, 2007.03.15, A.T.
definition
let A be non empty natural-membered set ;
:: original:inf
redefine func min A ->  Element of NAT ;
coherence
 inf A is Element of NAT by ORDINAL1:def_12;
end;

begin

theorem :: SEQ_4:49
0c is_a_unity_wrt addcomplex by BINOP_2:1, SETWISEO:14;

theorem Th50: :: SEQ_4:50
compcomplex is_an_inverseOp_wrt addcomplex
proofend;

theorem Th51: :: SEQ_4:51
addcomplex is having_an_inverseOp by Th50, FINSEQOP:def_2;

theorem Th52: :: SEQ_4:52
the_inverseOp_wrt addcomplex = compcomplex by Th50, Th51, FINSEQOP:def_3;

definition
redefine func diffcomplex  equals :: SEQ_4:def 3
addcomplex * ((id COMPLEX),compcomplex);
compatibility
 for b1 being Element of bool [:[:COMPLEX,COMPLEX:],COMPLEX:] holds
( b1 = diffcomplex iff b1 = addcomplex * ((id COMPLEX),compcomplex) )
proofend;
end;

:: deftheorem  defines diffcomplex SEQ_4:def_3_:_
 diffcomplex = addcomplex * ((id COMPLEX),compcomplex);

theorem :: SEQ_4:53
1r is_a_unity_wrt multcomplex by BINOP_2:6, SETWISEO:14;

theorem Th54: :: SEQ_4:54
multcomplex is_distributive_wrt addcomplex
proofend;

definition
let c be complex number ;
funcc multcomplex  ->  UnOp of COMPLEX equals :: SEQ_4:def 4
multcomplex [;] (c,(id COMPLEX));
coherence
 multcomplex [;] (c,(id COMPLEX)) is UnOp of COMPLEX
proofend;
end;

:: deftheorem  defines multcomplex SEQ_4:def_4_:_
 for c being complex number holds c multcomplex = multcomplex [;] (c,(id COMPLEX));

Lm3:  for c, c9 being Element of COMPLEX holds (multcomplex [;] (c,(id COMPLEX))) . c9 = c * c9
proofend;

theorem :: SEQ_4:55
for c, c9 being Element of COMPLEX holds (c multcomplex) . c9 = c * c9 by Lm3;

theorem :: SEQ_4:56
for c being Element of COMPLEX holds c multcomplex is_distributive_wrt addcomplex by Th54, FINSEQOP:54;

definition
func abscomplex  ->  Function of COMPLEX,REAL means :Def5: :: SEQ_4:def 5
 for c being Element of COMPLEX holds it . c = |.c.|;
existence
 ex b1 being Function of COMPLEX,REAL st
for c being Element of COMPLEX holds b1 . c = |.c.| from FUNCT_2:sch_4();
uniqueness
 for b1, b2 being Function of COMPLEX,REAL st ( for c being Element of COMPLEX holds b1 . c = |.c.| ) &amp; ( for c being Element of COMPLEX holds b2 . c = |.c.| ) holds
b1 = b2 from BINOP_2:sch_1();
end;

:: deftheorem Def5 defines abscomplex SEQ_4:def_5_:_
 for b1 being Function of COMPLEX,REAL holds
( b1 = abscomplex iff for c being Element of COMPLEX holds b1 . c = |.c.| );

definition
let z1, z2 be FinSequence of COMPLEX ;
:: original:+
redefine funcz1 + z2 ->  FinSequence of COMPLEX  equals :: SEQ_4:def 6
addcomplex .: (z1,z2);
coherence
 z1 + z2 is FinSequence of COMPLEX
proofend;
compatibility
 for b1 being FinSequence of COMPLEX holds
( b1 = z1 + z2 iff b1 = addcomplex .: (z1,z2) )
proofend;
:: original:-
redefine funcz1 - z2 ->  FinSequence of COMPLEX  equals :: SEQ_4:def 7
diffcomplex .: (z1,z2);
coherence
 z1 - z2 is FinSequence of COMPLEX
proofend;
compatibility
 for b1 being FinSequence of COMPLEX holds
( b1 = z1 - z2 iff b1 = diffcomplex .: (z1,z2) )
proofend;
end;

:: deftheorem  defines + SEQ_4:def_6_:_
 for z1, z2 being FinSequence of COMPLEX holds z1 + z2 = addcomplex .: (z1,z2);

:: deftheorem  defines - SEQ_4:def_7_:_
 for z1, z2 being FinSequence of COMPLEX holds z1 - z2 = diffcomplex .: (z1,z2);

definition
let z be FinSequence of COMPLEX ;
:: original:-
redefine func - z ->  FinSequence of COMPLEX  equals :: SEQ_4:def 8
compcomplex * z;
coherence
 - z is FinSequence of COMPLEX
proofend;
compatibility
 for b1 being FinSequence of COMPLEX holds
( b1 = - z iff b1 = compcomplex * z )
proofend;
end;

:: deftheorem  defines - SEQ_4:def_8_:_
 for z being FinSequence of COMPLEX holds - z = compcomplex * z;

notation
let z be FinSequence of COMPLEX ;
let c be complex number ;
synonym c * z for c (#) z;
end;

definition
let z be FinSequence of COMPLEX ;
let c be complex number ;
:: original:*
redefine funcc * z ->  FinSequence of COMPLEX  equals :: SEQ_4:def 9
(c multcomplex) * z;
coherence
 c * z is FinSequence of COMPLEX
proofend;
compatibility
 for b1 being FinSequence of COMPLEX holds
( b1 = c * z iff b1 = (c multcomplex) * z )
proofend;
end;

:: deftheorem  defines * SEQ_4:def_9_:_
 for z being FinSequence of COMPLEX
for c being complex number holds c * z = (c multcomplex) * z;

definition
let z be FinSequence of COMPLEX ;
:: original:|.
redefine func abs z ->  FinSequence of REAL  equals :: SEQ_4:def 10
abscomplex * z;
coherence
 |.z.| is FinSequence of REAL
proofend;
compatibility
 for b1 being FinSequence of REAL holds
( b1 = |.z.| iff b1 = abscomplex * z )
proofend;
end;

:: deftheorem  defines abs SEQ_4:def_10_:_
 for z being FinSequence of COMPLEX holds abs z = abscomplex * z;

definition
let n be Element of NAT ;
func COMPLEX n ->  FinSequenceSet of COMPLEX  equals :: SEQ_4:def 11
n -tuples_on COMPLEX;
correctness
coherence
n -tuples_on COMPLEX is FinSequenceSet of COMPLEX ;
;
end;

:: deftheorem  defines COMPLEX SEQ_4:def_11_:_
 for n being Element of NAT holds COMPLEX n = n -tuples_on COMPLEX;

registration
let n be Element of NAT ;
cluster COMPLEX n ->  non empty ;
coherence
 not COMPLEX n is empty ;
end;

Lm4:  for n being Element of NAT
for z being Element of COMPLEX n holds dom z = Seg n
proofend;

theorem Th57: :: SEQ_4:57
for k, n being Element of NAT
for z being Element of COMPLEX n st k in Seg n holds
z . k in COMPLEX
proofend;

definition
let n be Element of NAT ;
let z1, z2 be Element of COMPLEX n;
:: original:+
redefine funcz1 + z2 ->  Element of COMPLEX n;
coherence
 z1 + z2 is Element of COMPLEX n by FINSEQ_2:120;
end;

theorem Th58: :: SEQ_4:58
for k, n being Element of NAT
for c1, c2 being Element of COMPLEX
for z1, z2 being Element of COMPLEX n st k in Seg n &amp; c1 = z1 . k &amp; c2 = z2 . k holds
(z1 + z2) . k = c1 + c2
proofend;

definition
let n be Element of NAT ;
func 0c n ->  FinSequence of COMPLEX  equals :: SEQ_4:def 12
n |-> 0c;
correctness
coherence
n |-> 0c is FinSequence of COMPLEX ;
;
end;

:: deftheorem  defines 0c SEQ_4:def_12_:_
 for n being Element of NAT holds 0c n = n |-> 0c;

definition
let n be Element of NAT ;
:: original:0c
redefine func 0c n ->  Element of COMPLEX n;
coherence
 0c n is Element of COMPLEX n ;
end;

theorem :: SEQ_4:59
for n being Element of NAT
for z being Element of COMPLEX n holds
( z + (0c n) = z &amp; z = (0c n) + z ) by BINOP_2:1, FINSEQOP:56;

definition
let n be Element of NAT ;
let z be Element of COMPLEX n;
:: original:-
redefine func - z ->  Element of COMPLEX n;
coherence
 - z is Element of COMPLEX n by FINSEQ_2:113;
end;

theorem Th60: :: SEQ_4:60
for k, n being Element of NAT
for c being Element of COMPLEX
for z being Element of COMPLEX n st k in Seg n &amp; c = z . k holds
(- z) . k = - c
proofend;

Lm5:  for n being Element of NAT holds - (0c n) = 0c n
proofend;

theorem :: SEQ_4:61
for n being Element of NAT
for z being Element of COMPLEX n holds
( z + (- z) = 0c n &amp; (- z) + z = 0c n ) by Th51, Th52, BINOP_2:1, FINSEQOP:73;

theorem :: SEQ_4:62
for n being Element of NAT
for z1, z2 being Element of COMPLEX n st z1 + z2 = 0c n holds
( z1 = - z2 &amp; z2 = - z1 ) by Th51, Th52, BINOP_2:1, FINSEQOP:74;

theorem :: SEQ_4:63
canceled;

theorem :: SEQ_4:64
for n being Element of NAT
for z1, z2 being Element of COMPLEX n st - z1 = - z2 holds
z1 = z2
proofend;

Lm6:  for n being Element of NAT
for z1, z, z2 being Element of COMPLEX n st z1 + z = z2 + z holds
z1 = z2
proofend;

theorem :: SEQ_4:65
for n being Element of NAT
for z1, z, z2 being Element of COMPLEX n st ( z1 + z = z2 + z or z1 + z = z + z2 ) holds
z1 = z2 by Lm6;

theorem Th66: :: SEQ_4:66
for n being Element of NAT
for z1, z2 being Element of COMPLEX n holds - (z1 + z2) = (- z1) + (- z2)
proofend;

definition
let n be Element of NAT ;
let z1, z2 be Element of COMPLEX n;
:: original:-
redefine funcz1 - z2 ->  Element of COMPLEX n;
coherence
 z1 - z2 is Element of COMPLEX n by FINSEQ_2:120;
end;

theorem :: SEQ_4:67
for k, n being Element of NAT
for z1, z2 being Element of COMPLEX n st k in Seg n holds
(z1 - z2) . k = (z1 . k) - (z2 . k)
proofend;

theorem :: SEQ_4:68
for n being Element of NAT
for z being Element of COMPLEX n holds z - (0c n) = z
proofend;

theorem :: SEQ_4:69
for n being Element of NAT
for z being Element of COMPLEX n holds (0c n) - z = - z
proofend;

theorem :: SEQ_4:70
for n being Element of NAT
for z1, z2 being Element of COMPLEX n holds z1 - (- z2) = z1 + z2 ;

theorem Th71: :: SEQ_4:71
for n being Element of NAT
for z1, z2 being Element of COMPLEX n holds - (z1 - z2) = z2 - z1
proofend;

theorem Th72: :: SEQ_4:72
for n being Element of NAT
for z1, z2 being Element of COMPLEX n holds - (z1 - z2) = (- z1) + z2
proofend;

theorem Th73: :: SEQ_4:73
for n being Element of NAT
for z being Element of COMPLEX n holds z - z = 0c n
proofend;

theorem Th74: :: SEQ_4:74
for n being Element of NAT
for z1, z2 being Element of COMPLEX n st z1 - z2 = 0c n holds
z1 = z2
proofend;

theorem Th75: :: SEQ_4:75
for n being Element of NAT
for z1, z2, z3 being Element of COMPLEX n holds (z1 - z2) - z3 = z1 - (z2 + z3)
proofend;

theorem Th76: :: SEQ_4:76
for n being Element of NAT
for z1, z2, z3 being Element of COMPLEX n holds z1 + (z2 - z3) = (z1 + z2) - z3
proofend;

theorem :: SEQ_4:77
for n being Element of NAT
for z1, z2, z3 being Element of COMPLEX n holds z1 - (z2 - z3) = (z1 - z2) + z3
proofend;

theorem :: SEQ_4:78
for n being Element of NAT
for z1, z2, z3 being Element of COMPLEX n holds (z1 - z2) + z3 = (z1 + z3) - z2 by Th76;

theorem Th79: :: SEQ_4:79
for n being Element of NAT
for z1, z being Element of COMPLEX n holds z1 = (z1 + z) - z
proofend;

theorem Th80: :: SEQ_4:80
for n being Element of NAT
for z1, z2 being Element of COMPLEX n holds z1 + (z2 - z1) = z2
proofend;

theorem Th81: :: SEQ_4:81
for n being Element of NAT
for z1, z being Element of COMPLEX n holds z1 = (z1 - z) + z
proofend;

definition
let n be Element of NAT ;
let z be Element of COMPLEX n;
let c be Element of COMPLEX ;
:: original:*
redefine funcc * z ->  Element of COMPLEX n;
coherence
 c * z is Element of COMPLEX n by FINSEQ_2:113;
end;

theorem Th82: :: SEQ_4:82
for k, n being Element of NAT
for c9, c being Element of COMPLEX
for z being Element of COMPLEX n st k in Seg n &amp; c9 = z . k holds
(c * z) . k = c * c9
proofend;

theorem :: SEQ_4:83
for n being Element of NAT
for c1, c2 being Element of COMPLEX
for z being Element of COMPLEX n holds c1 * (c2 * z) = (c1 * c2) * z
proofend;

theorem :: SEQ_4:84
for n being Element of NAT
for c1, c2 being Element of COMPLEX
for z being Element of COMPLEX n holds (c1 + c2) * z = (c1 * z) + (c2 * z)
proofend;

theorem :: SEQ_4:85
for n being Element of NAT
for c being Element of COMPLEX
for z1, z2 being Element of COMPLEX n holds c * (z1 + z2) = (c * z1) + (c * z2) by Th54, FINSEQOP:51, FINSEQOP:54;

theorem :: SEQ_4:86
for n being Element of NAT
for z being Element of COMPLEX n holds 1r * z = z
proofend;

theorem :: SEQ_4:87
for n being Element of NAT
for z being Element of COMPLEX n holds 0c * z = 0c n
proofend;

theorem :: SEQ_4:88
for n being Element of NAT
for z being Element of COMPLEX n holds (- 1r) * z = - z ;

definition
let n be Element of NAT ;
let z be Element of COMPLEX n;
:: original:|.
redefine func abs z ->  Element of n -tuples_on REAL;
correctness
coherence
|.z.| is Element of n -tuples_on REAL;
by FINSEQ_2:113;
end;

theorem Th89: :: SEQ_4:89
for k, n being Element of NAT
for c being Element of COMPLEX
for z being Element of COMPLEX n st k in Seg n &amp; c = z . k holds
(abs z) . k = |.c.|
proofend;

theorem Th90: :: SEQ_4:90
for n being Element of NAT holds abs (0c n) = n |-> 0
proofend;

theorem Th91: :: SEQ_4:91
for n being Element of NAT
for z being Element of COMPLEX n holds abs (- z) = abs z
proofend;

theorem Th92: :: SEQ_4:92
for n being Element of NAT
for c being Element of COMPLEX
for z being Element of COMPLEX n holds abs (c * z) = |.c.| * (abs z)
proofend;

definition
let z be FinSequence of COMPLEX ;
func|.z.| ->  Real equals :: SEQ_4:def 13
 sqrt (Sum (sqr (abs z)));
correctness
coherence
sqrt (Sum (sqr (abs z))) is Real;
;
end;

:: deftheorem  defines |. SEQ_4:def_13_:_
 for z being FinSequence of COMPLEX holds |.z.| = sqrt (Sum (sqr (abs z)));

theorem Th93: :: SEQ_4:93
for n being Element of NAT holds |.(0c n).| = 0
proofend;

theorem Th94: :: SEQ_4:94
for n being Element of NAT
for z being Element of COMPLEX n st |.z.| = 0 holds
z = 0c n
proofend;

theorem Th95: :: SEQ_4:95
for n being Element of NAT
for z being Element of COMPLEX n holds 0 <= |.z.|
proofend;

theorem :: SEQ_4:96
for n being Element of NAT
for z being Element of COMPLEX n holds |.(- z).| = |.z.| by Th91;

theorem :: SEQ_4:97
for n being Element of NAT
for c being Element of COMPLEX
for z being Element of COMPLEX n holds |.(c * z).| = |.c.| * |.z.|
proofend;

theorem Th98: :: SEQ_4:98
for n being Element of NAT
for z1, z2 being Element of COMPLEX n holds |.(z1 + z2).| <= |.z1.| + |.z2.|
proofend;

theorem Th99: :: SEQ_4:99
for n being Element of NAT
for z1, z2 being Element of COMPLEX n holds |.(z1 - z2).| <= |.z1.| + |.z2.|
proofend;

theorem :: SEQ_4:100
for n being Element of NAT
for z1, z2 being Element of COMPLEX n holds |.z1.| - |.z2.| <= |.(z1 + z2).|
proofend;

theorem :: SEQ_4:101
for n being Element of NAT
for z1, z2 being Element of COMPLEX n holds |.z1.| - |.z2.| <= |.(z1 - z2).|
proofend;

theorem Th102: :: SEQ_4:102
for n being Element of NAT
for z1, z2 being Element of COMPLEX n holds
( |.(z1 - z2).| = 0 iff z1 = z2 )
proofend;

theorem :: SEQ_4:103
for n being Element of NAT
for z1, z2 being Element of COMPLEX n st z1 <> z2 holds
0 < |.(z1 - z2).|
proofend;

theorem Th104: :: SEQ_4:104
for n being Element of NAT
for z1, z2 being Element of COMPLEX n holds |.(z1 - z2).| = |.(z2 - z1).|
proofend;

theorem Th105: :: SEQ_4:105
for n being Element of NAT
for z1, z2, z being Element of COMPLEX n holds |.(z1 - z2).| <= |.(z1 - z).| + |.(z - z2).|
proofend;

definition
let n be Element of NAT ;
let A be Subset of (COMPLEX n);
attrA is open  means :Def14: :: SEQ_4:def 14
 for x being Element of COMPLEX n st x in A holds
ex r being Real st
( 0 < r &amp; ( for z being Element of COMPLEX n st |.z.| < r holds
x + z in A ) );
end;

:: deftheorem Def14 defines open SEQ_4:def_14_:_
 for n being Element of NAT
for A being Subset of (COMPLEX n) holds
( A is open iff for x being Element of COMPLEX n st x in A holds
ex r being Real st
( 0 < r &amp; ( for z being Element of COMPLEX n st |.z.| < r holds
x + z in A ) ) );

definition
let n be Element of NAT ;
let A be Subset of (COMPLEX n);
attrA is closed  means :: SEQ_4:def 15
 for x being Element of COMPLEX n st ( for r being Real st r > 0 holds
ex z being Element of COMPLEX n st
( |.z.| < r &amp; x + z in A ) ) holds
x in A;
end;

:: deftheorem  defines closed SEQ_4:def_15_:_
 for n being Element of NAT
for A being Subset of (COMPLEX n) holds
( A is closed iff for x being Element of COMPLEX n st ( for r being Real st r > 0 holds
ex z being Element of COMPLEX n st
( |.z.| < r &amp; x + z in A ) ) holds
x in A );

theorem :: SEQ_4:106
for n being Element of NAT
for A being Subset of (COMPLEX n) st A = {} holds
A is open
proofend;

theorem :: SEQ_4:107
for n being Element of NAT
for A being Subset of (COMPLEX n) st A = COMPLEX n holds
A is open
proofend;

theorem :: SEQ_4:108
for n being Element of NAT
for AA being Subset-Family of (COMPLEX n) st ( for A being Subset of (COMPLEX n) st A in AA holds
A is open ) holds
for A being Subset of (COMPLEX n) st A = union AA holds
A is open
proofend;

theorem :: SEQ_4:109
for n being Element of NAT
for A, B being Subset of (COMPLEX n) st A is open &amp; B is open holds
for C being Subset of (COMPLEX n) st C = A /\ B holds
C is open
proofend;

definition
let n be Element of NAT ;
let x be Element of COMPLEX n;
let r be Real;
func Ball (x,r) ->  Subset of (COMPLEX n) equals :: SEQ_4:def 16
 {  z where z is Element of COMPLEX n : |.(z - x).| < r  }  ;
coherence
  {  z where z is Element of COMPLEX n : |.(z - x).| < r  }  is Subset of (COMPLEX n)
proofend;
end;

:: deftheorem  defines Ball SEQ_4:def_16_:_
 for n being Element of NAT
for x being Element of COMPLEX n
for r being Real holds Ball (x,r) =  {  z where z is Element of COMPLEX n : |.(z - x).| < r  }  ;

theorem Th110: :: SEQ_4:110
for n being Element of NAT
for r being Real
for z, x being Element of COMPLEX n holds
( z in Ball (x,r) iff |.(x - z).| < r )
proofend;

theorem :: SEQ_4:111
for n being Element of NAT
for r being Real
for x being Element of COMPLEX n st 0 < r holds
x in Ball (x,r)
proofend;

theorem :: SEQ_4:112
for n being Element of NAT
for r1 being Real
for z1 being Element of COMPLEX n holds Ball (z1,r1) is open
proofend;

definition
let n be Element of NAT ;
let x be Element of COMPLEX n;
let A be Subset of (COMPLEX n);
func dist (x,A) ->  Real means :Def17: :: SEQ_4:def 17
 for X being Subset of REAL st X =  {  |.(x - z).| where z is Element of COMPLEX n : z in A  }  holds
it = lower_bound X;
existence
 ex b1 being Real st
for X being Subset of REAL st X =  {  |.(x - z).| where z is Element of COMPLEX n : z in A  }  holds
b1 = lower_bound X
proofend;
uniqueness
 for b1, b2 being Real st ( for X being Subset of REAL st X =  {  |.(x - z).| where z is Element of COMPLEX n : z in A  }  holds
b1 = lower_bound X ) &amp; ( for X being Subset of REAL st X =  {  |.(x - z).| where z is Element of COMPLEX n : z in A  }  holds
b2 = lower_bound X ) holds
b1 = b2
proofend;
end;

:: deftheorem Def17 defines dist SEQ_4:def_17_:_
 for n being Element of NAT
for x being Element of COMPLEX n
for A being Subset of (COMPLEX n)
for b4 being Real holds
( b4 = dist (x,A) iff for X being Subset of REAL st X =  {  |.(x - z).| where z is Element of COMPLEX n : z in A  }  holds
b4 = lower_bound X );

definition
let n be Element of NAT ;
let A be Subset of (COMPLEX n);
let r be Real;
func Ball (A,r) ->  Subset of (COMPLEX n) equals :: SEQ_4:def 18
 {  z where z is Element of COMPLEX n : dist (z,A) < r  }  ;
coherence
  {  z where z is Element of COMPLEX n : dist (z,A) < r  }  is Subset of (COMPLEX n)
proofend;
end;

:: deftheorem  defines Ball SEQ_4:def_18_:_
 for n being Element of NAT
for A being Subset of (COMPLEX n)
for r being Real holds Ball (A,r) =  {  z where z is Element of COMPLEX n : dist (z,A) < r  }  ;

theorem Th113: :: SEQ_4:113
for X being Subset of REAL
for r being Real st X <> {} &amp; ( for r9 being Real st r9 in X holds
r <= r9 ) holds
lower_bound X >= r
proofend;

theorem Th114: :: SEQ_4:114
for n being Element of NAT
for x being Element of COMPLEX n
for A being Subset of (COMPLEX n) st A <> {} holds
dist (x,A) >= 0
proofend;

theorem Th115: :: SEQ_4:115
for n being Element of NAT
for x, z being Element of COMPLEX n
for A being Subset of (COMPLEX n) st A <> {} holds
dist ((x + z),A) <= (dist (x,A)) + |.z.|
proofend;

theorem Th116: :: SEQ_4:116
for n being Element of NAT
for x being Element of COMPLEX n
for A being Subset of (COMPLEX n) st x in A holds
dist (x,A) = 0
proofend;

theorem :: SEQ_4:117
for n being Element of NAT
for x being Element of COMPLEX n
for A being Subset of (COMPLEX n) st not x in A &amp; A <> {} &amp; A is closed holds
dist (x,A) > 0
proofend;

theorem :: SEQ_4:118
for n being Element of NAT
for z1, x being Element of COMPLEX n
for A being Subset of (COMPLEX n) st A <> {} holds
|.(z1 - x).| + (dist (x,A)) >= dist (z1,A)
proofend;

theorem Th119: :: SEQ_4:119
for n being Element of NAT
for r being Real
for z being Element of COMPLEX n
for A being Subset of (COMPLEX n) holds
( z in Ball (A,r) iff dist (z,A) < r )
proofend;

theorem Th120: :: SEQ_4:120
for n being Element of NAT
for r being Real
for x being Element of COMPLEX n
for A being Subset of (COMPLEX n) st 0 < r &amp; x in A holds
x in Ball (A,r)
proofend;

theorem :: SEQ_4:121
for n being Element of NAT
for r being Real
for A being Subset of (COMPLEX n) st 0 < r holds
A c= Ball (A,r)
proofend;

theorem :: SEQ_4:122
for n being Element of NAT
for r1 being Real
for A being Subset of (COMPLEX n) st A <> {} holds
Ball (A,r1) is open
proofend;

definition
let n be Element of NAT ;
let A, B be Subset of (COMPLEX n);
func dist (A,B) ->  Real means :Def19: :: SEQ_4:def 19
 for X being Subset of REAL st X =  {  |.(x - z).| where x, z is Element of COMPLEX n : ( x in A &amp; z in B )  }  holds
it = lower_bound X;
existence
 ex b1 being Real st
for X being Subset of REAL st X =  {  |.(x - z).| where x, z is Element of COMPLEX n : ( x in A &amp; z in B )  }  holds
b1 = lower_bound X
proofend;
uniqueness
 for b1, b2 being Real st ( for X being Subset of REAL st X =  {  |.(x - z).| where x, z is Element of COMPLEX n : ( x in A &amp; z in B )  }  holds
b1 = lower_bound X ) &amp; ( for X being Subset of REAL st X =  {  |.(x - z).| where x, z is Element of COMPLEX n : ( x in A &amp; z in B )  }  holds
b2 = lower_bound X ) holds
b1 = b2
proofend;
end;

:: deftheorem Def19 defines dist SEQ_4:def_19_:_
 for n being Element of NAT
for A, B being Subset of (COMPLEX n)
for b4 being Real holds
( b4 = dist (A,B) iff for X being Subset of REAL st X =  {  |.(x - z).| where x, z is Element of COMPLEX n : ( x in A &amp; z in B )  }  holds
b4 = lower_bound X );

theorem :: SEQ_4:123
for X, Y being Subset of REAL st X <> {} &amp; Y <> {} holds
X ++ Y <> {} ;

theorem Th124: :: SEQ_4:124
for X, Y being Subset of REAL st X is bounded_below &amp; Y is bounded_below holds
X ++ Y is bounded_below
proofend;

theorem Th125: :: SEQ_4:125
for X, Y being Subset of REAL st X <> {} &amp; X is bounded_below &amp; Y <> {} &amp; Y is bounded_below holds
lower_bound (X ++ Y) = (lower_bound X) + (lower_bound Y)
proofend;

theorem Th126: :: SEQ_4:126
for X, Y being Subset of REAL st Y is bounded_below &amp; X <> {} &amp; ( for r being Real st r in X holds
ex r1 being Real st
( r1 in Y &amp; r1 <= r ) ) holds
lower_bound X >= lower_bound Y
proofend;

theorem Th127: :: SEQ_4:127
for n being Element of NAT
for A, B being Subset of (COMPLEX n) st A <> {} &amp; B <> {} holds
dist (A,B) >= 0
proofend;

theorem :: SEQ_4:128
for n being Element of NAT
for A, B being Subset of (COMPLEX n) holds dist (A,B) = dist (B,A)
proofend;

theorem Th129: :: SEQ_4:129
for n being Element of NAT
for x being Element of COMPLEX n
for A, B being Subset of (COMPLEX n) st A <> {} &amp; B <> {} holds
(dist (x,A)) + (dist (x,B)) >= dist (A,B)
proofend;

theorem :: SEQ_4:130
for n being Element of NAT
for A, B being Subset of (COMPLEX n) st A meets B holds
dist (A,B) = 0
proofend;

definition
let n be Element of NAT ;
func ComplexOpenSets n ->  Subset-Family of (COMPLEX n) equals :: SEQ_4:def 20
 {  A where A is Subset of (COMPLEX n) : A is open  }  ;
coherence
  {  A where A is Subset of (COMPLEX n) : A is open  }  is Subset-Family of (COMPLEX n)
proofend;
end;

:: deftheorem  defines ComplexOpenSets SEQ_4:def_20_:_
 for n being Element of NAT holds ComplexOpenSets n =  {  A where A is Subset of (COMPLEX n) : A is open  }  ;

theorem :: SEQ_4:131
for n being Element of NAT
for A being Subset of (COMPLEX n) holds
( A in ComplexOpenSets n iff A is open )
proofend;

theorem :: SEQ_4:132
for n being Element of NAT
for A being Subset of (COMPLEX n) holds
( A is closed iff A ` is open )
proofend;

begin

defpred S1[ Nat] means  for R being finite Subset of REAL st R <> {} &amp; card R = $1 holds
( R is bounded_above &amp; upper_bound R in R &amp; R is bounded_below &amp; lower_bound R in R );

Lm7:  S1[ 0 ]
;

Lm8:  for n being Element of NAT st S1[n] holds
S1[n + 1]
proofend;

Lm9:  for n being Element of NAT holds S1[n]
from NAT_1:sch_1(Lm7, Lm8);

theorem Th133: :: SEQ_4:133
for R being finite Subset of REAL st R <> {} holds
( R is bounded_above &amp; upper_bound R in R &amp; R is bounded_below &amp; lower_bound R in R )
proofend;

theorem :: SEQ_4:134
for n being Nat
for f being FinSequence holds
( 1 <= n &amp; n + 1 <= len f iff ( n in dom f &amp; n + 1 in dom f ) )
proofend;

theorem :: SEQ_4:135
for n being Nat
for f being FinSequence holds
( 1 <= n &amp; n + 2 <= len f iff ( n in dom f &amp; n + 1 in dom f &amp; n + 2 in dom f ) )
proofend;

theorem :: SEQ_4:136
for D being non empty set
for f1, f2 being FinSequence of D
for n being Element of NAT st 1 <= n &amp; n <= len f2 holds
(f1 ^ f2) /. (n + (len f1)) = f2 /. n
proofend;

theorem :: SEQ_4:137
for v being FinSequence of REAL st v is increasing holds
for n, m being Element of NAT st n in dom v &amp; m in dom v &amp; n <= m holds
v . n <= v . m
proofend;

theorem Th138: :: SEQ_4:138
for v being FinSequence of REAL st v is increasing holds
for n, m being Element of NAT st n in dom v &amp; m in dom v &amp; n <> m holds
v . n <> v . m
proofend;

theorem Th139: :: SEQ_4:139
for v, v1 being FinSequence of REAL
for n being Element of NAT st v is increasing &amp; v1 = v | (Seg n) holds
v1 is increasing
proofend;

defpred S2[ Element of NAT ] means  for v being FinSequence of REAL st card (rng v) = $1 holds
ex v1 being FinSequence of REAL st
( rng v1 = rng v &amp; len v1 = card (rng v) &amp; v1 is increasing );

Lm10:  S2[ 0 ]
proofend;

Lm11:  for n being Element of NAT st S2[n] holds
S2[n + 1]
proofend;

Lm12:  for n being Element of NAT holds S2[n]
from NAT_1:sch_1(Lm10, Lm11);

theorem :: SEQ_4:140
for v being FinSequence of REAL ex v1 being FinSequence of REAL st
( rng v1 = rng v &amp; len v1 = card (rng v) &amp; v1 is increasing ) by Lm12;

defpred S3[ Element of NAT ] means  for v1, v2 being FinSequence of REAL st len v1 = $1 &amp; len v2 = $1 &amp; rng v1 = rng v2 &amp; v1 is increasing &amp; v2 is increasing holds
v1 = v2;

Lm13:  S3[ 0 ]
proofend;

Lm14:  for n being Element of NAT st S3[n] holds
S3[n + 1]
proofend;

Lm15:  for n being Element of NAT holds S3[n]
from NAT_1:sch_1(Lm13, Lm14);

theorem :: SEQ_4:141
for v1, v2 being FinSequence of REAL st len v1 = len v2 &amp; rng v1 = rng v2 &amp; v1 is increasing &amp; v2 is increasing holds
v1 = v2 by Lm15;

definition
let v be FinSequence of REAL ;
func Incr v ->  increasing FinSequence of REAL  means :Def21: :: SEQ_4:def 21
( rng it = rng v &amp; len it = card (rng v) );
existence
 ex b1 being increasing FinSequence of REAL st
( rng b1 = rng v &amp; len b1 = card (rng v) )
proofend;
uniqueness
 for b1, b2 being increasing FinSequence of REAL st rng b1 = rng v &amp; len b1 = card (rng v) &amp; rng b2 = rng v &amp; len b2 = card (rng v) holds
b1 = b2 by Lm15;
end;

:: deftheorem Def21 defines Incr SEQ_4:def_21_:_
 for v being FinSequence of REAL
for b2 being increasing FinSequence of REAL holds
( b2 = Incr v iff ( rng b2 = rng v &amp; len b2 = card (rng v) ) );

registration
let v be non empty FinSequence of REAL ;
cluster Incr v ->  non empty increasing ;
coherence
 not Incr v is empty
proofend;
end;

:: from SPRECT_1, 2011.04.24, A.T
registration
cluster non empty complex-membered ext-real-membered real-membered bounded_below bounded_above for Element of bool REAL;
existence
 ex b1 being Subset of REAL st
( not b1 is empty &amp; b1 is bounded_above &amp; b1 is bounded_below )
proofend;
end;

theorem :: SEQ_4:142
for A, B being non empty bounded_below Subset of REAL holds lower_bound (A \/ B) = min ((lower_bound A),(lower_bound B))
proofend;

theorem :: SEQ_4:143
for A, B being non empty bounded_above Subset of REAL holds upper_bound (A \/ B) = max ((upper_bound A),(upper_bound B))
proofend;

:: from TOPMETR3, 2011.04.24, A.T
theorem :: SEQ_4:144
for R being non empty Subset of REAL
for r0 being real number st ( for r being real number st r in R holds
r <= r0 ) holds
upper_bound R <= r0
proofend;