begin
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 ) & ( 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
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 ) & ( 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
begin
begin
Lm3:
for c, c9 being Element of COMPLEX holds (multcomplex [;] (c,(id COMPLEX))) . c9 = c * c9
Lm4:
for n being Element of NAT
for z being Element of COMPLEX n holds dom z = Seg n
Lm5:
for n being Element of NAT holds - (0c n) = 0c n
Lm6:
for n being Element of NAT
for z1, z, z2 being Element of COMPLEX n st z1 + z = z2 + z holds
z1 = z2
begin
defpred S1[ Nat] means for R being finite Subset of REAL st R <> {} & card R = $1 holds
( R is bounded_above & upper_bound R in R & R is bounded_below & lower_bound R in R );
Lm7:
S1[ 0 ]
;
Lm8:
for n being Element of NAT st S1[n] holds
S1[n + 1]
Lm9:
for n being Element of NAT holds S1[n]
from NAT_1:sch 1(Lm7, Lm8);
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 & len v1 = card (rng v) & v1 is increasing );
Lm10:
S2[ 0 ]
Lm11:
for n being Element of NAT st S2[n] holds
S2[n + 1]
Lm12:
for n being Element of NAT holds S2[n]
from NAT_1:sch 1(Lm10, Lm11);
defpred S3[ Element of NAT ] means for v1, v2 being FinSequence of REAL st len v1 = $1 & len v2 = $1 & rng v1 = rng v2 & v1 is increasing & v2 is increasing holds
v1 = v2;
Lm13:
S3[ 0 ]
Lm14:
for n being Element of NAT st S3[n] holds
S3[n + 1]
Lm15:
for n being Element of NAT holds S3[n]
from NAT_1:sch 1(Lm13, Lm14);
:: Theorems about the Convergence and the Limit
::