begin
Lm1:
0c = 0 + (0 * <i> )
;
theorem
theorem Th2:
theorem Th3:
reconsider C = NAT --> 0 as Real_Sequence by FUNCOP_1:57;
Lm2:
for n being Element of NAT holds C . n = 0
by FUNCOP_1:13;
theorem
theorem
theorem
theorem
theorem
theorem
theorem
begin
Lm3:
for seq being Complex_Sequence
for n being Element of NAT holds
( |.(seq . n).| = |.seq.| . n & 0 <= |.seq.| . n )
:: deftheorem Def1 defines GeoSeq COMSEQ_3:def 1 :
:: deftheorem defines #N COMSEQ_3:def 2 :
theorem
:: deftheorem Def3 defines Re COMSEQ_3:def 3 :
:: deftheorem Def4 defines Im COMSEQ_3:def 4 :
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem
theorem
theorem
theorem Th22:
theorem Th23:
:: deftheorem COMSEQ_3:def 5 :
canceled;
:: deftheorem COMSEQ_3:def 6 :
canceled;
:: deftheorem Def7 defines Partial_Sums COMSEQ_3:def 7 :
:: deftheorem defines Sum COMSEQ_3:def 8 :
theorem Th24:
theorem Th25:
theorem Th26:
theorem Th27:
theorem Th28:
theorem Th29:
theorem
theorem Th31:
theorem Th32:
theorem
theorem Th34:
theorem
theorem Th36:
theorem Th37:
begin
theorem Th38:
theorem Th39:
theorem Th40:
theorem Th41:
theorem Th42:
theorem Th43:
theorem Th44:
theorem
theorem Th46:
theorem
theorem
begin
theorem
theorem
canceled;
theorem
:: deftheorem COMSEQ_3:def 9 :
canceled;
:: deftheorem Def10 defines summable COMSEQ_3:def 10 :
set D = NAT --> 0c ;
:: deftheorem Def11 defines absolutely_summable COMSEQ_3:def 11 :
theorem Th52:
theorem Th53:
theorem Th54:
theorem Th55:
theorem Th56:
theorem Th57:
theorem Th58:
theorem Th59:
theorem
theorem
theorem Th62:
theorem Th63:
theorem Th64:
theorem Th65:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem