begin
definition
canceled;
end;
:: deftheorem LOPBAN_3:def 1 :
canceled;
theorem Th1:
:: deftheorem Def2 defines summable LOPBAN_3:def 2 :
:: deftheorem defines Sum LOPBAN_3:def 3 :
:: deftheorem Def4 defines norm_summable LOPBAN_3:def 4 :
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th11:
theorem Th12:
theorem
canceled;
theorem
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 Th31:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
begin
theorem Th43:
:: deftheorem LOPBAN_3:def 5 :
canceled;
:: deftheorem LOPBAN_3:def 6 :
canceled;
:: deftheorem LOPBAN_3:def 7 :
canceled;
:: deftheorem Def8 defines invertible LOPBAN_3:def 8 :
:: deftheorem defines * LOPBAN_3:def 9 :
:: deftheorem defines * LOPBAN_3:def 10 :
:: deftheorem defines * LOPBAN_3:def 11 :
:: deftheorem Def12 defines " LOPBAN_3:def 12 :
:: deftheorem Def13 defines GeoSeq LOPBAN_3:def 13 :
:: deftheorem defines #N LOPBAN_3:def 14 :
theorem
theorem Th45:
theorem
Lm1:
for X being RealNormSpace
for x being Point of st ( for e being Real st e > 0 holds
||.x.|| < e ) holds
x = 0. X
Lm2:
for X being RealNormSpace
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 RealNormSpace
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