begin
theorem Th1:
:: deftheorem CLOPBAN3:def 1 :
canceled;
:: deftheorem Def2 defines summable CLOPBAN3:def 2 :
:: deftheorem defines Sum CLOPBAN3:def 3 :
:: deftheorem Def4 defines norm_summable CLOPBAN3:def 4 :
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th10:
theorem Th11:
theorem
canceled;
theorem
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
theorem Th26:
theorem Th27:
theorem Th28:
theorem Th29:
theorem Th30:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
begin
theorem Th42:
:: deftheorem CLOPBAN3:def 5 :
canceled;
:: deftheorem CLOPBAN3:def 6 :
canceled;
:: deftheorem CLOPBAN3:def 7 :
canceled;
:: deftheorem defines * CLOPBAN3:def 8 :
:: deftheorem defines * CLOPBAN3:def 9 :
:: deftheorem defines * CLOPBAN3:def 10 :
:: deftheorem CLOPBAN3:def 11 :
canceled;
:: deftheorem Def12 defines GeoSeq CLOPBAN3:def 12 :
:: deftheorem defines #N CLOPBAN3:def 13 :
theorem
theorem Th44:
theorem
Lm1:
for X being ComplexNormSpace
for x being Point of st ( for e being Real st e > 0 holds
||.x.|| < e ) holds
x = 0. X
Lm2:
for X being ComplexNormSpace
for x, y being Point of st ( for e being Real st e > 0 holds
||.(x - y).|| < e ) holds
x = y
Lm3:
for X being ComplexNormSpace
for x, y being Point of
for seq being Real_Sequence st seq is convergent & lim seq = 0 & ( for n being Element of NAT holds ||.(x - y).|| <= seq . n ) holds
x = y
theorem