:: BHSP_3  semantic presentation begin  




































definitionlet "X" be   ($#l1_bhsp_1 :::"RealUnitarySpace":::); let "seq" be   ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "X")); attr "seq" is  :::"Cauchy":::  means :: BHSP_3:def 1 (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "ex" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Set (Var "k"))) & (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::">="::: )  (Set (Var "k")))) "holds"  (Bool (Set   ($#k4_bhsp_1 :::"dist"::: )   "(" (Set  "(" "seq"  ($#k1_normsp_1 :::"."::: )  (Set (Var "n")) ")" ) "," (Set  "(" "seq"  ($#k1_normsp_1 :::"."::: )  (Set (Var "m")) ")" ) ")" )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r")))))); end; 





:: deftheorem    defines :::"Cauchy"::: BHSP_3:def 1 :  (Bool  "for" (Set (Var "X")) "being"   ($#l1_bhsp_1 :::"RealUnitarySpace":::)  (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds"   (Bool  "("  (Bool (Set (Var "seq")) "is"   ($#v1_bhsp_3 :::"Cauchy"::: )  ) "iff" (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "ex" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Set (Var "k"))) & (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::">="::: )  (Set (Var "k")))) "holds"  (Bool (Set   ($#k4_bhsp_1 :::"dist"::: )   "(" (Set  "(" (Set (Var "seq"))  ($#k1_normsp_1 :::"."::: )  (Set (Var "n")) ")" ) "," (Set  "(" (Set (Var "seq"))  ($#k1_normsp_1 :::"."::: )  (Set (Var "m")) ")" ) ")" )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r"))))))  ")" ))); 
 
theorem :: BHSP_3:1 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bhsp_1 :::"RealUnitarySpace":::)  (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "seq")) "is"   ($#v3_funct_1 :::"constant"::: )  )) "holds"  (Bool (Set (Var "seq")) "is"   ($#v1_bhsp_3 :::"Cauchy"::: )  ))) ; 
 
theorem :: BHSP_3:2 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bhsp_1 :::"RealUnitarySpace":::)  (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds"   (Bool  "("  (Bool (Set (Var "seq")) "is"   ($#v1_bhsp_3 :::"Cauchy"::: )  ) "iff" (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "ex" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Set (Var "k"))) & (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::">="::: )  (Set (Var "k")))) "holds"  (Bool (Set  ($#k3_bhsp_1 :::"||."::: ) (Set  "(" (Set  "(" (Set (Var "seq"))  ($#k1_normsp_1 :::"."::: )  (Set (Var "n")) ")" )  ($#k5_algstr_0 :::"-"::: )  (Set  "(" (Set (Var "seq"))  ($#k1_normsp_1 :::"."::: )  (Set (Var "m")) ")" ) ")" ) ($#k3_bhsp_1 :::".||"::: ) )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r"))))))  ")" ))) ; 
 
theorem :: BHSP_3:3 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bhsp_1 :::"RealUnitarySpace":::)  (Bool  "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "seq1")) "is"   ($#v1_bhsp_3 :::"Cauchy"::: )  ) & (Bool (Set (Var "seq2")) "is"   ($#v1_bhsp_3 :::"Cauchy"::: )  )) "holds"  (Bool (Set (Set (Var "seq1"))  ($#k6_bhsp_1 :::"+"::: )  (Set (Var "seq2"))) "is"   ($#v1_bhsp_3 :::"Cauchy"::: )  ))) ; 
 
theorem :: BHSP_3:4 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bhsp_1 :::"RealUnitarySpace":::)  (Bool  "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "seq1")) "is"   ($#v1_bhsp_3 :::"Cauchy"::: )  ) & (Bool (Set (Var "seq2")) "is"   ($#v1_bhsp_3 :::"Cauchy"::: )  )) "holds"  (Bool (Set (Set (Var "seq1"))  ($#k3_normsp_1 :::"-"::: )  (Set (Var "seq2"))) "is"   ($#v1_bhsp_3 :::"Cauchy"::: )  ))) ; 
 
theorem :: BHSP_3:5 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bhsp_1 :::"RealUnitarySpace":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "seq")) "is"   ($#v1_bhsp_3 :::"Cauchy"::: )  )) "holds"  (Bool (Set (Set (Var "a"))  ($#k5_normsp_1 :::"*"::: )  (Set (Var "seq"))) "is"   ($#v1_bhsp_3 :::"Cauchy"::: )  )))) ; 
 
theorem :: BHSP_3:6 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bhsp_1 :::"RealUnitarySpace":::)  (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "seq")) "is"   ($#v1_bhsp_3 :::"Cauchy"::: )  )) "holds"  (Bool (Set   ($#k5_vfunct_1 :::"-"::: )  (Set (Var "seq"))) "is"   ($#v1_bhsp_3 :::"Cauchy"::: )  ))) ; 
 
theorem :: BHSP_3:7 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bhsp_1 :::"RealUnitarySpace":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "seq")) "is"   ($#v1_bhsp_3 :::"Cauchy"::: )  )) "holds"  (Bool (Set (Set (Var "seq"))  ($#k5_bhsp_1 :::"+"::: )  (Set (Var "x"))) "is"   ($#v1_bhsp_3 :::"Cauchy"::: )  )))) ; 
 
theorem :: BHSP_3:8 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bhsp_1 :::"RealUnitarySpace":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "seq")) "is"   ($#v1_bhsp_3 :::"Cauchy"::: )  )) "holds"  (Bool (Set (Set (Var "seq"))  ($#k4_normsp_1 :::"-"::: )  (Set (Var "x"))) "is"   ($#v1_bhsp_3 :::"Cauchy"::: )  )))) ; 
 
theorem :: BHSP_3:9 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bhsp_1 :::"RealUnitarySpace":::)  (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "seq")) "is"   ($#v1_bhsp_2 :::"convergent"::: )  )) "holds"  (Bool (Set (Var "seq")) "is"   ($#v1_bhsp_3 :::"Cauchy"::: )  ))) ; 
 definitionlet "X" be   ($#l1_bhsp_1 :::"RealUnitarySpace":::); let "seq1", "seq2" be   ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "X")); pred "seq1" :::"is_compared_to"::: "seq2" means :: BHSP_3:def 2 (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "ex" (Set (Var "m")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Set (Var "m")))) "holds"  (Bool (Set   ($#k4_bhsp_1 :::"dist"::: )   "(" (Set  "(" "seq1"  ($#k1_normsp_1 :::"."::: )  (Set (Var "n")) ")" ) "," (Set  "(" "seq2"  ($#k1_normsp_1 :::"."::: )  (Set (Var "n")) ")" ) ")" )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r")))))); end; 






:: deftheorem    defines :::"is_compared_to"::: BHSP_3:def 2 :  (Bool  "for" (Set (Var "X")) "being"   ($#l1_bhsp_1 :::"RealUnitarySpace":::)  (Bool  "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds"   (Bool  "("  (Bool (Set (Var "seq1"))  ($#r1_bhsp_3 :::"is_compared_to"::: )  (Set (Var "seq2"))) "iff" (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "ex" (Set (Var "m")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Set (Var "m")))) "holds"  (Bool (Set   ($#k4_bhsp_1 :::"dist"::: )   "(" (Set  "(" (Set (Var "seq1"))  ($#k1_normsp_1 :::"."::: )  (Set (Var "n")) ")" ) "," (Set  "(" (Set (Var "seq2"))  ($#k1_normsp_1 :::"."::: )  (Set (Var "n")) ")" ) ")" )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r"))))))  ")" ))); 
 
theorem :: BHSP_3:10 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bhsp_1 :::"RealUnitarySpace":::)  (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Var "seq"))  ($#r1_bhsp_3 :::"is_compared_to"::: )  (Set (Var "seq"))))) ; 
 
theorem :: BHSP_3:11 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bhsp_1 :::"RealUnitarySpace":::)  (Bool  "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "seq1"))  ($#r1_bhsp_3 :::"is_compared_to"::: )  (Set (Var "seq2")))) "holds"  (Bool (Set (Var "seq2"))  ($#r1_bhsp_3 :::"is_compared_to"::: )  (Set (Var "seq1"))))) ; 
 definitionlet "X" be   ($#l1_bhsp_1 :::"RealUnitarySpace":::); let "seq1", "seq2" be   ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "X")); :: original: :::"is_compared_to"::: redefine pred "seq1" :::"is_compared_to"::: "seq2"; reflexivity  
(Bool  "for" (Set (Var "seq1")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "X")) "holds"  (Bool ((Set (Const "X")) "," (Set (Var "b1")) "," (Set (Var "b1")))))
 ; symmetry  
(Bool  "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "X"))  "st" (Bool (Bool ((Set (Const "X")) "," (Set (Var "b1")) "," (Set (Var "b2"))))) "holds"  (Bool ((Set (Const "X")) "," (Set (Var "b2")) "," (Set (Var "b1")))))
 ; end; 
theorem :: BHSP_3:12 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bhsp_1 :::"RealUnitarySpace":::)  (Bool  "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "," (Set (Var "seq3")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "seq1"))  ($#r2_bhsp_3 :::"is_compared_to"::: )  (Set (Var "seq2"))) & (Bool (Set (Var "seq2"))  ($#r2_bhsp_3 :::"is_compared_to"::: )  (Set (Var "seq3")))) "holds"  (Bool (Set (Var "seq1"))  ($#r2_bhsp_3 :::"is_compared_to"::: )  (Set (Var "seq3"))))) ; 
 
theorem :: BHSP_3:13 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bhsp_1 :::"RealUnitarySpace":::)  (Bool  "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds"   (Bool  "("  (Bool (Set (Var "seq1"))  ($#r2_bhsp_3 :::"is_compared_to"::: )  (Set (Var "seq2"))) "iff" (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "ex" (Set (Var "m")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Set (Var "m")))) "holds"  (Bool (Set  ($#k3_bhsp_1 :::"||."::: ) (Set  "(" (Set  "(" (Set (Var "seq1"))  ($#k1_normsp_1 :::"."::: )  (Set (Var "n")) ")" )  ($#k5_algstr_0 :::"-"::: )  (Set  "(" (Set (Var "seq2"))  ($#k1_normsp_1 :::"."::: )  (Set (Var "n")) ")" ) ")" ) ($#k3_bhsp_1 :::".||"::: ) )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r"))))))  ")" ))) ; 
 
theorem :: BHSP_3:14 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bhsp_1 :::"RealUnitarySpace":::)  (Bool  "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X"))  "st" (Bool (Bool  "ex" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Set (Var "k")))) "holds"  (Bool (Set (Set (Var "seq1"))  ($#k1_normsp_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "seq2"))  ($#k1_normsp_1 :::"."::: )  (Set (Var "n"))))))) "holds"  (Bool (Set (Var "seq1"))  ($#r2_bhsp_3 :::"is_compared_to"::: )  (Set (Var "seq2"))))) ; 
 
theorem :: BHSP_3:15 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bhsp_1 :::"RealUnitarySpace":::)  (Bool  "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "seq1")) "is"   ($#v1_bhsp_3 :::"Cauchy"::: )  ) & (Bool (Set (Var "seq1"))  ($#r2_bhsp_3 :::"is_compared_to"::: )  (Set (Var "seq2")))) "holds"  (Bool (Set (Var "seq2")) "is"   ($#v1_bhsp_3 :::"Cauchy"::: )  ))) ; 
 
theorem :: BHSP_3:16 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bhsp_1 :::"RealUnitarySpace":::)  (Bool  "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "seq1")) "is"   ($#v1_bhsp_2 :::"convergent"::: )  ) & (Bool (Set (Var "seq1"))  ($#r2_bhsp_3 :::"is_compared_to"::: )  (Set (Var "seq2")))) "holds"  (Bool (Set (Var "seq2")) "is"   ($#v1_bhsp_2 :::"convergent"::: )  ))) ; 
 
theorem :: BHSP_3:17 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bhsp_1 :::"RealUnitarySpace":::)  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "seq1")) "is"   ($#v1_bhsp_2 :::"convergent"::: )  ) & (Bool (Set   ($#k1_bhsp_2 :::"lim"::: )  (Set (Var "seq1")))  ($#r1_hidden :::"="::: )  (Set (Var "g"))) & (Bool (Set (Var "seq1"))  ($#r2_bhsp_3 :::"is_compared_to"::: )  (Set (Var "seq2")))) "holds"  (Bool  "("  (Bool (Set (Var "seq2")) "is"   ($#v1_bhsp_2 :::"convergent"::: )  ) & (Bool (Set   ($#k1_bhsp_2 :::"lim"::: )  (Set (Var "seq2")))  ($#r1_hidden :::"="::: )  (Set (Var "g")))  ")" )))) ; 
 definitionlet "X" be   ($#l1_bhsp_1 :::"RealUnitarySpace":::); let "seq" be   ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "X")); attr "seq" is  :::"bounded":::  means :: BHSP_3:def 3 (Bool  "ex" (Set (Var "M")) "being"   ($#m1_subset_1 :::"Real":::) "st"  (Bool  "("  (Bool (Set (Var "M"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool  "("   "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set  ($#k3_bhsp_1 :::"||."::: ) (Set  "(" "seq"  ($#k1_normsp_1 :::"."::: )  (Set (Var "n")) ")" ) ($#k3_bhsp_1 :::".||"::: ) )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "M")))  ")" )  ")" )); end; 





:: deftheorem    defines :::"bounded"::: BHSP_3:def 3 :  (Bool  "for" (Set (Var "X")) "being"   ($#l1_bhsp_1 :::"RealUnitarySpace":::)  (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds"   (Bool  "("  (Bool (Set (Var "seq")) "is"   ($#v2_bhsp_3 :::"bounded"::: )  ) "iff" (Bool  "ex" (Set (Var "M")) "being"   ($#m1_subset_1 :::"Real":::) "st"  (Bool  "("  (Bool (Set (Var "M"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool  "("   "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set  ($#k3_bhsp_1 :::"||."::: ) (Set  "(" (Set (Var "seq"))  ($#k1_normsp_1 :::"."::: )  (Set (Var "n")) ")" ) ($#k3_bhsp_1 :::".||"::: ) )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "M")))  ")" )  ")" ))  ")" ))); 
 
theorem :: BHSP_3:18 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bhsp_1 :::"RealUnitarySpace":::)  (Bool  "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "seq1")) "is"   ($#v2_bhsp_3 :::"bounded"::: )  ) & (Bool (Set (Var "seq2")) "is"   ($#v2_bhsp_3 :::"bounded"::: )  )) "holds"  (Bool (Set (Set (Var "seq1"))  ($#k6_bhsp_1 :::"+"::: )  (Set (Var "seq2"))) "is"   ($#v2_bhsp_3 :::"bounded"::: )  ))) ; 
 
theorem :: BHSP_3:19 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bhsp_1 :::"RealUnitarySpace":::)  (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "seq")) "is"   ($#v2_bhsp_3 :::"bounded"::: )  )) "holds"  (Bool (Set   ($#k5_vfunct_1 :::"-"::: )  (Set (Var "seq"))) "is"   ($#v2_bhsp_3 :::"bounded"::: )  ))) ; 
 
theorem :: BHSP_3:20 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bhsp_1 :::"RealUnitarySpace":::)  (Bool  "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "seq1")) "is"   ($#v2_bhsp_3 :::"bounded"::: )  ) & (Bool (Set (Var "seq2")) "is"   ($#v2_bhsp_3 :::"bounded"::: )  )) "holds"  (Bool (Set (Set (Var "seq1"))  ($#k3_normsp_1 :::"-"::: )  (Set (Var "seq2"))) "is"   ($#v2_bhsp_3 :::"bounded"::: )  ))) ; 
 
theorem :: BHSP_3:21 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bhsp_1 :::"RealUnitarySpace":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "seq")) "is"   ($#v2_bhsp_3 :::"bounded"::: )  )) "holds"  (Bool (Set (Set (Var "a"))  ($#k5_normsp_1 :::"*"::: )  (Set (Var "seq"))) "is"   ($#v2_bhsp_3 :::"bounded"::: )  )))) ; 
 
theorem :: BHSP_3:22 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bhsp_1 :::"RealUnitarySpace":::)  (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "seq")) "is"   ($#v3_funct_1 :::"constant"::: )  )) "holds"  (Bool (Set (Var "seq")) "is"   ($#v2_bhsp_3 :::"bounded"::: )  ))) ; 
 
theorem :: BHSP_3:23 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bhsp_1 :::"RealUnitarySpace":::)  (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "m")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) (Bool  "ex" (Set (Var "M")) "being"   ($#m1_subset_1 :::"Real":::) "st"  (Bool  "("  (Bool (Set (Var "M"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool  "("   "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "m")))) "holds"  (Bool (Set  ($#k3_bhsp_1 :::"||."::: ) (Set  "(" (Set (Var "seq"))  ($#k1_normsp_1 :::"."::: )  (Set (Var "n")) ")" ) ($#k3_bhsp_1 :::".||"::: ) )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "M")))  ")" )  ")" ))))) ; 
 
theorem :: BHSP_3:24 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bhsp_1 :::"RealUnitarySpace":::)  (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "seq")) "is"   ($#v1_bhsp_2 :::"convergent"::: )  )) "holds"  (Bool (Set (Var "seq")) "is"   ($#v2_bhsp_3 :::"bounded"::: )  ))) ; 
 
theorem :: BHSP_3:25 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bhsp_1 :::"RealUnitarySpace":::)  (Bool  "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "seq1")) "is"   ($#v2_bhsp_3 :::"bounded"::: )  ) & (Bool (Set (Var "seq1"))  ($#r2_bhsp_3 :::"is_compared_to"::: )  (Set (Var "seq2")))) "holds"  (Bool (Set (Var "seq2")) "is"   ($#v2_bhsp_3 :::"bounded"::: )  ))) ; 
 
theorem :: BHSP_3:26 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bhsp_1 :::"RealUnitarySpace":::)  (Bool  "for" (Set (Var "seq")) "," (Set (Var "seq1")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "seq")) "is"   ($#v2_bhsp_3 :::"bounded"::: )  ) & (Bool (Set (Var "seq1")) "is"    ($#m2_valued_0 :::"subsequence"::: )   "of" (Set (Var "seq")))) "holds"  (Bool (Set (Var "seq1")) "is"   ($#v2_bhsp_3 :::"bounded"::: )  ))) ; 
 
theorem :: BHSP_3:27 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bhsp_1 :::"RealUnitarySpace":::)  (Bool  "for" (Set (Var "seq")) "," (Set (Var "seq1")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "seq")) "is"   ($#v1_bhsp_2 :::"convergent"::: )  ) & (Bool (Set (Var "seq1")) "is"    ($#m2_valued_0 :::"subsequence"::: )   "of" (Set (Var "seq")))) "holds"  (Bool (Set (Var "seq1")) "is"   ($#v1_bhsp_2 :::"convergent"::: )  ))) ; 
 
theorem :: BHSP_3:28 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bhsp_1 :::"RealUnitarySpace":::)  (Bool  "for" (Set (Var "seq1")) "," (Set (Var "seq")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "seq1")) "is"    ($#m2_valued_0 :::"subsequence"::: )   "of" (Set (Var "seq"))) & (Bool (Set (Var "seq")) "is"   ($#v1_bhsp_2 :::"convergent"::: )  )) "holds"  (Bool (Set   ($#k1_bhsp_2 :::"lim"::: )  (Set (Var "seq1")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_bhsp_2 :::"lim"::: )  (Set (Var "seq")))))) ; 
 
theorem :: BHSP_3:29 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bhsp_1 :::"RealUnitarySpace":::)  (Bool  "for" (Set (Var "seq")) "," (Set (Var "seq1")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "seq")) "is"   ($#v1_bhsp_3 :::"Cauchy"::: )  ) & (Bool (Set (Var "seq1")) "is"    ($#m2_valued_0 :::"subsequence"::: )   "of" (Set (Var "seq")))) "holds"  (Bool (Set (Var "seq1")) "is"   ($#v1_bhsp_3 :::"Cauchy"::: )  ))) ; 
 
theorem :: BHSP_3:30 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bhsp_1 :::"RealUnitarySpace":::)  (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "k")) "," (Set (Var "m")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set  "(" (Set (Var "seq"))  ($#k1_valued_0 :::"^\"::: )  (Set (Var "k")) ")" )  ($#k1_valued_0 :::"^\"::: )  (Set (Var "m")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "seq"))  ($#k1_valued_0 :::"^\"::: )  (Set (Var "m")) ")" )  ($#k1_valued_0 :::"^\"::: )  (Set (Var "k"))))))) ; 
 
theorem :: BHSP_3:31 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bhsp_1 :::"RealUnitarySpace":::)  (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "k")) "," (Set (Var "m")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set  "(" (Set (Var "seq"))  ($#k1_valued_0 :::"^\"::: )  (Set (Var "k")) ")" )  ($#k1_valued_0 :::"^\"::: )  (Set (Var "m")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "seq"))  ($#k1_valued_0 :::"^\"::: )  (Set  "(" (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Set (Var "m")) ")" )))))) ; 
 
theorem :: BHSP_3:32 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bhsp_1 :::"RealUnitarySpace":::)  (Bool  "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set  "(" (Set (Var "seq1"))  ($#k6_bhsp_1 :::"+"::: )  (Set (Var "seq2")) ")" )  ($#k1_valued_0 :::"^\"::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "seq1"))  ($#k1_valued_0 :::"^\"::: )  (Set (Var "k")) ")" )  ($#k6_bhsp_1 :::"+"::: )  (Set  "(" (Set (Var "seq2"))  ($#k1_valued_0 :::"^\"::: )  (Set (Var "k")) ")" )))))) ; 
 
theorem :: BHSP_3:33 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bhsp_1 :::"RealUnitarySpace":::)  (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set  "("  ($#k5_vfunct_1 :::"-"::: )  (Set (Var "seq")) ")" )  ($#k1_valued_0 :::"^\"::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set   ($#k5_vfunct_1 :::"-"::: )  (Set  "(" (Set (Var "seq"))  ($#k1_valued_0 :::"^\"::: )  (Set (Var "k")) ")" )))))) ; 
 
theorem :: BHSP_3:34 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bhsp_1 :::"RealUnitarySpace":::)  (Bool  "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set  "(" (Set (Var "seq1"))  ($#k3_normsp_1 :::"-"::: )  (Set (Var "seq2")) ")" )  ($#k1_valued_0 :::"^\"::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "seq1"))  ($#k1_valued_0 :::"^\"::: )  (Set (Var "k")) ")" )  ($#k3_normsp_1 :::"-"::: )  (Set  "(" (Set (Var "seq2"))  ($#k1_valued_0 :::"^\"::: )  (Set (Var "k")) ")" )))))) ; 
 
theorem :: BHSP_3:35 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bhsp_1 :::"RealUnitarySpace":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k5_normsp_1 :::"*"::: )  (Set (Var "seq")) ")" )  ($#k1_valued_0 :::"^\"::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k5_normsp_1 :::"*"::: )  (Set  "(" (Set (Var "seq"))  ($#k1_valued_0 :::"^\"::: )  (Set (Var "k")) ")" ))))))) ; 
 
theorem :: BHSP_3:36 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bhsp_1 :::"RealUnitarySpace":::)  (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "seq")) "is"   ($#v1_bhsp_2 :::"convergent"::: )  )) "holds"  (Bool  "("  (Bool (Set (Set (Var "seq"))  ($#k1_valued_0 :::"^\"::: )  (Set (Var "k"))) "is"   ($#v1_bhsp_2 :::"convergent"::: )  ) & (Bool (Set   ($#k1_bhsp_2 :::"lim"::: )  (Set  "(" (Set (Var "seq"))  ($#k1_valued_0 :::"^\"::: )  (Set (Var "k")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_bhsp_2 :::"lim"::: )  (Set (Var "seq"))))  ")" )))) ; 
 
theorem :: BHSP_3:37 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bhsp_1 :::"RealUnitarySpace":::)  (Bool  "for" (Set (Var "seq")) "," (Set (Var "seq1")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "seq")) "is"   ($#v1_bhsp_2 :::"convergent"::: )  ) & (Bool  "ex" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st" (Bool (Set (Var "seq"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "seq1"))  ($#k1_valued_0 :::"^\"::: )  (Set (Var "k")))))) "holds"  (Bool (Set (Var "seq1")) "is"   ($#v1_bhsp_2 :::"convergent"::: )  ))) ; 
 
theorem :: BHSP_3:38 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bhsp_1 :::"RealUnitarySpace":::)  (Bool  "for" (Set (Var "seq")) "," (Set (Var "seq1")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "seq")) "is"   ($#v1_bhsp_3 :::"Cauchy"::: )  ) & (Bool  "ex" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st" (Bool (Set (Var "seq"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "seq1"))  ($#k1_valued_0 :::"^\"::: )  (Set (Var "k")))))) "holds"  (Bool (Set (Var "seq1")) "is"   ($#v1_bhsp_3 :::"Cauchy"::: )  ))) ; 
 
theorem :: BHSP_3:39 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bhsp_1 :::"RealUnitarySpace":::)  (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "seq")) "is"   ($#v1_bhsp_3 :::"Cauchy"::: )  )) "holds"  (Bool (Set (Set (Var "seq"))  ($#k1_valued_0 :::"^\"::: )  (Set (Var "k"))) "is"   ($#v1_bhsp_3 :::"Cauchy"::: )  )))) ; 
 
theorem :: BHSP_3:40 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bhsp_1 :::"RealUnitarySpace":::)  (Bool  "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "seq1"))  ($#r2_bhsp_3 :::"is_compared_to"::: )  (Set (Var "seq2")))) "holds"  (Bool (Set (Set (Var "seq1"))  ($#k1_valued_0 :::"^\"::: )  (Set (Var "k")))  ($#r2_bhsp_3 :::"is_compared_to"::: )  (Set (Set (Var "seq2"))  ($#k1_valued_0 :::"^\"::: )  (Set (Var "k"))))))) ; 
 
theorem :: BHSP_3:41 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bhsp_1 :::"RealUnitarySpace":::)  (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "seq")) "is"   ($#v2_bhsp_3 :::"bounded"::: )  )) "holds"  (Bool (Set (Set (Var "seq"))  ($#k1_valued_0 :::"^\"::: )  (Set (Var "k"))) "is"   ($#v2_bhsp_3 :::"bounded"::: )  )))) ; 
 
theorem :: BHSP_3:42 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bhsp_1 :::"RealUnitarySpace":::)  (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "seq")) "is"   ($#v3_funct_1 :::"constant"::: )  )) "holds"  (Bool (Set (Set (Var "seq"))  ($#k1_valued_0 :::"^\"::: )  (Set (Var "k"))) "is"   ($#v3_funct_1 :::"constant"::: )  )))) ; 
 definitionlet "X" be   ($#l1_bhsp_1 :::"RealUnitarySpace":::); attr "X" is  :::"complete":::  means :: BHSP_3:def 4 (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"sequence":::) "of" "X"  "st" (Bool (Bool (Set (Var "seq")) "is"   ($#v1_bhsp_3 :::"Cauchy"::: )  )) "holds"  (Bool (Set (Var "seq")) "is"   ($#v1_bhsp_2 :::"convergent"::: )  )); end; 




:: deftheorem    defines :::"complete"::: BHSP_3:def 4 :  (Bool  "for" (Set (Var "X")) "being"   ($#l1_bhsp_1 :::"RealUnitarySpace":::) "holds"   (Bool  "("  (Bool (Set (Var "X")) "is"   ($#v3_bhsp_3 :::"complete"::: )  ) "iff" (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "seq")) "is"   ($#v1_bhsp_3 :::"Cauchy"::: )  )) "holds"  (Bool (Set (Var "seq")) "is"   ($#v1_bhsp_2 :::"convergent"::: )  ))  ")" )); 
 
theorem :: BHSP_3:43 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bhsp_1 :::"RealUnitarySpace":::)  (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "X")) "is"   ($#v3_bhsp_3 :::"complete"::: )  ) & (Bool (Set (Var "seq")) "is"   ($#v1_bhsp_3 :::"Cauchy"::: )  )) "holds"  (Bool (Set (Var "seq")) "is"   ($#v2_bhsp_3 :::"bounded"::: )  ))) ;