:: BHSP_6  semantic presentation begin  









definitionlet "X" be   ($#l1_bhsp_1 :::"RealUnitarySpace":::); assume 
(Bool  "("  (Bool (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" (Set (Const "X"))) "is"   ($#v1_binop_1 :::"commutative"::: )  ) & (Bool (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" (Set (Const "X"))) "is"   ($#v2_binop_1 :::"associative"::: )  ) & (Bool (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" (Set (Const "X"))) "is"   ($#v1_setwiseo :::"having_a_unity"::: )  )  ")" )
 ; let "Y" be   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")); func  :::"setsum"::: "Y" ->   ($#m1_subset_1 :::"Element":::) "of" "X" means :: BHSP_6:def 1 (Bool  "ex" (Set (Var "p")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "X") "st"  (Bool  "("  (Bool (Set (Var "p")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) & (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  "Y") & (Bool it  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" "X")  ($#k1_finsop_1 :::""**""::: )  (Set (Var "p"))))  ")" )); end; 







:: deftheorem    defines :::"setsum"::: BHSP_6:def 1 :  (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 "Y")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "b3")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_bhsp_6 :::"setsum"::: )  (Set (Var "Y")))) "iff" (Bool  "ex" (Set (Var "p")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "X"))) "st"  (Bool  "("  (Bool (Set (Var "p")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) & (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Var "Y"))) & (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" (Set (Var "X")))  ($#k1_finsop_1 :::""**""::: )  (Set (Var "p"))))  ")" ))  ")" )))); 
 
theorem :: BHSP_6:1 (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 "Y")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X"))  (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 "Y"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "I")))) & (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "I"))))) "holds"  (Bool (Set (Set (Var "I"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Var "x")))  ")" )) "holds"  (Bool (Set   ($#k1_bhsp_6 :::"setsum"::: )  (Set (Var "Y")))  ($#r1_hidden :::"="::: )  (Set   ($#k5_bhsp_5 :::"setopfunc"::: )   "(" (Set (Var "Y")) "," (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"))) ")" ))))) ; 
 
theorem :: BHSP_6: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 "Y1")) "," (Set (Var "Y2")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "Y1"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "Y2")))) "holds"  (Bool  "for" (Set (Var "Z")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "Z"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "Y1"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "Y2"))))) "holds"  (Bool (Set   ($#k1_bhsp_6 :::"setsum"::: )  (Set (Var "Z")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_bhsp_6 :::"setsum"::: )  (Set (Var "Y1")) ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "("  ($#k1_bhsp_6 :::"setsum"::: )  (Set (Var "Y2")) ")" )))))) ; 
 begin  definitionlet "X" be   ($#l1_bhsp_1 :::"RealUnitarySpace":::); let "Y" be   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")); attr "Y" is  :::"summable_set":::  means :: BHSP_6:def 2 (Bool  "ex" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" "X" "st"  (Bool  "for" (Set (Var "e")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "e"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "ex" (Set (Var "Y0")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" "X" "st"  (Bool  "("  (Bool (Bool  "not" (Set (Var "Y0")) "is"   ($#v1_xboole_0 :::"empty"::: )  )) & (Bool (Set (Var "Y0"))  ($#r1_tarski :::"c="::: )  "Y") & (Bool  "("   "for" (Set (Var "Y1")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" "X"  "st" (Bool (Bool (Set (Var "Y0"))  ($#r1_tarski :::"c="::: )  (Set (Var "Y1"))) & (Bool (Set (Var "Y1"))  ($#r1_tarski :::"c="::: )  "Y")) "holds"  (Bool (Set  ($#k3_bhsp_1 :::"||."::: ) (Set  "(" (Set (Var "x"))  ($#k5_algstr_0 :::"-"::: )  (Set  "("  ($#k1_bhsp_6 :::"setsum"::: )  (Set (Var "Y1")) ")" ) ")" ) ($#k3_bhsp_1 :::".||"::: ) )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "e")))  ")" )  ")" )))); end; 





:: deftheorem    defines :::"summable_set"::: BHSP_6:def 2 :  (Bool  "for" (Set (Var "X")) "being"   ($#l1_bhsp_1 :::"RealUnitarySpace":::)  (Bool  "for" (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds"   (Bool  "("  (Bool (Set (Var "Y")) "is"   ($#v1_bhsp_6 :::"summable_set"::: )  ) "iff" (Bool  "ex" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "st"  (Bool  "for" (Set (Var "e")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "e"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "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 (Set (Var "Y0"))  ($#r1_tarski :::"c="::: )  (Set (Var "Y1"))) & (Bool (Set (Var "Y1"))  ($#r1_tarski :::"c="::: )  (Set (Var "Y")))) "holds"  (Bool (Set  ($#k3_bhsp_1 :::"||."::: ) (Set  "(" (Set (Var "x"))  ($#k5_algstr_0 :::"-"::: )  (Set  "("  ($#k1_bhsp_6 :::"setsum"::: )  (Set (Var "Y1")) ")" ) ")" ) ($#k3_bhsp_1 :::".||"::: ) )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "e")))  ")" )  ")" ))))  ")" ))); 
 definitionlet "X" be   ($#l1_bhsp_1 :::"RealUnitarySpace":::); let "Y" be   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")); assume 
(Bool (Set (Const "Y")) "is"   ($#v1_bhsp_6 :::"summable_set"::: )  )
 ; func  :::"sum"::: "Y" ->   ($#m1_subset_1 :::"Point":::) "of" "X" means :: BHSP_6:def 3 (Bool  "for" (Set (Var "e")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "e"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "ex" (Set (Var "Y0")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" "X" "st"  (Bool  "("  (Bool (Bool  "not" (Set (Var "Y0")) "is"   ($#v1_xboole_0 :::"empty"::: )  )) & (Bool (Set (Var "Y0"))  ($#r1_tarski :::"c="::: )  "Y") & (Bool  "("   "for" (Set (Var "Y1")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" "X"  "st" (Bool (Bool (Set (Var "Y0"))  ($#r1_tarski :::"c="::: )  (Set (Var "Y1"))) & (Bool (Set (Var "Y1"))  ($#r1_tarski :::"c="::: )  "Y")) "holds"  (Bool (Set  ($#k3_bhsp_1 :::"||."::: ) (Set  "(" it  ($#k5_algstr_0 :::"-"::: )  (Set  "("  ($#k1_bhsp_6 :::"setsum"::: )  (Set (Var "Y1")) ")" ) ")" ) ($#k3_bhsp_1 :::".||"::: ) )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "e")))  ")" )  ")" ))); end; 







:: deftheorem    defines :::"sum"::: BHSP_6:def 3 :  (Bool  "for" (Set (Var "X")) "being"   ($#l1_bhsp_1 :::"RealUnitarySpace":::)  (Bool  "for" (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "Y")) "is"   ($#v1_bhsp_6 :::"summable_set"::: )  )) "holds"  (Bool  "for" (Set (Var "b3")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_bhsp_6 :::"sum"::: )  (Set (Var "Y")))) "iff" (Bool  "for" (Set (Var "e")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "e"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "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 (Set (Var "Y0"))  ($#r1_tarski :::"c="::: )  (Set (Var "Y1"))) & (Bool (Set (Var "Y1"))  ($#r1_tarski :::"c="::: )  (Set (Var "Y")))) "holds"  (Bool (Set  ($#k3_bhsp_1 :::"||."::: ) (Set  "(" (Set (Var "b3"))  ($#k5_algstr_0 :::"-"::: )  (Set  "("  ($#k1_bhsp_6 :::"setsum"::: )  (Set (Var "Y1")) ")" ) ")" ) ($#k3_bhsp_1 :::".||"::: ) )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "e")))  ")" )  ")" )))  ")" )))); 
 definitionlet "X" be   ($#l1_bhsp_1 :::"RealUnitarySpace":::); let "L" be   ($#m1_subset_1 :::"linear-Functional":::) "of" (Set (Const "X")); attr "L" is  :::"Lipschitzian":::  means :: BHSP_6:def 4 (Bool  "ex" (Set (Var "K")) "being"   ($#m1_subset_1 :::"Real":::) "st"  (Bool  "("  (Bool (Set (Var "K"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" "X" "holds"  (Bool (Set   ($#k18_complex1 :::"abs"::: )  (Set  "(" "L"  ($#k3_funct_2 :::"."::: )  (Set (Var "x")) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "K"))  ($#k11_binop_2 :::"*"::: )  (Set  ($#k3_bhsp_1 :::"||."::: ) (Set (Var "x")) ($#k3_bhsp_1 :::".||"::: ) )))  ")" )  ")" )); end; 





:: deftheorem    defines :::"Lipschitzian"::: BHSP_6:def 4 :  (Bool  "for" (Set (Var "X")) "being"   ($#l1_bhsp_1 :::"RealUnitarySpace":::)  (Bool  "for" (Set (Var "L")) "being"   ($#m1_subset_1 :::"linear-Functional":::) "of" (Set (Var "X")) "holds"   (Bool  "("  (Bool (Set (Var "L")) "is"   ($#v2_bhsp_6 :::"Lipschitzian"::: )  ) "iff" (Bool  "ex" (Set (Var "K")) "being"   ($#m1_subset_1 :::"Real":::) "st"  (Bool  "("  (Bool (Set (Var "K"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds"  (Bool (Set   ($#k18_complex1 :::"abs"::: )  (Set  "(" (Set (Var "L"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x")) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "K"))  ($#k11_binop_2 :::"*"::: )  (Set  ($#k3_bhsp_1 :::"||."::: ) (Set (Var "x")) ($#k3_bhsp_1 :::".||"::: ) )))  ")" )  ")" ))  ")" ))); 
 definitionlet "X" be   ($#l1_bhsp_1 :::"RealUnitarySpace":::); let "Y" be   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")); attr "Y" is  :::"weakly_summable_set":::  means :: BHSP_6:def 5 (Bool  "ex" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" "X" "st"  (Bool  "for" (Set (Var "L")) "being"   ($#m1_subset_1 :::"linear-Functional":::) "of" "X"  "st" (Bool (Bool (Set (Var "L")) "is"   ($#v2_bhsp_6 :::"Lipschitzian"::: )  )) "holds"  (Bool  "for" (Set (Var "e")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "e"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "ex" (Set (Var "Y0")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" "X" "st"  (Bool  "("  (Bool (Bool  "not" (Set (Var "Y0")) "is"   ($#v1_xboole_0 :::"empty"::: )  )) & (Bool (Set (Var "Y0"))  ($#r1_tarski :::"c="::: )  "Y") & (Bool  "("   "for" (Set (Var "Y1")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" "X"  "st" (Bool (Bool (Set (Var "Y0"))  ($#r1_tarski :::"c="::: )  (Set (Var "Y1"))) & (Bool (Set (Var "Y1"))  ($#r1_tarski :::"c="::: )  "Y")) "holds"  (Bool (Set   ($#k18_complex1 :::"abs"::: )  (Set  "(" (Set (Var "L"))  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "x"))  ($#k5_algstr_0 :::"-"::: )  (Set  "("  ($#k1_bhsp_6 :::"setsum"::: )  (Set (Var "Y1")) ")" ) ")" ) ")" ))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "e")))  ")" )  ")" ))))); end; 





:: deftheorem    defines :::"weakly_summable_set"::: BHSP_6:def 5 :  (Bool  "for" (Set (Var "X")) "being"   ($#l1_bhsp_1 :::"RealUnitarySpace":::)  (Bool  "for" (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds"   (Bool  "("  (Bool (Set (Var "Y")) "is"   ($#v3_bhsp_6 :::"weakly_summable_set"::: )  ) "iff" (Bool  "ex" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "st"  (Bool  "for" (Set (Var "L")) "being"   ($#m1_subset_1 :::"linear-Functional":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "L")) "is"   ($#v2_bhsp_6 :::"Lipschitzian"::: )  )) "holds"  (Bool  "for" (Set (Var "e")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "e"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "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 (Set (Var "Y0"))  ($#r1_tarski :::"c="::: )  (Set (Var "Y1"))) & (Bool (Set (Var "Y1"))  ($#r1_tarski :::"c="::: )  (Set (Var "Y")))) "holds"  (Bool (Set   ($#k18_complex1 :::"abs"::: )  (Set  "(" (Set (Var "L"))  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "x"))  ($#k5_algstr_0 :::"-"::: )  (Set  "("  ($#k1_bhsp_6 :::"setsum"::: )  (Set (Var "Y1")) ")" ) ")" ) ")" ))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "e")))  ")" )  ")" )))))  ")" ))); 
 definitionlet "X" be   ($#l1_bhsp_1 :::"RealUnitarySpace":::); let "Y" be   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")); let "L" be   ($#m1_subset_1 :::"Functional":::) "of" (Set (Const "X")); pred "Y" :::"is_summable_set_by"::: "L" means :: BHSP_6:def 6 (Bool  "ex" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::) "st"  (Bool  "for" (Set (Var "e")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "e"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "ex" (Set (Var "Y0")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" "X" "st"  (Bool  "("  (Bool (Bool  "not" (Set (Var "Y0")) "is"   ($#v1_xboole_0 :::"empty"::: )  )) & (Bool (Set (Var "Y0"))  ($#r1_tarski :::"c="::: )  "Y") & (Bool  "("   "for" (Set (Var "Y1")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" "X"  "st" (Bool (Bool (Set (Var "Y0"))  ($#r1_tarski :::"c="::: )  (Set (Var "Y1"))) & (Bool (Set (Var "Y1"))  ($#r1_tarski :::"c="::: )  "Y")) "holds"  (Bool (Set   ($#k18_complex1 :::"abs"::: )  (Set  "(" (Set (Var "r"))  ($#k10_binop_2 :::"-"::: )  (Set  "("  ($#k5_bhsp_5 :::"setopfunc"::: )   "(" (Set (Var "Y1")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "X") "," (Set  ($#k1_numbers :::"REAL"::: ) ) "," "L" "," (Set  ($#k33_binop_2 :::"addreal"::: ) ) ")"  ")" ) ")" ))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "e")))  ")" )  ")" )))); end; 






:: deftheorem    defines :::"is_summable_set_by"::: BHSP_6:def 6 :  (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  "ex" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::) "st"  (Bool  "for" (Set (Var "e")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "e"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "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 (Set (Var "Y0"))  ($#r1_tarski :::"c="::: )  (Set (Var "Y1"))) & (Bool (Set (Var "Y1"))  ($#r1_tarski :::"c="::: )  (Set (Var "Y")))) "holds"  (Bool (Set   ($#k18_complex1 :::"abs"::: )  (Set  "(" (Set (Var "r"))  ($#k10_binop_2 :::"-"::: )  (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")))  ")" )  ")" ))))  ")" )))); 
 definitionlet "X" be   ($#l1_bhsp_1 :::"RealUnitarySpace":::); let "Y" be   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")); let "L" be   ($#m1_subset_1 :::"Functional":::) "of" (Set (Const "X")); assume 
(Bool (Set (Const "Y"))  ($#r1_bhsp_6 :::"is_summable_set_by"::: )  (Set (Const "L")))
 ; func  :::"sum_byfunc":::  "(" "Y" "," "L" ")"  ->   ($#m1_subset_1 :::"Real":::) means :: BHSP_6:def 7 (Bool  "for" (Set (Var "e")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "e"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "ex" (Set (Var "Y0")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" "X" "st"  (Bool  "("  (Bool (Bool  "not" (Set (Var "Y0")) "is"   ($#v1_xboole_0 :::"empty"::: )  )) & (Bool (Set (Var "Y0"))  ($#r1_tarski :::"c="::: )  "Y") & (Bool  "("   "for" (Set (Var "Y1")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" "X"  "st" (Bool (Bool (Set (Var "Y0"))  ($#r1_tarski :::"c="::: )  (Set (Var "Y1"))) & (Bool (Set (Var "Y1"))  ($#r1_tarski :::"c="::: )  "Y")) "holds"  (Bool (Set   ($#k18_complex1 :::"abs"::: )  (Set  "(" it  ($#k10_binop_2 :::"-"::: )  (Set  "("  ($#k5_bhsp_5 :::"setopfunc"::: )   "(" (Set (Var "Y1")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "X") "," (Set  ($#k1_numbers :::"REAL"::: ) ) "," "L" "," (Set  ($#k33_binop_2 :::"addreal"::: ) ) ")"  ")" ) ")" ))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "e")))  ")" )  ")" ))); end; 








:: deftheorem    defines :::"sum_byfunc"::: BHSP_6:def 7 :  (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"))  "st" (Bool (Bool (Set (Var "Y"))  ($#r1_bhsp_6 :::"is_summable_set_by"::: )  (Set (Var "L")))) "holds"  (Bool  "for" (Set (Var "b4")) "being"   ($#m1_subset_1 :::"Real":::) "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_bhsp_6 :::"sum_byfunc"::: )   "(" (Set (Var "Y")) "," (Set (Var "L")) ")" )) "iff" (Bool  "for" (Set (Var "e")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "e"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "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 (Set (Var "Y0"))  ($#r1_tarski :::"c="::: )  (Set (Var "Y1"))) & (Bool (Set (Var "Y1"))  ($#r1_tarski :::"c="::: )  (Set (Var "Y")))) "holds"  (Bool (Set   ($#k18_complex1 :::"abs"::: )  (Set  "(" (Set (Var "b4"))  ($#k10_binop_2 :::"-"::: )  (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_6:3 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bhsp_1 :::"RealUnitarySpace":::)  (Bool  "for" (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "Y")) "is"   ($#v1_bhsp_6 :::"summable_set"::: )  )) "holds"  (Bool (Set (Var "Y")) "is"   ($#v3_bhsp_6 :::"weakly_summable_set"::: )  ))) ; 
 
theorem :: BHSP_6:4 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bhsp_1 :::"RealUnitarySpace":::)  (Bool  "for" (Set (Var "L")) "being"   ($#m1_subset_1 :::"linear-Functional":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "p")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "X")))  "st" (Bool (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "p")))  ($#r1_xxreal_0 :::">="::: )  (Num 1))) "holds"  (Bool  "for" (Set (Var "q")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  )  "st" (Bool (Bool (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "q")))) & (Bool  "("   "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "q"))))) "holds"  (Bool (Set (Set (Var "q"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "L"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i")) ")" )))  ")" )) "holds"  (Bool (Set (Set (Var "L"))  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set  "the"  ($#u1_algstr_0 :::"addF"::: )  "of" (Set (Var "X")))  ($#k1_finsop_1 :::""**""::: )  (Set (Var "p")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k33_binop_2 :::"addreal"::: ) )  ($#k1_finsop_1 :::""**""::: )  (Set (Var "q")))))))) ; 
 
theorem :: BHSP_6:5 (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_subset_1 :::"Subset":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Bool  "not" (Set (Var "S")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "holds"  (Bool  "for" (Set (Var "L")) "being"   ($#m1_subset_1 :::"linear-Functional":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Set (Var "L"))  ($#k3_funct_2 :::"."::: )  (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 "L")) "," (Set  ($#k33_binop_2 :::"addreal"::: ) ) ")" ))))) ; 
 
theorem :: BHSP_6:6 (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 "Y")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "Y")) "is"   ($#v3_bhsp_6 :::"weakly_summable_set"::: )  )) "holds"  (Bool  "ex" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "st"  (Bool  "for" (Set (Var "L")) "being"   ($#m1_subset_1 :::"linear-Functional":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "L")) "is"   ($#v2_bhsp_6 :::"Lipschitzian"::: )  )) "holds"  (Bool  "for" (Set (Var "e")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "e"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "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 (Set (Var "Y0"))  ($#r1_tarski :::"c="::: )  (Set (Var "Y1"))) & (Bool (Set (Var "Y1"))  ($#r1_tarski :::"c="::: )  (Set (Var "Y")))) "holds"  (Bool (Set   ($#k18_complex1 :::"abs"::: )  (Set  "(" (Set  "(" (Set (Var "L"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x")) ")" )  ($#k10_binop_2 :::"-"::: )  (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_6:7 (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 "Y")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "Y")) "is"   ($#v3_bhsp_6 :::"weakly_summable_set"::: )  )) "holds"  (Bool  "for" (Set (Var "L")) "being"   ($#m1_subset_1 :::"linear-Functional":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "L")) "is"   ($#v2_bhsp_6 :::"Lipschitzian"::: )  )) "holds"  (Bool (Set (Var "Y"))  ($#r1_bhsp_6 :::"is_summable_set_by"::: )  (Set (Var "L")))))) ; 
 
theorem :: BHSP_6:8 (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 "Y")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "Y")) "is"   ($#v1_bhsp_6 :::"summable_set"::: )  )) "holds"  (Bool  "for" (Set (Var "L")) "being"   ($#m1_subset_1 :::"linear-Functional":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "L")) "is"   ($#v2_bhsp_6 :::"Lipschitzian"::: )  )) "holds"  (Bool (Set (Var "Y"))  ($#r1_bhsp_6 :::"is_summable_set_by"::: )  (Set (Var "L")))))) ; 
 
theorem :: BHSP_6:9 (Bool  "for" (Set (Var "X")) "being"   ($#l1_bhsp_1 :::"RealUnitarySpace":::)  (Bool  "for" (Set (Var "Y")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Bool  "not" (Set (Var "Y")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "holds"  (Bool (Set (Var "Y")) "is"   ($#v1_bhsp_6 :::"summable_set"::: )  ))) ; 
 begin  
theorem :: BHSP_6:10 (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 "Y")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds"   (Bool  "("  (Bool (Set (Var "Y")) "is"   ($#v1_bhsp_6 :::"summable_set"::: )  ) "iff" (Bool  "for" (Set (Var "e")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "e"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "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  ($#k3_bhsp_1 :::"||."::: ) (Set  "("  ($#k1_bhsp_6 :::"setsum"::: )  (Set (Var "Y1")) ")" ) ($#k3_bhsp_1 :::".||"::: ) )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "e")))  ")" )  ")" )))  ")" ))) ;