:: by Jaros{\l}aw Kotowicz

::

:: Received November 23, 1989

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

theorem Th1: :: SEQ_4:1

for X, Y being Subset of REAL st ( for r, p being Real st r in X & p in Y holds

r < p ) holds

ex g being Real st

for r, p being Real st r in X & p in Y holds

( r <= g & g <= p )

r < p ) holds

ex g being Real st

for r, p being Real st r in X & p in Y holds

( r <= g & g <= p )

proof end;

theorem Th2: :: SEQ_4:2

for p being Real

for X being Subset of REAL st 0 < p & ex r being Real st r in X & ( for r being Real st r in X holds

r + p in X ) holds

for g being Real ex r being Real st

( r in X & g < r )

for X being Subset of REAL st 0 < p & ex r being Real st r in X & ( for r being Real st r in X holds

r + p in X ) holds

for g being Real ex r being Real st

( r in X & g < r )

proof end;

theorem :: SEQ_4:4

for X being Subset of REAL holds

( X is real-bounded iff ex s being Real st

( 0 < s & ( for r being Real st r in X holds

|.r.| < s ) ) )

( X is real-bounded iff ex s being Real st

( 0 < s & ( for r being Real st r in X holds

|.r.| < s ) ) )

proof end;

definition

let r be Real;

:: original: {

redefine func {r} -> Subset of REAL;

coherence

{r} is Subset of REAL

end;
:: original: {

redefine func {r} -> Subset of REAL;

coherence

{r} is Subset of REAL

proof end;

theorem Th5: :: SEQ_4:5

for X being real-membered set st not X is empty & X is bounded_above holds

ex g being Real st

( ( for r being Real st r in X holds

r <= g ) & ( for s being Real st 0 < s holds

ex r being Real st

( r in X & g - s < r ) ) )

ex g being Real st

( ( for r being Real st r in X holds

r <= g ) & ( for s being Real st 0 < s holds

ex r being Real st

( r in X & g - s < r ) ) )

proof end;

theorem Th6: :: SEQ_4:6

for g1, g2 being Real

for X being real-membered set st ( for r being Real st r in X holds

r <= g1 ) & ( for s being Real st 0 < s holds

ex r being Real st

( r in X & g1 - s < r ) ) & ( for r being Real st r in X holds

r <= g2 ) & ( for s being Real st 0 < s holds

ex r being Real st

( r in X & g2 - s < r ) ) holds

g1 = g2

for X being real-membered set st ( for r being Real st r in X holds

r <= g1 ) & ( for s being Real st 0 < s holds

ex r being Real st

( r in X & g1 - s < r ) ) & ( for r being Real st r in X holds

r <= g2 ) & ( for s being Real st 0 < s holds

ex r being Real st

( r in X & g2 - s < r ) ) holds

g1 = g2

proof end;

theorem Th7: :: SEQ_4:7

for X being real-membered set st not X is empty & X is bounded_below holds

ex g being Real st

( ( for r being Real st r in X holds

g <= r ) & ( for s being Real st 0 < s holds

ex r being Real st

( r in X & r < g + s ) ) )

ex g being Real st

( ( for r being Real st r in X holds

g <= r ) & ( for s being Real st 0 < s holds

ex r being Real st

( r in X & r < g + s ) ) )

proof end;

theorem Th8: :: SEQ_4:8

for g1, g2 being Real

for X being real-membered set st ( for r being Real st r in X holds

g1 <= r ) & ( for s being Real st 0 < s holds

ex r being Real st

( r in X & r < g1 + s ) ) & ( for r being Real st r in X holds

g2 <= r ) & ( for s being Real st 0 < s holds

ex r being Real st

( r in X & r < g2 + s ) ) holds

g1 = g2

for X being real-membered set st ( for r being Real st r in X holds

g1 <= r ) & ( for s being Real st 0 < s holds

ex r being Real st

( r in X & r < g1 + s ) ) & ( for r being Real st r in X holds

g2 <= r ) & ( for s being Real st 0 < s holds

ex r being Real st

( r in X & r < g2 + s ) ) holds

g1 = g2

proof end;

definition

let X be real-membered set ;

assume A1: ( not X is empty & X is bounded_above ) ;

ex b_{1} being Real st

( ( for r being Real st r in X holds

r <= b_{1} ) & ( for s being Real st 0 < s holds

ex r being Real st

( r in X & b_{1} - s < r ) ) )
by A1, Th5;

uniqueness

for b_{1}, b_{2} being Real st ( for r being Real st r in X holds

r <= b_{1} ) & ( for s being Real st 0 < s holds

ex r being Real st

( r in X & b_{1} - s < r ) ) & ( for r being Real st r in X holds

r <= b_{2} ) & ( for s being Real st 0 < s holds

ex r being Real st

( r in X & b_{2} - s < r ) ) holds

b_{1} = b_{2}
by Th6;

end;
assume A1: ( not X is empty & X is bounded_above ) ;

func upper_bound X -> Real means :Def1: :: SEQ_4:def 1

( ( for r being Real st r in X holds

r <= it ) & ( for s being Real st 0 < s holds

ex r being Real st

( r in X & it - s < r ) ) );

existence ( ( for r being Real st r in X holds

r <= it ) & ( for s being Real st 0 < s holds

ex r being Real st

( r in X & it - s < r ) ) );

ex b

( ( for r being Real st r in X holds

r <= b

ex r being Real st

( r in X & b

uniqueness

for b

r <= b

ex r being Real st

( r in X & b

r <= b

ex r being Real st

( r in X & b

b

:: deftheorem Def1 defines upper_bound SEQ_4:def 1 :

for X being real-membered set st not X is empty & X is bounded_above holds

for b_{2} being Real holds

( b_{2} = upper_bound X iff ( ( for r being Real st r in X holds

r <= b_{2} ) & ( for s being Real st 0 < s holds

ex r being Real st

( r in X & b_{2} - s < r ) ) ) );

for X being real-membered set st not X is empty & X is bounded_above holds

for b

( b

r <= b

ex r being Real st

( r in X & b

definition

let X be real-membered set ;

assume A1: ( not X is empty & X is bounded_below ) ;

ex b_{1} being Real st

( ( for r being Real st r in X holds

b_{1} <= r ) & ( for s being Real st 0 < s holds

ex r being Real st

( r in X & r < b_{1} + s ) ) )
by A1, Th7;

uniqueness

for b_{1}, b_{2} being Real st ( for r being Real st r in X holds

b_{1} <= r ) & ( for s being Real st 0 < s holds

ex r being Real st

( r in X & r < b_{1} + s ) ) & ( for r being Real st r in X holds

b_{2} <= r ) & ( for s being Real st 0 < s holds

ex r being Real st

( r in X & r < b_{2} + s ) ) holds

b_{1} = b_{2}
by Th8;

end;
assume A1: ( not X is empty & X is bounded_below ) ;

func lower_bound X -> Real means :Def2: :: SEQ_4:def 2

( ( for r being Real st r in X holds

it <= r ) & ( for s being Real st 0 < s holds

ex r being Real st

( r in X & r < it + s ) ) );

existence ( ( for r being Real st r in X holds

it <= r ) & ( for s being Real st 0 < s holds

ex r being Real st

( r in X & r < it + s ) ) );

ex b

( ( for r being Real st r in X holds

b

ex r being Real st

( r in X & r < b

uniqueness

for b

b

ex r being Real st

( r in X & r < b

b

ex r being Real st

( r in X & r < b

b

:: deftheorem Def2 defines lower_bound SEQ_4:def 2 :

for X being real-membered set st not X is empty & X is bounded_below holds

for b_{2} being Real holds

( b_{2} = lower_bound X iff ( ( for r being Real st r in X holds

b_{2} <= r ) & ( for s being Real st 0 < s holds

ex r being Real st

( r in X & r < b_{2} + s ) ) ) );

for X being real-membered set st not X is empty & X is bounded_below holds

for b

( b

b

ex r being Real st

( r in X & r < b

Lm1: for r being Real

for X being non empty real-membered set st ( for s being Real st s in X holds

s >= r ) & ( for t being Real st ( for s being Real st s in X holds

s >= t ) holds

r >= t ) holds

r = lower_bound X

proof end;

Lm2: for X being non empty real-membered set

for r being Real st ( for s being Real st s in X holds

s <= r ) & ( for t being Real st ( for s being Real st s in X holds

s <= t ) holds

r <= t ) holds

r = upper_bound X

proof end;

registration
end;

registration
end;

theorem :: SEQ_4:11

for X being Subset of REAL st X is real-bounded & not X is empty holds

lower_bound X <= upper_bound X

lower_bound X <= upper_bound X

proof end;

theorem :: SEQ_4:12

for X being Subset of REAL st X is real-bounded & not X is empty holds

( ex r, p being Real st

( r in X & p in X & p <> r ) iff lower_bound X < upper_bound X )

( ex r, p being Real st

( r in X & p in X & p <> r ) iff lower_bound X < upper_bound X )

proof end;

registration

let seq be convergent Real_Sequence;

coherence

for b_{1} being Real_Sequence st b_{1} = abs seq holds

b_{1} is convergent
by Th13;

end;
coherence

for b

b

theorem :: SEQ_4:15

for seq being Real_Sequence st abs seq is convergent & lim (abs seq) = 0 holds

( seq is convergent & lim seq = 0 )

( seq is convergent & lim seq = 0 )

proof end;

theorem Th16: :: SEQ_4:16

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

seq1 is convergent

seq1 is convergent

proof end;

theorem Th17: :: SEQ_4:17

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

lim seq1 = lim seq

lim seq1 = lim seq

proof end;

theorem Th18: :: SEQ_4:18

for seq, seq1 being Real_Sequence st seq is convergent & ex k being Nat st

for n being Nat st k <= n holds

seq1 . n = seq . n holds

seq1 is convergent

for n being Nat st k <= n holds

seq1 . n = seq . n holds

seq1 is convergent

proof end;

theorem :: SEQ_4:19

for seq, seq1 being Real_Sequence st seq is convergent & ex k being Nat st

for n being Nat st k <= n holds

seq1 . n = seq . n holds

lim seq = lim seq1

for n being Nat st k <= n holds

seq1 . n = seq . n holds

lim seq = lim seq1

proof end;

registration

let seq be convergent Real_Sequence;

let k be Nat;

coherence

for b_{1} being Real_Sequence st b_{1} = seq ^\ k holds

b_{1} is convergent
by Th16;

end;
let k be Nat;

coherence

for b

b

theorem :: SEQ_4:20

for k being Nat

for seq being Real_Sequence st seq is convergent holds

lim (seq ^\ k) = lim seq by Th17;

for seq being Real_Sequence st seq is convergent holds

lim (seq ^\ k) = lim seq by Th17;

theorem :: SEQ_4:22

for k being Nat

for seq being Real_Sequence st seq ^\ k is convergent holds

lim seq = lim (seq ^\ k)

for seq being Real_Sequence st seq ^\ k is convergent holds

lim seq = lim (seq ^\ k)

proof end;

theorem Th23: :: SEQ_4:23

for seq being Real_Sequence st seq is convergent & lim seq <> 0 holds

ex k being Nat st seq ^\ k is non-zero

ex k being Nat st seq ^\ k is non-zero

proof end;

theorem :: SEQ_4:24

for seq being Real_Sequence st seq is convergent & lim seq <> 0 holds

ex seq1 being Real_Sequence st

( seq1 is subsequence of seq & seq1 is non-zero )

ex seq1 being Real_Sequence st

( seq1 is subsequence of seq & seq1 is non-zero )

proof end;

reconsider zz = 0 as Nat ;

theorem Th25: :: SEQ_4:25

for r being Real

for seq being Real_Sequence st seq is constant & ( r in rng seq or ex n being Nat st seq . n = r ) holds

lim seq = r

for seq being Real_Sequence st seq is constant & ( r in rng seq or ex n being Nat st seq . n = r ) holds

lim seq = r

proof end;

theorem :: SEQ_4:26

theorem :: SEQ_4:27

for seq being Real_Sequence st seq is convergent & lim seq <> 0 holds

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

lim (seq1 ") = (lim seq) "

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

lim (seq1 ") = (lim seq) "

proof end;

theorem Th28: :: SEQ_4:28

for r being Real

for seq being Real_Sequence st 0 <= r & ( for n being Nat holds seq . n = 1 / (n + r) ) holds

seq is convergent

for seq being Real_Sequence st 0 <= r & ( for n being Nat holds seq . n = 1 / (n + r) ) holds

seq is convergent

proof end;

theorem Th29: :: SEQ_4:29

for r being Real

for seq being Real_Sequence st 0 <= r & ( for n being Nat holds seq . n = 1 / (n + r) ) holds

lim seq = 0

for seq being Real_Sequence st 0 <= r & ( for n being Nat holds seq . n = 1 / (n + r) ) holds

lim seq = 0

proof end;

theorem :: SEQ_4:30

theorem :: SEQ_4:31

for r, g being Real

for seq being Real_Sequence st 0 <= r & ( for n being Nat holds seq . n = g / (n + r) ) holds

( seq is convergent & lim seq = 0 )

for seq being Real_Sequence st 0 <= r & ( for n being Nat holds seq . n = g / (n + r) ) holds

( seq is convergent & lim seq = 0 )

proof end;

theorem Th32: :: SEQ_4:32

for r being Real

for seq being Real_Sequence st 0 <= r & ( for n being Nat holds seq . n = 1 / ((n * n) + r) ) holds

seq is convergent

for seq being Real_Sequence st 0 <= r & ( for n being Nat holds seq . n = 1 / ((n * n) + r) ) holds

seq is convergent

proof end;

theorem Th33: :: SEQ_4:33

for r being Real

for seq being Real_Sequence st 0 <= r & ( for n being Nat holds seq . n = 1 / ((n * n) + r) ) holds

lim seq = 0

for seq being Real_Sequence st 0 <= r & ( for n being Nat holds seq . n = 1 / ((n * n) + r) ) holds

lim seq = 0

proof end;

theorem :: SEQ_4:34

theorem :: SEQ_4:35

for r, g being Real

for seq being Real_Sequence st 0 <= r & ( for n being Nat holds seq . n = g / ((n * n) + r) ) holds

( seq is convergent & lim seq = 0 )

for seq being Real_Sequence st 0 <= r & ( for n being Nat holds seq . n = g / ((n * n) + r) ) holds

( seq is convergent & lim seq = 0 )

proof end;

registration

for b_{1} being Real_Sequence st b_{1} is V47() & b_{1} is bounded_above holds

b_{1} is convergent
end;

cluster Function-like V18( NAT , REAL ) V47() bounded_above -> convergent for Element of bool [:NAT,REAL:];

coherence for b

b

proof end;

registration

for b_{1} being Real_Sequence st b_{1} is V48() & b_{1} is bounded_below holds

b_{1} is convergent
end;

cluster Function-like V18( NAT , REAL ) V48() bounded_below -> convergent for Element of bool [:NAT,REAL:];

coherence for b

b

proof end;

registration

for b_{1} being Real_Sequence st b_{1} is monotone & b_{1} is bounded holds

b_{1} is convergent
end;

cluster Function-like V18( NAT , REAL ) monotone bounded -> convergent for Element of bool [:NAT,REAL:];

coherence for b

b

proof end;

theorem :: SEQ_4:37

for seq being Real_Sequence st seq is bounded_above & seq is V47() holds

for n being Nat holds seq . n <= lim seq

for n being Nat holds seq . n <= lim seq

proof end;

theorem :: SEQ_4:38

for seq being Real_Sequence st seq is bounded_below & seq is V48() holds

for n being Nat holds lim seq <= seq . n

for n being Nat holds lim seq <= seq . n

proof end;

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 & seq1 is convergent )

ex seq1 being Real_Sequence st

( seq1 is subsequence of seq & seq1 is convergent )

proof end;

theorem :: SEQ_4:41

for seq being Real_Sequence holds

( seq is convergent iff for s being Real st 0 < s holds

ex n being Nat st

for m being Nat st n <= m holds

|.((seq . m) - (seq . n)).| < s )

( seq is convergent iff for s being Real st 0 < s holds

ex n being Nat st

for m being Nat st n <= m holds

|.((seq . m) - (seq . n)).| < s )

proof end;

theorem :: SEQ_4:42

for seq, seq1 being Real_Sequence st seq is constant & seq1 is convergent holds

( lim (seq + seq1) = (seq . 0) + (lim seq1) & lim (seq - seq1) = (seq . 0) - (lim seq1) & lim (seq1 - seq) = (lim seq1) - (seq . 0) & lim (seq (#) seq1) = (seq . 0) * (lim seq1) )

( lim (seq + seq1) = (seq . 0) + (lim seq1) & lim (seq - seq1) = (seq . 0) - (lim seq1) & lim (seq1 - seq) = (lim seq1) - (seq . 0) & lim (seq (#) seq1) = (seq . 0) * (lim seq1) )

proof end;

:: from PSCOMP_1

theorem Th43: :: SEQ_4:43

for X being non empty real-membered set

for t being Real st ( for s being Real st s in X holds

s >= t ) holds

lower_bound X >= t

for t being Real st ( for s being Real st s in X holds

s >= t ) holds

lower_bound X >= t

proof end;

theorem Th45: :: SEQ_4:45

for X being non empty real-membered set

for r, t being Real st ( for s being Real st s in X holds

s <= t ) holds

upper_bound X <= t

for r, t being Real st ( for s being Real st s in X holds

s <= t ) holds

upper_bound X <= t

proof end;

theorem :: SEQ_4:47

for X being non empty real-membered set

for Y being real-membered set st X c= Y & Y is bounded_below holds

lower_bound Y <= lower_bound X

for Y being real-membered set st X c= Y & Y is bounded_below holds

lower_bound Y <= lower_bound X

proof end;

theorem :: SEQ_4:48

for X being non empty real-membered set

for Y being real-membered set st X c= Y & Y is bounded_above holds

upper_bound X <= upper_bound Y

for Y being real-membered set st X c= Y & Y is bounded_above holds

upper_bound X <= upper_bound Y

proof end;

:: 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;
:: original: inf

redefine func min A -> Element of NAT ;

coherence

inf A is Element of NAT by ORDINAL1:def 12;

definition

compatibility

for b_{1} being Element of bool [:[:COMPLEX,COMPLEX:],COMPLEX:] holds

( b_{1} = diffcomplex iff b_{1} = addcomplex * ((id COMPLEX),compcomplex) )

end;
for b

( b

proof end;

:: deftheorem defines diffcomplex SEQ_4:def 3 :

diffcomplex = addcomplex * ((id COMPLEX),compcomplex);

diffcomplex = addcomplex * ((id COMPLEX),compcomplex);

definition
end;

:: deftheorem defines multcomplex SEQ_4:def 4 :

for c being Complex holds c multcomplex = multcomplex [;] (c,(id COMPLEX));

for c being Complex holds c multcomplex = multcomplex [;] (c,(id COMPLEX));

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

proof end;

theorem :: SEQ_4:56

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

definition

ex b_{1} being Function of COMPLEX,REAL st

for c being Element of COMPLEX holds b_{1} . c = |.c.|

for b_{1}, b_{2} being Function of COMPLEX,REAL st ( for c being Element of COMPLEX holds b_{1} . c = |.c.| ) & ( for c being Element of COMPLEX holds b_{2} . c = |.c.| ) holds

b_{1} = b_{2}
from BINOP_2:sch 1();

end;

func abscomplex -> Function of COMPLEX,REAL means :Def5: :: SEQ_4:def 5

for c being Element of COMPLEX holds it . c = |.c.|;

existence for c being Element of COMPLEX holds it . c = |.c.|;

ex b

for c being Element of COMPLEX holds b

proof end;

uniqueness for b

b

:: deftheorem Def5 defines abscomplex SEQ_4:def 5 :

for b_{1} being Function of COMPLEX,REAL holds

( b_{1} = abscomplex iff for c being Element of COMPLEX holds b_{1} . c = |.c.| );

for b

( b

definition

let z1, z2 be FinSequence of COMPLEX ;

z1 + z2 is FinSequence of COMPLEX

for b_{1} being FinSequence of COMPLEX holds

( b_{1} = z1 + z2 iff b_{1} = addcomplex .: (z1,z2) )

z1 - z2 is FinSequence of COMPLEX

for b_{1} being FinSequence of COMPLEX holds

( b_{1} = z1 - z2 iff b_{1} = diffcomplex .: (z1,z2) )

end;
:: original: +

redefine func z1 + z2 -> FinSequence of COMPLEX equals :: SEQ_4:def 6

addcomplex .: (z1,z2);

coherence redefine func z1 + z2 -> FinSequence of COMPLEX equals :: SEQ_4:def 6

addcomplex .: (z1,z2);

z1 + z2 is FinSequence of COMPLEX

proof end;

compatibility for b

( b

proof end;

:: original: -

redefine func z1 - z2 -> FinSequence of COMPLEX equals :: SEQ_4:def 7

diffcomplex .: (z1,z2);

coherence redefine func z1 - z2 -> FinSequence of COMPLEX equals :: SEQ_4:def 7

diffcomplex .: (z1,z2);

z1 - z2 is FinSequence of COMPLEX

proof end;

compatibility for b

( b

proof end;

:: deftheorem defines + SEQ_4:def 6 :

for z1, z2 being FinSequence of COMPLEX holds z1 + z2 = addcomplex .: (z1,z2);

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);

for z1, z2 being FinSequence of COMPLEX holds z1 - z2 = diffcomplex .: (z1,z2);

definition

let z be FinSequence of COMPLEX ;

coherence

- z is FinSequence of COMPLEX

for b_{1} being FinSequence of COMPLEX holds

( b_{1} = - z iff b_{1} = compcomplex * z )

end;
coherence

- z is FinSequence of COMPLEX

proof end;

compatibility for b

( b

proof end;

:: deftheorem defines - SEQ_4:def 8 :

for z being FinSequence of COMPLEX holds - z = compcomplex * z;

for z being FinSequence of COMPLEX holds - z = compcomplex * z;

definition

let z be FinSequence of COMPLEX ;

let c be Complex;

c * z is FinSequence of COMPLEX

for b_{1} being FinSequence of COMPLEX holds

( b_{1} = c * z iff b_{1} = (c multcomplex) * z )

end;
let c be Complex;

:: original: *

redefine func c * z -> FinSequence of COMPLEX equals :: SEQ_4:def 9

(c multcomplex) * z;

coherence redefine func c * z -> FinSequence of COMPLEX equals :: SEQ_4:def 9

(c multcomplex) * z;

c * z is FinSequence of COMPLEX

proof end;

compatibility for b

( b

proof end;

:: deftheorem defines * SEQ_4:def 9 :

for z being FinSequence of COMPLEX

for c being Complex holds c * z = (c multcomplex) * z;

for z being FinSequence of COMPLEX

for c being Complex holds c * z = (c multcomplex) * z;

definition

let z be FinSequence of COMPLEX ;

coherence

|.z.| is FinSequence of REAL

for b_{1} being FinSequence of REAL holds

( b_{1} = |.z.| iff b_{1} = abscomplex * z )

end;
coherence

|.z.| is FinSequence of REAL

proof end;

compatibility for b

( b

proof end;

:: deftheorem defines abs SEQ_4:def 10 :

for z being FinSequence of COMPLEX holds abs z = abscomplex * z;

for z being FinSequence of COMPLEX holds abs z = abscomplex * z;

definition
end;

:: deftheorem defines COMPLEX SEQ_4:def 11 :

for n being Nat holds COMPLEX n = n -tuples_on COMPLEX;

for n being Nat holds COMPLEX n = n -tuples_on COMPLEX;

Lm4: for n being Nat

for z being Element of COMPLEX n holds dom z = Seg n

proof end;

definition

let n be Nat;

let z1, z2 be Element of COMPLEX n;

:: original: +

redefine func z1 + z2 -> Element of COMPLEX n;

coherence

z1 + z2 is Element of COMPLEX n by FINSEQ_2:120;

end;
let z1, z2 be Element of COMPLEX n;

:: original: +

redefine func z1 + z2 -> Element of COMPLEX n;

coherence

z1 + z2 is Element of COMPLEX n by FINSEQ_2:120;

theorem Th58: :: SEQ_4:58

for k, n being Nat

for c1, c2 being Element of COMPLEX

for z1, z2 being Element of COMPLEX n st k in Seg n & c1 = z1 . k & c2 = z2 . k holds

(z1 + z2) . k = c1 + c2

for c1, c2 being Element of COMPLEX

for z1, z2 being Element of COMPLEX n st k in Seg n & c1 = z1 . k & c2 = z2 . k holds

(z1 + z2) . k = c1 + c2

proof end;

definition

let n be Nat;

:: original: 0c

redefine func 0c n -> Element of COMPLEX n;

coherence

0c n is Element of COMPLEX n ;

end;
:: original: 0c

redefine func 0c n -> Element of COMPLEX n;

coherence

0c n is Element of COMPLEX n ;

theorem :: SEQ_4:59

definition

let n be 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;
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;

theorem Th60: :: SEQ_4:60

for k, n being Nat

for c being Element of COMPLEX

for z being Element of COMPLEX n st k in Seg n & c = z . k holds

(- z) . k = - c

for c being Element of COMPLEX

for z being Element of COMPLEX n st k in Seg n & c = z . k holds

(- z) . k = - c

proof end;

Lm5: for n being Nat holds - (0c n) = 0c n

proof end;

theorem :: SEQ_4:61

theorem :: SEQ_4:62

::$CT

Lm6: for n being Nat

for z, z1, z2 being Element of COMPLEX n st z1 + z = z2 + z holds

z1 = z2

proof end;

theorem :: SEQ_4:65

definition

let n be Nat;

let z1, z2 be Element of COMPLEX n;

:: original: -

redefine func z1 - z2 -> Element of COMPLEX n;

coherence

z1 - z2 is Element of COMPLEX n by FINSEQ_2:120;

end;
let z1, z2 be Element of COMPLEX n;

:: original: -

redefine func z1 - z2 -> Element of COMPLEX n;

coherence

z1 - z2 is Element of COMPLEX n by FINSEQ_2:120;

theorem :: SEQ_4:67

for k, n being Nat

for z1, z2 being Element of COMPLEX n st k in Seg n holds

(z1 - z2) . k = (z1 . k) - (z2 . k)

for z1, z2 being Element of COMPLEX n st k in Seg n holds

(z1 - z2) . k = (z1 . k) - (z2 . k)

proof end;

theorem :: SEQ_4:70

theorem :: SEQ_4:78

definition

let n be Nat;

let z be Element of COMPLEX n;

let c be Element of COMPLEX ;

:: original: *

redefine func c * z -> Element of COMPLEX n;

coherence

c * z is Element of COMPLEX n by FINSEQ_2:113;

end;
let z be Element of COMPLEX n;

let c be Element of COMPLEX ;

:: original: *

redefine func c * z -> Element of COMPLEX n;

coherence

c * z is Element of COMPLEX n by FINSEQ_2:113;

theorem Th81: :: SEQ_4:82

for k, n being Nat

for c, c9 being Element of COMPLEX

for z being Element of COMPLEX n st k in Seg n & c9 = z . k holds

(c * z) . k = c * c9

for c, c9 being Element of COMPLEX

for z being Element of COMPLEX n st k in Seg n & c9 = z . k holds

(c * z) . k = c * c9

proof end;

theorem :: SEQ_4:83

for n being Nat

for c1, c2 being Element of COMPLEX

for z being Element of COMPLEX n holds c1 * (c2 * z) = (c1 * c2) * z

for c1, c2 being Element of COMPLEX

for z being Element of COMPLEX n holds c1 * (c2 * z) = (c1 * c2) * z

proof end;

theorem :: SEQ_4:84

for n being Nat

for c1, c2 being Element of COMPLEX

for z being Element of COMPLEX n holds (c1 + c2) * z = (c1 * z) + (c2 * z)

for c1, c2 being Element of COMPLEX

for z being Element of COMPLEX n holds (c1 + c2) * z = (c1 * z) + (c2 * z)

proof end;

theorem :: SEQ_4:85

definition

let n be 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;
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;

theorem Th88: :: SEQ_4:89

for k, n being Nat

for c being Element of COMPLEX

for z being Element of COMPLEX n st k in Seg n & c = z . k holds

(abs z) . k = |.c.|

for c being Element of COMPLEX

for z being Element of COMPLEX n st k in Seg n & c = z . k holds

(abs z) . k = |.c.|

proof end;

theorem Th91: :: SEQ_4:92

for n being Nat

for c being Element of COMPLEX

for z being Element of COMPLEX n holds abs (c * z) = |.c.| * (abs z)

for c being Element of COMPLEX

for z being Element of COMPLEX n holds abs (c * z) = |.c.| * (abs z)

proof end;

definition
end;

:: deftheorem defines |. SEQ_4:def 13 :

for z being FinSequence of COMPLEX holds |.z.| = sqrt (Sum (sqr (abs z)));

for z being FinSequence of COMPLEX holds |.z.| = sqrt (Sum (sqr (abs z)));

theorem :: SEQ_4:96

theorem :: SEQ_4:97

for n being Nat

for c being Element of COMPLEX

for z being Element of COMPLEX n holds |.(c * z).| = |.c.| * |.z.|

for c being Element of COMPLEX

for z being Element of COMPLEX n holds |.(c * z).| = |.c.| * |.z.|

proof end;

theorem Th104: :: SEQ_4:105

for n being Nat

for z, z1, z2 being Element of COMPLEX n holds |.(z1 - z2).| <= |.(z1 - z).| + |.(z - z2).|

for z, z1, z2 being Element of COMPLEX n holds |.(z1 - z2).| <= |.(z1 - z).| + |.(z - z2).|

proof end;

:: deftheorem defines open SEQ_4:def 14 :

for n being 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 & ( for z being Element of COMPLEX n st |.z.| < r holds

x + z in A ) ) );

for n being 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 & ( for z being Element of COMPLEX n st |.z.| < r holds

x + z in A ) ) );

:: deftheorem defines closed SEQ_4:def 15 :

for n being 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 & x + z in A ) ) holds

x in A );

for n being 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 & x + z in A ) ) holds

x in A );

theorem :: SEQ_4:108

for n being 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

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

proof end;

theorem :: SEQ_4:109

for n being Nat

for A, B being Subset of (COMPLEX n) st A is open & B is open holds

for C being Subset of (COMPLEX n) st C = A /\ B holds

C is open

for A, B being Subset of (COMPLEX n) st A is open & B is open holds

for C being Subset of (COMPLEX n) st C = A /\ B holds

C is open

proof end;

definition

let n be Nat;

let x be Element of COMPLEX n;

let r be Real;

{ z where z is Element of COMPLEX n : |.(z - x).| < r } is Subset of (COMPLEX n)

end;
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 } ;

{ z where z is Element of COMPLEX n : |.(z - x).| < r } is Subset of (COMPLEX n)

proof end;

:: deftheorem defines Ball SEQ_4:def 16 :

for n being 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 } ;

for n being 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 Th109: :: SEQ_4:110

for n being Nat

for r being Real

for x, z being Element of COMPLEX n holds

( z in Ball (x,r) iff |.(x - z).| < r )

for r being Real

for x, z being Element of COMPLEX n holds

( z in Ball (x,r) iff |.(x - z).| < r )

proof end;

definition

let n be Nat;

let x be Element of COMPLEX n;

let A be Subset of (COMPLEX n);

deffunc H_{1}( Element of COMPLEX n) -> Element of REAL = In (|.(x - $1).|,REAL);

deffunc H_{2}( Element of COMPLEX n) -> Real = |.(x - $1).|;

defpred S_{1}[ set ] means $1 in A;

reconsider X = { H_{1}(z) where z is Element of COMPLEX n : S_{1}[z] } as Subset of REAL from DOMAIN_1:sch 8();

A1: for z being Element of COMPLEX n holds H_{1}(z) = H_{2}(z)
;

A2: { H_{1}(z1) where z1 is Element of COMPLEX n : S_{1}[z1] } = { H_{2}(z2) where z2 is Element of COMPLEX n : S_{1}[z2] }
from FRAENKEL:sch 5(A1);

ex b_{1} being Real st

for X being Subset of REAL st X = { |.(x - z).| where z is Element of COMPLEX n : z in A } holds

b_{1} = lower_bound X

for b_{1}, b_{2} being Real st ( for X being Subset of REAL st X = { |.(x - z).| where z is Element of COMPLEX n : z in A } holds

b_{1} = lower_bound X ) & ( for X being Subset of REAL st X = { |.(x - z).| where z is Element of COMPLEX n : z in A } holds

b_{2} = lower_bound X ) holds

b_{1} = b_{2}

end;
let x be Element of COMPLEX n;

let A be Subset of (COMPLEX n);

deffunc H

deffunc H

defpred S

reconsider X = { H

A1: for z being Element of COMPLEX n holds H

A2: { H

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 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;

ex b

for X being Subset of REAL st X = { |.(x - z).| where z is Element of COMPLEX n : z in A } holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def17 defines dist SEQ_4:def 17 :

for n being Nat

for x being Element of COMPLEX n

for A being Subset of (COMPLEX n)

for b_{4} being Real holds

( b_{4} = 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

b_{4} = lower_bound X );

for n being Nat

for x being Element of COMPLEX n

for A being Subset of (COMPLEX n)

for b

( b

b

definition

let n be Nat;

let A be Subset of (COMPLEX n);

let r be Real;

{ z where z is Element of COMPLEX n : dist (z,A) < r } is Subset of (COMPLEX n)

end;
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 } ;

{ z where z is Element of COMPLEX n : dist (z,A) < r } is Subset of (COMPLEX n)

proof end;

:: deftheorem defines Ball SEQ_4:def 18 :

for n being 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 } ;

for n being 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 Th112: :: SEQ_4:113

for X being Subset of REAL

for r being Real st X <> {} & ( for r9 being Real st r9 in X holds

r <= r9 ) holds

lower_bound X >= r

for r being Real st X <> {} & ( for r9 being Real st r9 in X holds

r <= r9 ) holds

lower_bound X >= r

proof end;

theorem Th113: :: SEQ_4:114

for n being Nat

for x being Element of COMPLEX n

for A being Subset of (COMPLEX n) st A <> {} holds

dist (x,A) >= 0

for x being Element of COMPLEX n

for A being Subset of (COMPLEX n) st A <> {} holds

dist (x,A) >= 0

proof end;

theorem Th114: :: SEQ_4:115

for n being 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.|

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.|

proof end;

theorem Th115: :: SEQ_4:116

for n being Nat

for x being Element of COMPLEX n

for A being Subset of (COMPLEX n) st x in A holds

dist (x,A) = 0

for x being Element of COMPLEX n

for A being Subset of (COMPLEX n) st x in A holds

dist (x,A) = 0

proof end;

theorem :: SEQ_4:117

for n being Nat

for x being Element of COMPLEX n

for A being Subset of (COMPLEX n) st not x in A & A <> {} & A is closed holds

dist (x,A) > 0

for x being Element of COMPLEX n

for A being Subset of (COMPLEX n) st not x in A & A <> {} & A is closed holds

dist (x,A) > 0

proof end;

theorem :: SEQ_4:118

for n being Nat

for x, z1 being Element of COMPLEX n

for A being Subset of (COMPLEX n) st A <> {} holds

|.(z1 - x).| + (dist (x,A)) >= dist (z1,A)

for x, z1 being Element of COMPLEX n

for A being Subset of (COMPLEX n) st A <> {} holds

|.(z1 - x).| + (dist (x,A)) >= dist (z1,A)

proof end;

theorem Th118: :: SEQ_4:119

for n being 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 )

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 )

proof end;

theorem Th119: :: SEQ_4:120

for n being Nat

for r being Real

for x being Element of COMPLEX n

for A being Subset of (COMPLEX n) st 0 < r & x in A holds

x in Ball (A,r)

for r being Real

for x being Element of COMPLEX n

for A being Subset of (COMPLEX n) st 0 < r & x in A holds

x in Ball (A,r)

proof end;

theorem :: SEQ_4:121

theorem :: SEQ_4:122

for n being Nat

for r1 being Real

for A being Subset of (COMPLEX n) st A <> {} holds

Ball (A,r1) is open

for r1 being Real

for A being Subset of (COMPLEX n) st A <> {} holds

Ball (A,r1) is open

proof end;

definition

let n be Nat;

let A, B be Subset of (COMPLEX n);

deffunc H_{1}( Element of COMPLEX n, Element of COMPLEX n) -> Element of REAL = In (|.($1 - $2).|,REAL);

deffunc H_{2}( Element of COMPLEX n, Element of COMPLEX n) -> Real = |.($1 - $2).|;

defpred S_{1}[ set , set ] means ( $1 in A & $2 in B );

reconsider X = { H_{1}(x,z) where x, z is Element of COMPLEX n : S_{1}[x,z] } as Subset of REAL from DOMAIN_1:sch 9();

A1: for z1, z2 being Element of COMPLEX n holds H_{1}(z1,z2) = H_{2}(z1,z2)
;

A2: { H_{1}(z1,z2) where z1, z2 is Element of COMPLEX n : S_{1}[z1,z2] } = { H_{2}(z1,z2) where z1, z2 is Element of COMPLEX n : S_{1}[z1,z2] }
from FRAENKEL:sch 7(A1);

ex b_{1} being Real st

for X being Subset of REAL st X = { |.(x - z).| where x, z is Element of COMPLEX n : ( x in A & z in B ) } holds

b_{1} = lower_bound X

for b_{1}, b_{2} being Real st ( for X being Subset of REAL st X = { |.(x - z).| where x, z is Element of COMPLEX n : ( x in A & z in B ) } holds

b_{1} = lower_bound X ) & ( for X being Subset of REAL st X = { |.(x - z).| where x, z is Element of COMPLEX n : ( x in A & z in B ) } holds

b_{2} = lower_bound X ) holds

b_{1} = b_{2}

end;
let A, B be Subset of (COMPLEX n);

deffunc H

deffunc H

defpred S

reconsider X = { H

A1: for z1, z2 being Element of COMPLEX n holds H

A2: { H

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 & z in B ) } holds

it = lower_bound X;

existence for X being Subset of REAL st X = { |.(x - z).| where x, z is Element of COMPLEX n : ( x in A & z in B ) } holds

it = lower_bound X;

ex b

for X being Subset of REAL st X = { |.(x - z).| where x, z is Element of COMPLEX n : ( x in A & z in B ) } holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def19 defines dist SEQ_4:def 19 :

for n being Nat

for A, B being Subset of (COMPLEX n)

for b_{4} being Real holds

( b_{4} = 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 & z in B ) } holds

b_{4} = lower_bound X );

for n being Nat

for A, B being Subset of (COMPLEX n)

for b

( b

b

theorem Th123: :: SEQ_4:124

for X, Y being Subset of REAL st X is bounded_below & Y is bounded_below holds

X ++ Y is bounded_below

X ++ Y is bounded_below

proof end;

theorem Th124: :: SEQ_4:125

for X, Y being Subset of REAL st X <> {} & X is bounded_below & Y <> {} & Y is bounded_below holds

lower_bound (X ++ Y) = (lower_bound X) + (lower_bound Y)

lower_bound (X ++ Y) = (lower_bound X) + (lower_bound Y)

proof end;

theorem Th125: :: SEQ_4:126

for X, Y being Subset of REAL st Y is bounded_below & X <> {} & ( for r being Real st r in X holds

ex r1 being Real st

( r1 in Y & r1 <= r ) ) holds

lower_bound X >= lower_bound Y

ex r1 being Real st

( r1 in Y & r1 <= r ) ) holds

lower_bound X >= lower_bound Y

proof end;

theorem Th128: :: SEQ_4:129

for n being Nat

for x being Element of COMPLEX n

for A, B being Subset of (COMPLEX n) st A <> {} & B <> {} holds

(dist (x,A)) + (dist (x,B)) >= dist (A,B)

for x being Element of COMPLEX n

for A, B being Subset of (COMPLEX n) st A <> {} & B <> {} holds

(dist (x,A)) + (dist (x,B)) >= dist (A,B)

proof end;

definition

let n be Nat;

{ A where A is Subset of (COMPLEX n) : A is open } is Subset-Family of (COMPLEX n)

end;
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 } ;

{ A where A is Subset of (COMPLEX n) : A is open } is Subset-Family of (COMPLEX n)

proof end;

:: deftheorem defines ComplexOpenSets SEQ_4:def 20 :

for n being Nat holds ComplexOpenSets n = { A where A is Subset of (COMPLEX n) : A is open } ;

for n being Nat holds ComplexOpenSets n = { A where A is Subset of (COMPLEX n) : A is open } ;

defpred S

( R is bounded_above & upper_bound R in R & R is bounded_below & lower_bound R in R );

Lm7: S

;

Lm8: for n being Nat st S

S

proof end;

Lm9: for n being Nat holds S

from NAT_1:sch 2(Lm7, Lm8);

theorem Th132: :: SEQ_4:133

for R being finite Subset of REAL st R <> {} holds

( R is bounded_above & upper_bound R in R & R is bounded_below & lower_bound R in R )

( R is bounded_above & upper_bound R in R & R is bounded_below & lower_bound R in R )

proof end;

theorem :: SEQ_4:134

for n being Nat

for f being FinSequence holds

( 1 <= n & n + 1 <= len f iff ( n in dom f & n + 1 in dom f ) )

for f being FinSequence holds

( 1 <= n & n + 1 <= len f iff ( n in dom f & n + 1 in dom f ) )

proof end;

theorem :: SEQ_4:135

for n being Nat

for f being FinSequence holds

( 1 <= n & n + 2 <= len f iff ( n in dom f & n + 1 in dom f & n + 2 in dom f ) )

for f being FinSequence holds

( 1 <= n & n + 2 <= len f iff ( n in dom f & n + 1 in dom f & n + 2 in dom f ) )

proof end;

theorem :: SEQ_4:136

for D being non empty set

for f1, f2 being FinSequence of D

for n being Nat st 1 <= n & n <= len f2 holds

(f1 ^ f2) /. (n + (len f1)) = f2 /. n

for f1, f2 being FinSequence of D

for n being Nat st 1 <= n & n <= len f2 holds

(f1 ^ f2) /. (n + (len f1)) = f2 /. n

proof end;

theorem :: SEQ_4:137

for v being FinSequence of REAL st v is increasing holds

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

v . n <= v . m

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

v . n <= v . m

proof end;

theorem Th137: :: SEQ_4:138

for v being FinSequence of REAL st v is increasing holds

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

v . n <> v . m

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

v . n <> v . m

proof end;

theorem Th138: :: SEQ_4:139

for v, v1 being FinSequence of REAL

for n being Nat st v is increasing & v1 = v | (Seg n) holds

v1 is increasing

for n being Nat st v is increasing & v1 = v | (Seg n) holds

v1 is increasing

proof end;

defpred S

ex v1 being FinSequence of REAL st

( rng v1 = rng v & len v1 = card (rng v) & v1 is increasing );

Lm10: S

proof end;

Lm11: for n being Nat st S

S

proof end;

Lm12: for n being Nat holds S

from NAT_1:sch 2(Lm10, Lm11);

theorem :: SEQ_4:140

for v being FinSequence of REAL ex v1 being FinSequence of REAL st

( rng v1 = rng v & len v1 = card (rng v) & v1 is increasing ) by Lm12;

( rng v1 = rng v & len v1 = card (rng v) & v1 is increasing ) by Lm12;

defpred S

v1 = v2;

Lm13: S

proof end;

Lm14: for n being Nat st S

S

proof end;

Lm15: for n being Nat holds S

from NAT_1:sch 2(Lm13, Lm14);

theorem :: SEQ_4:141

for v1, v2 being FinSequence of REAL st len v1 = len v2 & rng v1 = rng v2 & v1 is increasing & v2 is increasing holds

v1 = v2 by Lm15;

v1 = v2 by Lm15;

definition

let v be FinSequence of REAL ;

ex b_{1} being increasing FinSequence of REAL st

( rng b_{1} = rng v & len b_{1} = card (rng v) )

for b_{1}, b_{2} being increasing FinSequence of REAL st rng b_{1} = rng v & len b_{1} = card (rng v) & rng b_{2} = rng v & len b_{2} = card (rng v) holds

b_{1} = b_{2}
by Lm15;

end;
func Incr v -> increasing FinSequence of REAL means :Def21: :: SEQ_4:def 21

( rng it = rng v & len it = card (rng v) );

existence ( rng it = rng v & len it = card (rng v) );

ex b

( rng b

proof end;

uniqueness for b

b

:: deftheorem Def21 defines Incr SEQ_4:def 21 :

for v being FinSequence of REAL

for b_{2} being increasing FinSequence of REAL holds

( b_{2} = Incr v iff ( rng b_{2} = rng v & len b_{2} = card (rng v) ) );

for v being FinSequence of REAL

for b

( b

:: from SPRECT_1, 2011.04.24, A.T

registration

ex b_{1} being Subset of REAL st

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

cluster non empty complex-membered ext-real-membered real-membered bounded_below bounded_above for Element of bool REAL;

existence ex b

( not b

proof 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))

proof end;

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))

proof end;

:: from TOPMETR3, 2011.04.24, A.T

theorem :: SEQ_4:144

for R being non empty Subset of REAL

for r0 being Real st ( for r being Real st r in R holds

r <= r0 ) holds

upper_bound R <= r0

for r0 being Real st ( for r being Real st r in R holds

r <= r0 ) holds

upper_bound R <= r0

proof end;

:: Theorems about the Convergence and the Limit

::