:: BHSP_4 semantic presentation begin definitionlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; let "seq" be ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "X")); func :::"Partial_Sums"::: "seq" -> ($#m1_subset_1 :::"sequence":::) "of" "X" means :: BHSP_4:def 1 (Bool "(" (Bool (Set it ($#k1_normsp_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set "seq" ($#k1_normsp_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set it ($#k1_normsp_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" it ($#k1_normsp_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" "seq" ($#k1_normsp_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"Partial_Sums"::: BHSP_4:def 1 : (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "seq")) "," (Set (Var "b3")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set (Var "seq")))) "iff" (Bool "(" (Bool (Set (Set (Var "b3")) ($#k1_normsp_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "seq")) ($#k1_normsp_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "b3")) ($#k1_normsp_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "b3")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "seq")) ($#k1_normsp_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ))) ")" ) ")" ) ")" ))); theorem :: BHSP_4:1 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set (Var "seq1")) ")" ) ($#k2_normsp_1 :::"+"::: ) (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set (Var "seq2")) ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set "(" (Set (Var "seq1")) ($#k2_normsp_1 :::"+"::: ) (Set (Var "seq2")) ")" ))))) ; theorem :: BHSP_4:2 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set (Var "seq1")) ")" ) ($#k3_normsp_1 :::"-"::: ) (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set (Var "seq2")) ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set "(" (Set (Var "seq1")) ($#k3_normsp_1 :::"-"::: ) (Set (Var "seq2")) ")" ))))) ; theorem :: BHSP_4:3 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_rlvect_1 :::"vector-distributive"::: ) ($#v6_rlvect_1 :::"scalar-distributive"::: ) ($#v7_rlvect_1 :::"scalar-associative"::: ) ($#v8_rlvect_1 :::"scalar-unital"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set "(" (Set (Var "a")) ($#k5_normsp_1 :::"*"::: ) (Set (Var "seq")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "a")) ($#k5_normsp_1 :::"*"::: ) (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set (Var "seq")) ")" )))))) ; theorem :: BHSP_4:4 (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 ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set "(" ($#k5_vfunct_1 :::"-"::: ) (Set (Var "seq")) ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k5_vfunct_1 :::"-"::: ) (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set (Var "seq")) ")" ))))) ; theorem :: BHSP_4:5 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) (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 (Set (Set "(" (Set (Var "a")) ($#k5_normsp_1 :::"*"::: ) (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set (Var "seq1")) ")" ) ")" ) ($#k6_bhsp_1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k5_normsp_1 :::"*"::: ) (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set (Var "seq2")) ")" ) ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k5_normsp_1 :::"*"::: ) (Set (Var "seq1")) ")" ) ($#k6_bhsp_1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k5_normsp_1 :::"*"::: ) (Set (Var "seq2")) ")" ) ")" )))))) ; definitionlet "X" be ($#l1_bhsp_1 :::"RealUnitarySpace":::); let "seq" be ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "X")); attr "seq" is :::"summable"::: means :: BHSP_4:def 2 (Bool (Set ($#k1_bhsp_4 :::"Partial_Sums"::: ) "seq") "is" ($#v1_bhsp_2 :::"convergent"::: ) ); func :::"Sum"::: "seq" -> ($#m1_subset_1 :::"Point":::) "of" "X" equals :: BHSP_4:def 3 (Set ($#k1_bhsp_2 :::"lim"::: ) (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) "seq" ")" )); end; :: deftheorem defines :::"summable"::: BHSP_4:def 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_4 :::"summable"::: ) ) "iff" (Bool (Set ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set (Var "seq"))) "is" ($#v1_bhsp_2 :::"convergent"::: ) ) ")" ))); :: deftheorem defines :::"Sum"::: BHSP_4: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 (Set ($#k2_bhsp_4 :::"Sum"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set ($#k1_bhsp_2 :::"lim"::: ) (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set (Var "seq")) ")" ))))); theorem :: BHSP_4:6 (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_4 :::"summable"::: ) ) & (Bool (Set (Var "seq2")) "is" ($#v1_bhsp_4 :::"summable"::: ) )) "holds" (Bool "(" (Bool (Set (Set (Var "seq1")) ($#k6_bhsp_1 :::"+"::: ) (Set (Var "seq2"))) "is" ($#v1_bhsp_4 :::"summable"::: ) ) & (Bool (Set ($#k2_bhsp_4 :::"Sum"::: ) (Set "(" (Set (Var "seq1")) ($#k6_bhsp_1 :::"+"::: ) (Set (Var "seq2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_bhsp_4 :::"Sum"::: ) (Set (Var "seq1")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" ($#k2_bhsp_4 :::"Sum"::: ) (Set (Var "seq2")) ")" ))) ")" ))) ; theorem :: BHSP_4:7 (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_4 :::"summable"::: ) ) & (Bool (Set (Var "seq2")) "is" ($#v1_bhsp_4 :::"summable"::: ) )) "holds" (Bool "(" (Bool (Set (Set (Var "seq1")) ($#k3_normsp_1 :::"-"::: ) (Set (Var "seq2"))) "is" ($#v1_bhsp_4 :::"summable"::: ) ) & (Bool (Set ($#k2_bhsp_4 :::"Sum"::: ) (Set "(" (Set (Var "seq1")) ($#k3_normsp_1 :::"-"::: ) (Set (Var "seq2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_bhsp_4 :::"Sum"::: ) (Set (Var "seq1")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" ($#k2_bhsp_4 :::"Sum"::: ) (Set (Var "seq2")) ")" ))) ")" ))) ; theorem :: BHSP_4:8 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) (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_4 :::"summable"::: ) )) "holds" (Bool "(" (Bool (Set (Set (Var "a")) ($#k5_normsp_1 :::"*"::: ) (Set (Var "seq"))) "is" ($#v1_bhsp_4 :::"summable"::: ) ) & (Bool (Set ($#k2_bhsp_4 :::"Sum"::: ) (Set "(" (Set (Var "a")) ($#k5_normsp_1 :::"*"::: ) (Set (Var "seq")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" ($#k2_bhsp_4 :::"Sum"::: ) (Set (Var "seq")) ")" ))) ")" )))) ; theorem :: BHSP_4: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_4 :::"summable"::: ) )) "holds" (Bool "(" (Bool (Set (Var "seq")) "is" ($#v1_bhsp_2 :::"convergent"::: ) ) & (Bool (Set ($#k1_bhsp_2 :::"lim"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X")))) ")" ))) ; theorem :: BHSP_4:10 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealHilbertSpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "seq")) "is" ($#v1_bhsp_4 :::"summable"::: ) ) "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 "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set (Var "seq")) ")" ) ($#k1_normsp_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set (Var "seq")) ")" ) ($#k1_normsp_1 :::"."::: ) (Set (Var "m")) ")" ) ")" ) ($#k3_bhsp_1 :::".||"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r")))))) ")" ))) ; theorem :: BHSP_4:11 (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_4 :::"summable"::: ) )) "holds" (Bool (Set ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set (Var "seq"))) "is" ($#v2_bhsp_3 :::"bounded"::: ) ))) ; theorem :: BHSP_4:12 (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 "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "seq1")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "seq")) ($#k1_normsp_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ))) ")" )) "holds" (Bool (Set ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set "(" (Set (Var "seq")) ($#k1_valued_0 :::"^\"::: ) (Num 1) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set (Var "seq")) ")" ) ($#k1_valued_0 :::"^\"::: ) (Num 1) ")" ) ($#k3_normsp_1 :::"-"::: ) (Set (Var "seq1")))))) ; theorem :: BHSP_4:13 (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_4 :::"summable"::: ) )) "holds" (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "seq")) ($#k1_valued_0 :::"^\"::: ) (Set (Var "k"))) "is" ($#v1_bhsp_4 :::"summable"::: ) )))) ; theorem :: BHSP_4:14 (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 "ex" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Set (Set (Var "seq")) ($#k1_valued_0 :::"^\"::: ) (Set (Var "k"))) "is" ($#v1_bhsp_4 :::"summable"::: ) ))) "holds" (Bool (Set (Var "seq")) "is" ($#v1_bhsp_4 :::"summable"::: ) ))) ; definitionlet "X" be ($#l1_bhsp_1 :::"RealUnitarySpace":::); let "seq" be ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "X")); let "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func :::"Sum"::: "(" "seq" "," "n" ")" -> ($#m1_subset_1 :::"Point":::) "of" "X" equals :: BHSP_4:def 4 (Set (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) "seq" ")" ) ($#k1_normsp_1 :::"."::: ) "n"); end; :: deftheorem defines :::"Sum"::: BHSP_4:def 4 : (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 "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k3_bhsp_4 :::"Sum"::: ) "(" (Set (Var "seq")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set (Var "seq")) ")" ) ($#k1_normsp_1 :::"."::: ) (Set (Var "n"))))))); theorem :: BHSP_4:15 (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 ($#k3_bhsp_4 :::"Sum"::: ) "(" (Set (Var "seq")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "seq")) ($#k1_normsp_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ))))) ; theorem :: BHSP_4:16 (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 ($#k3_bhsp_4 :::"Sum"::: ) "(" (Set (Var "seq")) "," (Num 1) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_bhsp_4 :::"Sum"::: ) "(" (Set (Var "seq")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "seq")) ($#k1_normsp_1 :::"."::: ) (Num 1) ")" ))))) ; theorem :: BHSP_4:17 (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 ($#k3_bhsp_4 :::"Sum"::: ) "(" (Set (Var "seq")) "," (Num 1) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "seq")) ($#k1_normsp_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "seq")) ($#k1_normsp_1 :::"."::: ) (Num 1) ")" ))))) ; theorem :: BHSP_4:18 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (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 ($#k3_bhsp_4 :::"Sum"::: ) "(" (Set (Var "seq")) "," (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_bhsp_4 :::"Sum"::: ) "(" (Set (Var "seq")) "," (Set (Var "n")) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "seq")) ($#k1_normsp_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" )))))) ; theorem :: BHSP_4:19 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (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 (Set (Var "seq")) ($#k1_normsp_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_bhsp_4 :::"Sum"::: ) "(" (Set (Var "seq")) "," (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" ($#k3_bhsp_4 :::"Sum"::: ) "(" (Set (Var "seq")) "," (Set (Var "n")) ")" ")" )))))) ; theorem :: BHSP_4:20 (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 (Set (Var "seq")) ($#k1_normsp_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_bhsp_4 :::"Sum"::: ) "(" (Set (Var "seq")) "," (Num 1) ")" ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" ($#k3_bhsp_4 :::"Sum"::: ) "(" (Set (Var "seq")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ")" ))))) ; definitionlet "X" be ($#l1_bhsp_1 :::"RealUnitarySpace":::); let "seq" be ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "X")); let "n", "m" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func :::"Sum"::: "(" "seq" "," "n" "," "m" ")" -> ($#m1_subset_1 :::"Point":::) "of" "X" equals :: BHSP_4:def 5 (Set (Set "(" ($#k3_bhsp_4 :::"Sum"::: ) "(" "seq" "," "n" ")" ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" ($#k3_bhsp_4 :::"Sum"::: ) "(" "seq" "," "m" ")" ")" )); end; :: deftheorem defines :::"Sum"::: BHSP_4:def 5 : (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 "n")) "," (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k4_bhsp_4 :::"Sum"::: ) "(" (Set (Var "seq")) "," (Set (Var "n")) "," (Set (Var "m")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_bhsp_4 :::"Sum"::: ) "(" (Set (Var "seq")) "," (Set (Var "n")) ")" ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" ($#k3_bhsp_4 :::"Sum"::: ) "(" (Set (Var "seq")) "," (Set (Var "m")) ")" ")" )))))); theorem :: BHSP_4:21 (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 ($#k4_bhsp_4 :::"Sum"::: ) "(" (Set (Var "seq")) "," (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "seq")) ($#k1_normsp_1 :::"."::: ) (Num 1))))) ; theorem :: BHSP_4:22 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (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 ($#k4_bhsp_4 :::"Sum"::: ) "(" (Set (Var "seq")) "," (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "seq")) ($#k1_normsp_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )))))) ; theorem :: BHSP_4:23 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealHilbertSpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "seq")) "is" ($#v1_bhsp_4 :::"summable"::: ) ) "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 "(" ($#k3_bhsp_4 :::"Sum"::: ) "(" (Set (Var "seq")) "," (Set (Var "n")) ")" ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" ($#k3_bhsp_4 :::"Sum"::: ) "(" (Set (Var "seq")) "," (Set (Var "m")) ")" ")" ) ")" ) ($#k3_bhsp_1 :::".||"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r")))))) ")" ))) ; theorem :: BHSP_4:24 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealHilbertSpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "seq")) "is" ($#v1_bhsp_4 :::"summable"::: ) ) "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 "(" ($#k4_bhsp_4 :::"Sum"::: ) "(" (Set (Var "seq")) "," (Set (Var "n")) "," (Set (Var "m")) ")" ")" ) ($#k3_bhsp_1 :::".||"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r")))))) ")" ))) ; definitionlet "X" be ($#l1_bhsp_1 :::"RealUnitarySpace":::); let "seq" be ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "X")); attr "seq" is :::"absolutely_summable"::: means :: BHSP_4:def 6 (Bool (Set ($#k2_bhsp_2 :::"||."::: ) "seq" ($#k2_bhsp_2 :::".||"::: ) ) "is" ($#v1_series_1 :::"summable"::: ) ); end; :: deftheorem defines :::"absolutely_summable"::: BHSP_4:def 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")) "holds" (Bool "(" (Bool (Set (Var "seq")) "is" ($#v2_bhsp_4 :::"absolutely_summable"::: ) ) "iff" (Bool (Set ($#k2_bhsp_2 :::"||."::: ) (Set (Var "seq")) ($#k2_bhsp_2 :::".||"::: ) ) "is" ($#v1_series_1 :::"summable"::: ) ) ")" ))); theorem :: BHSP_4: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_4 :::"absolutely_summable"::: ) ) & (Bool (Set (Var "seq2")) "is" ($#v2_bhsp_4 :::"absolutely_summable"::: ) )) "holds" (Bool (Set (Set (Var "seq1")) ($#k6_bhsp_1 :::"+"::: ) (Set (Var "seq2"))) "is" ($#v2_bhsp_4 :::"absolutely_summable"::: ) ))) ; theorem :: BHSP_4:26 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) (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_4 :::"absolutely_summable"::: ) )) "holds" (Bool (Set (Set (Var "a")) ($#k5_normsp_1 :::"*"::: ) (Set (Var "seq"))) "is" ($#v2_bhsp_4 :::"absolutely_summable"::: ) )))) ; theorem :: BHSP_4:27 (Bool "for" (Set (Var "Rseq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) (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 "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set ($#k2_bhsp_2 :::"||."::: ) (Set (Var "seq")) ($#k2_bhsp_2 :::".||"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "Rseq")) ($#k1_seq_1 :::"."::: ) (Set (Var "n")))) ")" ) & (Bool (Set (Var "Rseq")) "is" ($#v1_series_1 :::"summable"::: ) )) "holds" (Bool (Set (Var "seq")) "is" ($#v2_bhsp_4 :::"absolutely_summable"::: ) )))) ; theorem :: BHSP_4:28 (Bool "for" (Set (Var "Rseq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) (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 "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Set (Var "seq")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X")))) & (Bool (Set (Set (Var "Rseq")) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k3_bhsp_1 :::"||."::: ) (Set "(" (Set (Var "seq")) ($#k1_normsp_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k3_bhsp_1 :::".||"::: ) ) ($#k10_real_1 :::"/"::: ) (Set ($#k3_bhsp_1 :::"||."::: ) (Set "(" (Set (Var "seq")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k3_bhsp_1 :::".||"::: ) ))) ")" ) ")" ) & (Bool (Set (Var "Rseq")) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set (Var "Rseq"))) ($#r1_xxreal_0 :::"<"::: ) (Num 1))) "holds" (Bool (Set (Var "seq")) "is" ($#v2_bhsp_4 :::"absolutely_summable"::: ) )))) ; theorem :: BHSP_4:29 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (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 "r")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (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 (Var "seq")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k3_bhsp_1 :::".||"::: ) ) ($#r1_xxreal_0 :::">="::: ) (Set (Var "r"))))) & (Bool (Set (Var "seq")) "is" ($#v1_bhsp_2 :::"convergent"::: ) )) "holds" (Bool (Set ($#k1_bhsp_2 :::"lim"::: ) (Set (Var "seq"))) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X"))))))) ; theorem :: BHSP_4: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")) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "seq")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X")))) ")" ) & (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 (Set ($#k3_bhsp_1 :::"||."::: ) (Set "(" (Set (Var "seq")) ($#k1_normsp_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k3_bhsp_1 :::".||"::: ) ) ($#k10_real_1 :::"/"::: ) (Set ($#k3_bhsp_1 :::"||."::: ) (Set "(" (Set (Var "seq")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k3_bhsp_1 :::".||"::: ) )) ($#r1_xxreal_0 :::">="::: ) (Num 1))))) "holds" (Bool "not" (Bool (Set (Var "seq")) "is" ($#v1_bhsp_4 :::"summable"::: ) )))) ; theorem :: BHSP_4:31 (Bool "for" (Set (Var "Rseq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) (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 "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "seq")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X")))) ")" ) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "Rseq")) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k3_bhsp_1 :::"||."::: ) (Set "(" (Set (Var "seq")) ($#k1_normsp_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k3_bhsp_1 :::".||"::: ) ) ($#k10_real_1 :::"/"::: ) (Set ($#k3_bhsp_1 :::"||."::: ) (Set "(" (Set (Var "seq")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k3_bhsp_1 :::".||"::: ) ))) ")" ) & (Bool (Set (Var "Rseq")) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set (Var "Rseq"))) ($#r1_xxreal_0 :::">"::: ) (Num 1))) "holds" (Bool "not" (Bool (Set (Var "seq")) "is" ($#v1_bhsp_4 :::"summable"::: ) ))))) ; theorem :: BHSP_4:32 (Bool "for" (Set (Var "Rseq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) (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 "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "Rseq")) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k2_power :::"-root"::: ) (Set ($#k3_bhsp_1 :::"||."::: ) (Set "(" (Set (Var "seq")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k3_bhsp_1 :::".||"::: ) ))) ")" ) & (Bool (Set (Var "Rseq")) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set (Var "Rseq"))) ($#r1_xxreal_0 :::"<"::: ) (Num 1))) "holds" (Bool (Set (Var "seq")) "is" ($#v2_bhsp_4 :::"absolutely_summable"::: ) )))) ; theorem :: BHSP_4:33 (Bool "for" (Set (Var "Rseq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) (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 "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "Rseq")) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k2_power :::"-root"::: ) (Set "(" (Set ($#k2_bhsp_2 :::"||."::: ) (Set (Var "seq")) ($#k2_bhsp_2 :::".||"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "n")) ")" ))) ")" ) & (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 (Set (Var "Rseq")) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::">="::: ) (Num 1))))) "holds" (Bool "not" (Bool (Set (Var "seq")) "is" ($#v1_bhsp_4 :::"summable"::: ) ))))) ; theorem :: BHSP_4:34 (Bool "for" (Set (Var "Rseq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) (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 "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "Rseq")) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k2_power :::"-root"::: ) (Set "(" (Set ($#k2_bhsp_2 :::"||."::: ) (Set (Var "seq")) ($#k2_bhsp_2 :::".||"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "n")) ")" ))) ")" ) & (Bool (Set (Var "Rseq")) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set (Var "Rseq"))) ($#r1_xxreal_0 :::">"::: ) (Num 1))) "holds" (Bool "not" (Bool (Set (Var "seq")) "is" ($#v1_bhsp_4 :::"summable"::: ) ))))) ; theorem :: BHSP_4:35 (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 ($#k3_series_1 :::"Partial_Sums"::: ) (Set ($#k2_bhsp_2 :::"||."::: ) (Set (Var "seq")) ($#k2_bhsp_2 :::".||"::: ) )) "is" ($#v7_valued_0 :::"non-decreasing"::: ) ))) ; theorem :: BHSP_4: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 "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set ($#k2_bhsp_2 :::"||."::: ) (Set (Var "seq")) ($#k2_bhsp_2 :::".||"::: ) ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))))) ; theorem :: BHSP_4:37 (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 "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k3_bhsp_1 :::"||."::: ) (Set "(" (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set (Var "seq")) ")" ) ($#k1_normsp_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k3_bhsp_1 :::".||"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set ($#k2_bhsp_2 :::"||."::: ) (Set (Var "seq")) ($#k2_bhsp_2 :::".||"::: ) ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))))))) ; theorem :: BHSP_4:38 (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 "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k3_bhsp_1 :::"||."::: ) (Set "(" ($#k3_bhsp_4 :::"Sum"::: ) "(" (Set (Var "seq")) "," (Set (Var "n")) ")" ")" ) ($#k3_bhsp_1 :::".||"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_series_1 :::"Sum"::: ) "(" (Set ($#k2_bhsp_2 :::"||."::: ) (Set (Var "seq")) ($#k2_bhsp_2 :::".||"::: ) ) "," (Set (Var "n")) ")" ))))) ; theorem :: BHSP_4: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 "n")) "," (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k3_bhsp_1 :::"||."::: ) (Set "(" (Set "(" (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set (Var "seq")) ")" ) ($#k1_normsp_1 :::"."::: ) (Set (Var "m")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set (Var "seq")) ")" ) ($#k1_normsp_1 :::"."::: ) (Set (Var "n")) ")" ) ")" ) ($#k3_bhsp_1 :::".||"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set "(" (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set ($#k2_bhsp_2 :::"||."::: ) (Set (Var "seq")) ($#k2_bhsp_2 :::".||"::: ) ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "m")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set ($#k2_bhsp_2 :::"||."::: ) (Set (Var "seq")) ($#k2_bhsp_2 :::".||"::: ) ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "n")) ")" ) ")" )))))) ; theorem :: BHSP_4:40 (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 "n")) "," (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k3_bhsp_1 :::"||."::: ) (Set "(" (Set "(" ($#k3_bhsp_4 :::"Sum"::: ) "(" (Set (Var "seq")) "," (Set (Var "m")) ")" ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" ($#k3_bhsp_4 :::"Sum"::: ) "(" (Set (Var "seq")) "," (Set (Var "n")) ")" ")" ) ")" ) ($#k3_bhsp_1 :::".||"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set "(" ($#k6_series_1 :::"Sum"::: ) "(" (Set ($#k2_bhsp_2 :::"||."::: ) (Set (Var "seq")) ($#k2_bhsp_2 :::".||"::: ) ) "," (Set (Var "m")) ")" ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k6_series_1 :::"Sum"::: ) "(" (Set ($#k2_bhsp_2 :::"||."::: ) (Set (Var "seq")) ($#k2_bhsp_2 :::".||"::: ) ) "," (Set (Var "n")) ")" ")" ) ")" )))))) ; theorem :: BHSP_4: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 "n")) "," (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k3_bhsp_1 :::"||."::: ) (Set "(" ($#k4_bhsp_4 :::"Sum"::: ) "(" (Set (Var "seq")) "," (Set (Var "m")) "," (Set (Var "n")) ")" ")" ) ($#k3_bhsp_1 :::".||"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k18_complex1 :::"abs"::: ) (Set "(" ($#k7_series_1 :::"Sum"::: ) "(" (Set ($#k2_bhsp_2 :::"||."::: ) (Set (Var "seq")) ($#k2_bhsp_2 :::".||"::: ) ) "," (Set (Var "m")) "," (Set (Var "n")) ")" ")" )))))) ; theorem :: BHSP_4:42 (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealHilbertSpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v2_bhsp_4 :::"absolutely_summable"::: ) )) "holds" (Bool (Set (Var "seq")) "is" ($#v1_bhsp_4 :::"summable"::: ) ))) ; definitionlet "X" be ($#l1_bhsp_1 :::"RealUnitarySpace":::); let "seq" be ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "X")); let "Rseq" be ($#m1_subset_1 :::"Real_Sequence":::); func "Rseq" :::"*"::: "seq" -> ($#m1_subset_1 :::"sequence":::) "of" "X" means :: BHSP_4:def 7 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set it ($#k1_normsp_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "Rseq" ($#k1_seq_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" "seq" ($#k1_normsp_1 :::"."::: ) (Set (Var "n")) ")" )))); end; :: deftheorem defines :::"*"::: BHSP_4:def 7 : (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 "Rseq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "Rseq")) ($#k5_bhsp_4 :::"*"::: ) (Set (Var "seq")))) "iff" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "b4")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "Rseq")) ($#k1_seq_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set (Var "seq")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n")) ")" )))) ")" ))))); theorem :: BHSP_4:43 (Bool "for" (Set (Var "Rseq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) (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 (Set (Set (Var "Rseq")) ($#k5_bhsp_4 :::"*"::: ) (Set "(" (Set (Var "seq1")) ($#k6_bhsp_1 :::"+"::: ) (Set (Var "seq2")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set (Var "Rseq")) ($#k5_bhsp_4 :::"*"::: ) (Set (Var "seq1")) ")" ) ($#k6_bhsp_1 :::"+"::: ) (Set "(" (Set (Var "Rseq")) ($#k5_bhsp_4 :::"*"::: ) (Set (Var "seq2")) ")" )))))) ; theorem :: BHSP_4:44 (Bool "for" (Set (Var "Rseq1")) "," (Set (Var "Rseq2")) "being" ($#m1_subset_1 :::"Real_Sequence":::) (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 (Set "(" (Set (Var "Rseq1")) ($#k1_series_1 :::"+"::: ) (Set (Var "Rseq2")) ")" ) ($#k5_bhsp_4 :::"*"::: ) (Set (Var "seq"))) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set (Var "Rseq1")) ($#k5_bhsp_4 :::"*"::: ) (Set (Var "seq")) ")" ) ($#k6_bhsp_1 :::"+"::: ) (Set "(" (Set (Var "Rseq2")) ($#k5_bhsp_4 :::"*"::: ) (Set (Var "seq")) ")" )))))) ; theorem :: BHSP_4:45 (Bool "for" (Set (Var "Rseq1")) "," (Set (Var "Rseq2")) "being" ($#m1_subset_1 :::"Real_Sequence":::) (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 (Set "(" (Set (Var "Rseq1")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "Rseq2")) ")" ) ($#k5_bhsp_4 :::"*"::: ) (Set (Var "seq"))) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "Rseq1")) ($#k5_bhsp_4 :::"*"::: ) (Set "(" (Set (Var "Rseq2")) ($#k5_bhsp_4 :::"*"::: ) (Set (Var "seq")) ")" )))))) ; theorem :: BHSP_4:46 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "Rseq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) (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 (Set "(" (Set (Var "a")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "Rseq")) ")" ) ($#k5_bhsp_4 :::"*"::: ) (Set (Var "seq"))) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "a")) ($#k5_normsp_1 :::"*"::: ) (Set "(" (Set (Var "Rseq")) ($#k5_bhsp_4 :::"*"::: ) (Set (Var "seq")) ")" ))))))) ; theorem :: BHSP_4:47 (Bool "for" (Set (Var "Rseq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) (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 (Set (Var "Rseq")) ($#k5_bhsp_4 :::"*"::: ) (Set "(" ($#k5_vfunct_1 :::"-"::: ) (Set (Var "seq")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k32_valued_1 :::"-"::: ) (Set (Var "Rseq")) ")" ) ($#k5_bhsp_4 :::"*"::: ) (Set (Var "seq"))))))) ; theorem :: BHSP_4:48 (Bool "for" (Set (Var "Rseq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) (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 "Rseq")) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set (Var "seq")) "is" ($#v1_bhsp_2 :::"convergent"::: ) )) "holds" (Bool (Set (Set (Var "Rseq")) ($#k5_bhsp_4 :::"*"::: ) (Set (Var "seq"))) "is" ($#v1_bhsp_2 :::"convergent"::: ) )))) ; theorem :: BHSP_4:49 (Bool "for" (Set (Var "Rseq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) (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 "Rseq")) "is" ($#v1_comseq_2 :::"bounded"::: ) ) & (Bool (Set (Var "seq")) "is" ($#v2_bhsp_3 :::"bounded"::: ) )) "holds" (Bool (Set (Set (Var "Rseq")) ($#k5_bhsp_4 :::"*"::: ) (Set (Var "seq"))) "is" ($#v2_bhsp_3 :::"bounded"::: ) )))) ; theorem :: BHSP_4:50 (Bool "for" (Set (Var "Rseq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) (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 "Rseq")) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set (Var "seq")) "is" ($#v1_bhsp_2 :::"convergent"::: ) )) "holds" (Bool "(" (Bool (Set (Set (Var "Rseq")) ($#k5_bhsp_4 :::"*"::: ) (Set (Var "seq"))) "is" ($#v1_bhsp_2 :::"convergent"::: ) ) & (Bool (Set ($#k1_bhsp_2 :::"lim"::: ) (Set "(" (Set (Var "Rseq")) ($#k5_bhsp_4 :::"*"::: ) (Set (Var "seq")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_seq_2 :::"lim"::: ) (Set (Var "Rseq")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" ($#k1_bhsp_2 :::"lim"::: ) (Set (Var "seq")) ")" ))) ")" )))) ; definitionlet "Rseq" be ($#m1_subset_1 :::"Real_Sequence":::); attr "Rseq" is :::"Cauchy"::: means :: BHSP_4:def 8 (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 ($#k18_complex1 :::"abs"::: ) (Set "(" (Set "(" "Rseq" ($#k1_seq_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" "Rseq" ($#k1_seq_1 :::"."::: ) (Set (Var "m")) ")" ) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r")))))); end; :: deftheorem defines :::"Cauchy"::: BHSP_4:def 8 : (Bool "for" (Set (Var "Rseq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "holds" (Bool "(" (Bool (Set (Var "Rseq")) "is" ($#v3_bhsp_4 :::"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 ($#k18_complex1 :::"abs"::: ) (Set "(" (Set "(" (Set (Var "Rseq")) ($#k1_seq_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "Rseq")) ($#k1_seq_1 :::"."::: ) (Set (Var "m")) ")" ) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r")))))) ")" )); theorem :: BHSP_4:51 (Bool "for" (Set (Var "Rseq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) (Bool "for" (Set (Var "X")) "being" ($#l1_bhsp_1 :::"RealHilbertSpace":::) (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"::: ) ) & (Bool (Set (Var "Rseq")) "is" ($#v3_bhsp_4 :::"Cauchy"::: ) )) "holds" (Bool (Set (Set (Var "Rseq")) ($#k5_bhsp_4 :::"*"::: ) (Set (Var "seq"))) "is" ($#v1_bhsp_3 :::"Cauchy"::: ) )))) ; theorem :: BHSP_4:52 (Bool "for" (Set (Var "Rseq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) (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 "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set "(" (Set "(" (Set (Var "Rseq")) ($#k47_valued_1 :::"-"::: ) (Set "(" (Set (Var "Rseq")) ($#k1_valued_0 :::"^\"::: ) (Num 1) ")" ) ")" ) ($#k5_bhsp_4 :::"*"::: ) (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set (Var "seq")) ")" ) ")" ) ")" ) ($#k1_normsp_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set "(" (Set (Var "Rseq")) ($#k5_bhsp_4 :::"*"::: ) (Set (Var "seq")) ")" ) ")" ) ($#k1_normsp_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set "(" (Set (Var "Rseq")) ($#k5_bhsp_4 :::"*"::: ) (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set (Var "seq")) ")" ) ")" ) ($#k1_normsp_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ))))))) ; theorem :: BHSP_4:53 (Bool "for" (Set (Var "Rseq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) (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 "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set "(" (Set (Var "Rseq")) ($#k5_bhsp_4 :::"*"::: ) (Set (Var "seq")) ")" ) ")" ) ($#k1_normsp_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "Rseq")) ($#k5_bhsp_4 :::"*"::: ) (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set (Var "seq")) ")" ) ")" ) ($#k1_normsp_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "Rseq")) ($#k1_valued_0 :::"^\"::: ) (Num 1) ")" ) ($#k47_valued_1 :::"-"::: ) (Set (Var "Rseq")) ")" ) ($#k5_bhsp_4 :::"*"::: ) (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set (Var "seq")) ")" ) ")" ) ")" ) ($#k1_normsp_1 :::"."::: ) (Set (Var "n")) ")" ))))))) ; theorem :: BHSP_4:54 (Bool "for" (Set (Var "Rseq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) (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 "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k3_bhsp_4 :::"Sum"::: ) "(" (Set "(" (Set (Var "Rseq")) ($#k5_bhsp_4 :::"*"::: ) (Set (Var "seq")) ")" ) "," (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "Rseq")) ($#k5_bhsp_4 :::"*"::: ) (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set (Var "seq")) ")" ) ")" ) ($#k1_normsp_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" ($#k3_bhsp_4 :::"Sum"::: ) "(" (Set "(" (Set "(" (Set "(" (Set (Var "Rseq")) ($#k1_valued_0 :::"^\"::: ) (Num 1) ")" ) ($#k47_valued_1 :::"-"::: ) (Set (Var "Rseq")) ")" ) ($#k5_bhsp_4 :::"*"::: ) (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set (Var "seq")) ")" ) ")" ) "," (Set (Var "n")) ")" ")" ))))))) ;