begin
theorem Th1:
theorem Th2:
begin
:: deftheorem Def1 defines *' COMSEQ_2:def 1 :
:: deftheorem Def2 defines *' COMSEQ_2:def 2 :
theorem
theorem
theorem
theorem
theorem
begin
:: deftheorem Def3 defines bounded COMSEQ_2:def 3 :
reconsider sc = NAT --> 0c as Complex_Sequence ;
Lm1:
for n being Element of NAT holds sc . n = 0c
by FUNCOP_1:13;
theorem Th8:
begin
:: deftheorem Def4 defines convergent COMSEQ_2:def 4 :
:: deftheorem Def5 defines lim COMSEQ_2:def 5 :
theorem Th9:
theorem Th10:
reconsider cs = NAT --> 0 as Real_Sequence by FUNCOP_1:57;
theorem Th11:
theorem Th12:
begin
theorem Th13:
theorem Th14:
theorem
theorem
theorem
theorem Th18:
theorem
theorem
theorem
theorem Th22:
theorem
theorem
theorem Th25:
theorem Th26:
theorem
theorem
theorem Th29:
theorem Th30:
theorem
theorem
theorem Th33:
theorem Th34:
theorem Th35:
theorem
theorem
theorem Th38:
theorem Th39:
theorem
theorem
theorem Th42:
theorem Th43:
theorem
theorem