begin
deffunc H1( RealUnitarySpace) -> Element of the carrier of $1 = 0. $1;
:: deftheorem Def1 defines convergent BHSP_2:def 1 :
theorem Th1:
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
:: deftheorem Def2 defines lim BHSP_2:def 2 :
theorem Th10:
theorem
theorem
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem
theorem Th19:
:: deftheorem Def3 defines ||. BHSP_2:def 3 :
theorem Th20:
theorem Th21:
theorem Th22:
:: deftheorem Def4 defines dist BHSP_2:def 4 :
theorem Th23:
theorem Th24:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
Lm1:
for X being RealUnitarySpace
for g, x being Point of
for seq being sequence of X st seq is convergent & lim seq = g holds
( ||.(seq + x).|| is convergent & lim ||.(seq + x).|| = ||.(g + x).|| )
theorem Th33:
theorem
theorem
theorem
theorem
theorem
theorem
:: deftheorem defines Ball BHSP_2:def 5 :
:: deftheorem defines cl_Ball BHSP_2:def 6 :
:: deftheorem defines Sphere BHSP_2:def 7 :
theorem Th40:
theorem Th41:
theorem
theorem
theorem
theorem
theorem
theorem Th47:
theorem Th48:
theorem
theorem Th50:
theorem Th51:
theorem
theorem
theorem Th54:
theorem Th55:
theorem