begin
deffunc H1( RealUnitarySpace) -> Element of the carrier of $1 = 0. $1;
:: deftheorem Def1 defines Partial_Sums BHSP_4:def 1 :
theorem Th1:
theorem Th2:
theorem Th3:
theorem
theorem
:: deftheorem Def2 defines summable BHSP_4:def 2 :
:: deftheorem defines Sum BHSP_4:def 3 :
theorem
theorem
theorem
theorem Th9:
theorem Th10:
theorem
theorem Th12:
theorem Th13:
theorem
:: deftheorem defines Sum BHSP_4:def 4 :
theorem
canceled;
theorem
theorem Th17:
theorem Th18:
theorem
theorem Th20:
theorem
:: deftheorem defines Sum BHSP_4:def 5 :
theorem
canceled;
theorem
theorem
theorem Th25:
theorem
:: deftheorem BHSP_4:def 6 :
canceled;
:: deftheorem BHSP_4:def 7 :
canceled;
:: deftheorem Def8 defines absolutely_summable BHSP_4:def 8 :
theorem
theorem
theorem
theorem
theorem Th31:
theorem Th32:
theorem
theorem
theorem
theorem
theorem Th37:
theorem
theorem Th39:
theorem
theorem Th41:
theorem
theorem
theorem
:: deftheorem Def9 defines * BHSP_4:def 9 :
theorem
theorem
theorem
theorem Th48:
theorem
theorem Th50:
theorem
theorem
:: deftheorem Def10 defines Cauchy BHSP_4:def 10 :
theorem
theorem Th54:
theorem Th55:
theorem