:: BHSP_7  semantic presentation begin  









theorem :: BHSP_7:1 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bhsp_1 :::"RealUnitarySpace":::)  (Bool  "for" (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "L")) "being"   ($#m1_subset_1 :::"Functional":::) "of" (Set (Var "X")) "holds"   (Bool  "("  (Bool (Set (Var "Y"))  ($#r1_bhsp_6 :::"is_summable_set_by"::: )  (Set (Var "L"))) "iff" (Bool  "for" (Set (Var "e")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "e")))) "holds"  (Bool  "ex" (Set (Var "Y0")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st"  (Bool  "("  (Bool (Bool  "not" (Set (Var "Y0")) "is"   ($#v1_xboole_0 :::"empty"::: )  )) & (Bool (Set (Var "Y0"))  ($#r1_tarski :::"c="::: )  (Set (Var "Y"))) & (Bool  "("   "for" (Set (Var "Y1")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Bool  "not" (Set (Var "Y1")) "is"   ($#v1_xboole_0 :::"empty"::: )  )) & (Bool (Set (Var "Y1"))  ($#r1_tarski :::"c="::: )  (Set (Var "Y"))) & (Bool (Set (Var "Y0"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "Y1")))) "holds"  (Bool (Set   ($#k18_complex1 :::"abs"::: )  (Set  "("  ($#k5_bhsp_5 :::"setopfunc"::: )   "(" (Set (Var "Y1")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "X"))) "," (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set (Var "L")) "," (Set  ($#k33_binop_2 :::"addreal"::: ) ) ")"  ")" ))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "e")))  ")" )  ")" )))  ")" )))) ; 
 
theorem :: BHSP_7:2 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bhsp_1 :::"RealUnitarySpace":::)  "st" (Bool (Bool (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" (Set (Var "X"))) "is"   ($#v1_binop_1 :::"commutative"::: )  ) & (Bool (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" (Set (Var "X"))) "is"   ($#v2_binop_1 :::"associative"::: )  ) & (Bool (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" (Set (Var "X"))) "is"   ($#v1_setwiseo :::"having_a_unity"::: )  )) "holds"  (Bool  "for" (Set (Var "S")) "being"   ($#v1_finset_1 :::"finite"::: )     ($#m1_bhsp_5 :::"OrthogonalFamily"::: )   "of" (Set (Var "X"))  "st" (Bool (Bool (Bool  "not" (Set (Var "S")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "holds"  (Bool  "for" (Set (Var "I")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "X"))) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "X")))  "st" (Bool (Bool (Set (Var "S"))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "I")))) & (Bool  "("   "for" (Set (Var "y")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "S")))) "holds"  (Bool (Set (Set (Var "I"))  ($#k3_funct_2 :::"."::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Var "y")))  ")" )) "holds"  (Bool  "for" (Set (Var "H")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "X"))) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "S"))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "H")))) & (Bool  "("   "for" (Set (Var "y")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "S")))) "holds"  (Bool (Set (Set (Var "H"))  ($#k3_funct_2 :::"."::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "y"))  ($#k2_bhsp_1 :::".|."::: )  (Set (Var "y"))))  ")" )) "holds"  (Bool (Set (Set  "("  ($#k5_bhsp_5 :::"setopfunc"::: )   "(" (Set (Var "S")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "X"))) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "X"))) "," (Set (Var "I")) "," (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" (Set (Var "X"))) ")"  ")" )  ($#k2_bhsp_1 :::".|."::: )  (Set  "("  ($#k5_bhsp_5 :::"setopfunc"::: )   "(" (Set (Var "S")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "X"))) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "X"))) "," (Set (Var "I")) "," (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" (Set (Var "X"))) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k5_bhsp_5 :::"setopfunc"::: )   "(" (Set (Var "S")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "X"))) "," (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set (Var "H")) "," (Set  ($#k33_binop_2 :::"addreal"::: ) ) ")" )))))) ; 
 
theorem :: BHSP_7:3 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bhsp_1 :::"RealUnitarySpace":::)  "st" (Bool (Bool (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" (Set (Var "X"))) "is"   ($#v1_binop_1 :::"commutative"::: )  ) & (Bool (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" (Set (Var "X"))) "is"   ($#v2_binop_1 :::"associative"::: )  ) & (Bool (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" (Set (Var "X"))) "is"   ($#v1_setwiseo :::"having_a_unity"::: )  )) "holds"  (Bool  "for" (Set (Var "S")) "being"   ($#v1_finset_1 :::"finite"::: )     ($#m1_bhsp_5 :::"OrthogonalFamily"::: )   "of" (Set (Var "X"))  "st" (Bool (Bool (Bool  "not" (Set (Var "S")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "holds"  (Bool  "for" (Set (Var "H")) "being"   ($#m1_subset_1 :::"Functional":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "S"))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "H")))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "S")))) "holds"  (Bool (Set (Set (Var "H"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k2_bhsp_1 :::".|."::: )  (Set (Var "x"))))  ")" )) "holds"  (Bool (Set (Set  "("  ($#k1_bhsp_6 :::"setsum"::: )  (Set (Var "S")) ")" )  ($#k2_bhsp_1 :::".|."::: )  (Set  "("  ($#k1_bhsp_6 :::"setsum"::: )  (Set (Var "S")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k5_bhsp_5 :::"setopfunc"::: )   "(" (Set (Var "S")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "X"))) "," (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set (Var "H")) "," (Set  ($#k33_binop_2 :::"addreal"::: ) ) ")" ))))) ; 
 
theorem :: BHSP_7:4 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bhsp_1 :::"RealUnitarySpace":::)  (Bool  "for" (Set (Var "Y")) "being"    ($#m1_bhsp_5 :::"OrthogonalFamily"::: )   "of" (Set (Var "X"))  (Bool  "for" (Set (Var "Z")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "Z")) "is"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")))) "holds"  (Bool (Set (Var "Z")) "is"    ($#m1_bhsp_5 :::"OrthogonalFamily"::: )   "of" (Set (Var "X")))))) ; 
 
theorem :: BHSP_7:5 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bhsp_1 :::"RealUnitarySpace":::)  (Bool  "for" (Set (Var "Y")) "being"    ($#m2_bhsp_5 :::"OrthonormalFamily"::: )   "of" (Set (Var "X"))  (Bool  "for" (Set (Var "Z")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "Z")) "is"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")))) "holds"  (Bool (Set (Var "Z")) "is"    ($#m2_bhsp_5 :::"OrthonormalFamily"::: )   "of" (Set (Var "X")))))) ; 
 begin  
theorem :: BHSP_7:6 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bhsp_1 :::"RealHilbertSpace":::)  "st" (Bool (Bool (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" (Set (Var "X"))) "is"   ($#v1_binop_1 :::"commutative"::: )  ) & (Bool (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" (Set (Var "X"))) "is"   ($#v2_binop_1 :::"associative"::: )  ) & (Bool (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" (Set (Var "X"))) "is"   ($#v1_setwiseo :::"having_a_unity"::: )  )) "holds"  (Bool  "for" (Set (Var "S")) "being"    ($#m2_bhsp_5 :::"OrthonormalFamily"::: )   "of" (Set (Var "X"))  (Bool  "for" (Set (Var "H")) "being"   ($#m1_subset_1 :::"Functional":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "S"))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "H")))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "S")))) "holds"  (Bool (Set (Set (Var "H"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k2_bhsp_1 :::".|."::: )  (Set (Var "x"))))  ")" )) "holds"  (Bool  "("  (Bool (Set (Var "S")) "is"   ($#v1_bhsp_6 :::"summable_set"::: )  ) "iff" (Bool (Set (Var "S"))  ($#r1_bhsp_6 :::"is_summable_set_by"::: )  (Set (Var "H")))  ")" )))) ; 
 
theorem :: BHSP_7:7 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bhsp_1 :::"RealUnitarySpace":::)  (Bool  "for" (Set (Var "S")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "S")) "is"   ($#v1_bhsp_6 :::"summable_set"::: )  )) "holds"  (Bool  "for" (Set (Var "e")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "e")))) "holds"  (Bool  "ex" (Set (Var "Y0")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st"  (Bool  "("  (Bool (Bool  "not" (Set (Var "Y0")) "is"   ($#v1_xboole_0 :::"empty"::: )  )) & (Bool (Set (Var "Y0"))  ($#r1_tarski :::"c="::: )  (Set (Var "S"))) & (Bool  "("   "for" (Set (Var "Y1")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "Y0"))  ($#r1_tarski :::"c="::: )  (Set (Var "Y1"))) & (Bool (Set (Var "Y1"))  ($#r1_tarski :::"c="::: )  (Set (Var "S")))) "holds"  (Bool (Set   ($#k18_complex1 :::"abs"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k2_bhsp_6 :::"sum"::: )  (Set (Var "S")) ")" )  ($#k2_bhsp_1 :::".|."::: )  (Set  "("  ($#k2_bhsp_6 :::"sum"::: )  (Set (Var "S")) ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set  "("  ($#k1_bhsp_6 :::"setsum"::: )  (Set (Var "Y1")) ")" )  ($#k2_bhsp_1 :::".|."::: )  (Set  "("  ($#k1_bhsp_6 :::"setsum"::: )  (Set (Var "Y1")) ")" ) ")" ) ")" ))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "e")))  ")" )  ")" ))))) ; 
 
theorem :: BHSP_7:8 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bhsp_1 :::"RealHilbertSpace":::)  "st" (Bool (Bool (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" (Set (Var "X"))) "is"   ($#v1_binop_1 :::"commutative"::: )  ) & (Bool (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" (Set (Var "X"))) "is"   ($#v2_binop_1 :::"associative"::: )  ) & (Bool (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" (Set (Var "X"))) "is"   ($#v1_setwiseo :::"having_a_unity"::: )  )) "holds"  (Bool  "for" (Set (Var "S")) "being"    ($#m2_bhsp_5 :::"OrthonormalFamily"::: )   "of" (Set (Var "X"))  (Bool  "for" (Set (Var "H")) "being"   ($#m1_subset_1 :::"Functional":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "S"))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "H")))) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "S")))) "holds"  (Bool (Set (Set (Var "H"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k2_bhsp_1 :::".|."::: )  (Set (Var "x"))))  ")" ) & (Bool (Set (Var "S")) "is"   ($#v1_bhsp_6 :::"summable_set"::: )  )) "holds"  (Bool (Set (Set  "("  ($#k2_bhsp_6 :::"sum"::: )  (Set (Var "S")) ")" )  ($#k2_bhsp_1 :::".|."::: )  (Set  "("  ($#k2_bhsp_6 :::"sum"::: )  (Set (Var "S")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k3_bhsp_6 :::"sum_byfunc"::: )   "(" (Set (Var "S")) "," (Set (Var "H")) ")" ))))) ;