begin
deffunc H1( RealUnitarySpace) -> Element of the carrier of $1 = 0. $1;
:: deftheorem Def1 defines Cauchy BHSP_3:def 1 :
theorem
theorem
theorem
theorem
theorem Th5:
theorem
theorem Th7:
theorem
theorem
:: deftheorem Def2 defines is_compared_to BHSP_3:def 2 :
theorem Th10:
theorem Th11:
theorem
theorem
theorem
theorem
theorem
theorem
:: deftheorem Def3 defines bounded BHSP_3:def 3 :
theorem Th18:
theorem Th19:
theorem
theorem
theorem
theorem Th23:
theorem Th24:
theorem
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
theorem
canceled;
theorem
theorem
theorem Th38:
theorem Th39:
theorem
theorem
theorem
canceled;
theorem
canceled;
theorem
theorem
canceled;
theorem
theorem
theorem
theorem
theorem
theorem
:: deftheorem BHSP_3:def 4 :
canceled;
:: deftheorem BHSP_3:def 5 :
canceled;
:: deftheorem Def6 defines complete BHSP_3:def 6 :
theorem
canceled;
theorem
:: deftheorem defines Hilbert BHSP_3:def 7 :