begin
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th8:
theorem Th9:
theorem Th10:
:: deftheorem Def1 defines bounded_above SEQ_4:def 1 :
:: deftheorem Def2 defines bounded_below SEQ_4:def 2 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
canceled;
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
:: deftheorem SEQ_4:def 3 :
canceled;
:: deftheorem Def4 defines upper_bound SEQ_4:def 4 :
:: deftheorem Def5 defines lower_bound SEQ_4:def 5 :
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
theorem
canceled;
theorem
canceled;
theorem Th22:
theorem Th23:
theorem
theorem
theorem Th26:
theorem
theorem
theorem Th29:
theorem Th30:
theorem Th31:
theorem
theorem
theorem
canceled;
theorem Th35:
theorem
theorem Th37:
theorem
theorem
canceled;
theorem Th40:
theorem
theorem
theorem Th43:
theorem Th44:
theorem
theorem
theorem Th47:
theorem Th48:
theorem
theorem
theorem
canceled;
theorem
canceled;
theorem Th53:
theorem
theorem
theorem Th56:
theorem Th57:
theorem
theorem
begin
theorem Th60:
theorem
theorem Th62:
theorem
theorem
theorem
begin
theorem
theorem Th6:
theorem Th7:
theorem Th8:
:: deftheorem defines diffcomplex SEQ_4:def 6 :
theorem
theorem Th15:
:: deftheorem defines multcomplex SEQ_4:def 7 :
Lm1:
for c, c9 being Element of COMPLEX holds (multcomplex [;] c,(id COMPLEX )) . c9 = c * c9
theorem
theorem
:: deftheorem Def6 defines abscomplex SEQ_4:def 8 :
:: deftheorem defines + SEQ_4:def 9 :
:: deftheorem defines - SEQ_4:def 10 :
:: deftheorem defines - SEQ_4:def 11 :
:: deftheorem defines * SEQ_4:def 12 :
:: deftheorem defines abs SEQ_4:def 13 :
:: deftheorem defines COMPLEX SEQ_4:def 14 :
Lm2:
for n being Element of NAT
for z being Element of COMPLEX n holds dom z = Seg n
theorem Th21:
theorem Th24:
:: deftheorem defines 0c SEQ_4:def 15 :
theorem
theorem Th29:
Lm3:
for n being Element of NAT holds - (0c n) = 0c n
theorem
theorem
theorem
theorem
Lm4:
for n being Element of NAT
for z1, z, z2 being Element of COMPLEX n st z1 + z = z2 + z holds
z1 = z2
theorem
theorem Th35:
theorem
theorem
theorem
theorem
theorem Th41:
theorem Th42:
theorem Th43:
theorem Th44:
theorem Th45:
theorem Th46:
theorem
theorem
theorem Th49:
theorem Th50:
theorem Th51:
theorem Th52:
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th59:
theorem Th60:
theorem Th61:
theorem Th62:
:: deftheorem defines |. SEQ_4:def 16 :
theorem Th63:
theorem Th64:
theorem Th65:
theorem
theorem
Lm5:
for i, j being Element of NAT
for t being Element of i -tuples_on REAL st j in Seg i holds
t . j is Real
theorem Th68:
theorem Th69:
theorem
theorem
theorem Th72:
theorem
theorem Th74:
theorem Th75:
:: deftheorem Def15 defines open SEQ_4:def 17 :
:: deftheorem defines closed SEQ_4:def 18 :
theorem
theorem
theorem
theorem
:: deftheorem defines Ball SEQ_4:def 19 :
theorem Th80:
theorem
theorem
:: deftheorem Def18 defines dist SEQ_4:def 20 :
:: deftheorem defines Ball SEQ_4:def 21 :
theorem Th84:
theorem Th85:
theorem Th86:
theorem Th87:
theorem
theorem
theorem Th90:
theorem Th91:
theorem
theorem
:: deftheorem Def20 defines dist SEQ_4:def 22 :
:: deftheorem defines + SEQ_4:def 23 :
theorem Th94:
theorem Th95:
theorem Th96:
theorem Th97:
theorem Th98:
theorem
theorem Th100:
theorem
:: deftheorem defines ComplexOpenSets SEQ_4:def 24 :
theorem
theorem
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 );
Lm1:
S1[ 0 ]
;
Lm2:
for n being Element of NAT st S1[n] holds
S1[n + 1]
Lm3:
for n being Element of NAT holds S1[n]
from NAT_1:sch 1(Lm1, Lm2);
theorem Th1:
theorem
theorem
theorem
theorem
theorem Th19:
theorem Th20:
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 );
Lm4:
S2[ 0 ]
Lm5:
for n being Element of NAT st S2[n] holds
S2[n + 1]
Lm6:
for n being Element of NAT holds S2[n]
from NAT_1:sch 1(Lm4, Lm5);
theorem
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;
Lm7:
S3[ 0 ]
Lm8:
for n being Element of NAT st S3[n] holds
S3[n + 1]
Lm9:
for n being Element of NAT holds S3[n]
from NAT_1:sch 1(Lm7, Lm8);
theorem
:: deftheorem Def2 defines Incr SEQ_4:def 25 :