:: CLVECT_3 semantic presentation begin theorem :: CLVECT_3:1 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (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")) ")" ) ($#k16_csspace :::"+"::: ) (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set (Var "seq2")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set "(" (Set (Var "seq1")) ($#k16_csspace :::"+"::: ) (Set (Var "seq2")) ")" ))))) ; theorem :: CLVECT_3:2 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (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")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set "(" (Set (Var "seq1")) ($#k3_normsp_1 :::"-"::: ) (Set (Var "seq2")) ")" ))))) ; theorem :: CLVECT_3:3 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "z")) "being" ($#m1_hidden :::"Complex":::) "holds" (Bool (Set ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set "(" (Set (Var "z")) ($#k6_clvect_1 :::"*"::: ) (Set (Var "seq")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "z")) ($#k6_clvect_1 :::"*"::: ) (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set (Var "seq")) ")" )))))) ; theorem :: CLVECT_3:4 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (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")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_vfunct_1 :::"-"::: ) (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set (Var "seq")) ")" ))))) ; theorem :: CLVECT_3:5 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (Bool "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#m1_hidden :::"Complex":::) "holds" (Bool (Set (Set "(" (Set (Var "z1")) ($#k6_clvect_1 :::"*"::: ) (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set (Var "seq1")) ")" ) ")" ) ($#k16_csspace :::"+"::: ) (Set "(" (Set (Var "z2")) ($#k6_clvect_1 :::"*"::: ) (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set (Var "seq2")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set "(" (Set "(" (Set (Var "z1")) ($#k6_clvect_1 :::"*"::: ) (Set (Var "seq1")) ")" ) ($#k16_csspace :::"+"::: ) (Set "(" (Set (Var "z2")) ($#k6_clvect_1 :::"*"::: ) (Set (Var "seq2")) ")" ) ")" )))))) ; definitionlet "X" be ($#l1_csspace :::"ComplexUnitarySpace":::); let "seq" be ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "X")); attr "seq" is :::"summable"::: means :: CLVECT_3:def 1 (Bool (Set ($#k1_bhsp_4 :::"Partial_Sums"::: ) "seq") "is" ($#v1_clvect_2 :::"convergent"::: ) ); func :::"Sum"::: "seq" -> ($#m1_subset_1 :::"Point":::) "of" "X" equals :: CLVECT_3:def 2 (Set ($#k1_clvect_2 :::"lim"::: ) (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) "seq" ")" )); end; :: deftheorem defines :::"summable"::: CLVECT_3:def 1 : (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "seq")) "is" ($#v1_clvect_3 :::"summable"::: ) ) "iff" (Bool (Set ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set (Var "seq"))) "is" ($#v1_clvect_2 :::"convergent"::: ) ) ")" ))); :: deftheorem defines :::"Sum"::: CLVECT_3:def 2 : (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k1_clvect_3 :::"Sum"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set ($#k1_clvect_2 :::"lim"::: ) (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set (Var "seq")) ")" ))))); theorem :: CLVECT_3:6 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (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_clvect_3 :::"summable"::: ) ) & (Bool (Set (Var "seq2")) "is" ($#v1_clvect_3 :::"summable"::: ) )) "holds" (Bool "(" (Bool (Set (Set (Var "seq1")) ($#k16_csspace :::"+"::: ) (Set (Var "seq2"))) "is" ($#v1_clvect_3 :::"summable"::: ) ) & (Bool (Set ($#k1_clvect_3 :::"Sum"::: ) (Set "(" (Set (Var "seq1")) ($#k16_csspace :::"+"::: ) (Set (Var "seq2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_clvect_3 :::"Sum"::: ) (Set (Var "seq1")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" ($#k1_clvect_3 :::"Sum"::: ) (Set (Var "seq2")) ")" ))) ")" ))) ; theorem :: CLVECT_3:7 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (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_clvect_3 :::"summable"::: ) ) & (Bool (Set (Var "seq2")) "is" ($#v1_clvect_3 :::"summable"::: ) )) "holds" (Bool "(" (Bool (Set (Set (Var "seq1")) ($#k3_normsp_1 :::"-"::: ) (Set (Var "seq2"))) "is" ($#v1_clvect_3 :::"summable"::: ) ) & (Bool (Set ($#k1_clvect_3 :::"Sum"::: ) (Set "(" (Set (Var "seq1")) ($#k3_normsp_1 :::"-"::: ) (Set (Var "seq2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_clvect_3 :::"Sum"::: ) (Set (Var "seq1")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" ($#k1_clvect_3 :::"Sum"::: ) (Set (Var "seq2")) ")" ))) ")" ))) ; theorem :: CLVECT_3:8 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "z")) "being" ($#m1_hidden :::"Complex":::) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v1_clvect_3 :::"summable"::: ) )) "holds" (Bool "(" (Bool (Set (Set (Var "z")) ($#k6_clvect_1 :::"*"::: ) (Set (Var "seq"))) "is" ($#v1_clvect_3 :::"summable"::: ) ) & (Bool (Set ($#k1_clvect_3 :::"Sum"::: ) (Set "(" (Set (Var "z")) ($#k6_clvect_1 :::"*"::: ) (Set (Var "seq")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "z")) ($#k1_clvect_1 :::"*"::: ) (Set "(" ($#k1_clvect_3 :::"Sum"::: ) (Set (Var "seq")) ")" ))) ")" )))) ; theorem :: CLVECT_3:9 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v1_clvect_3 :::"summable"::: ) )) "holds" (Bool "(" (Bool (Set (Var "seq")) "is" ($#v1_clvect_2 :::"convergent"::: ) ) & (Bool (Set ($#k1_clvect_2 :::"lim"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X")))) ")" ))) ; theorem :: CLVECT_3:10 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexHilbertSpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "seq")) "is" ($#v1_clvect_3 :::"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 ($#k13_csspace :::"||."::: ) (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")) ")" ) ")" ) ($#k13_csspace :::".||"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r")))))) ")" ))) ; theorem :: CLVECT_3:11 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v1_clvect_3 :::"summable"::: ) )) "holds" (Bool (Set ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set (Var "seq"))) "is" ($#v3_clvect_2 :::"bounded"::: ) ))) ; theorem :: CLVECT_3:12 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (Bool "for" (Set (Var "seq1")) "," (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 "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) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set (Var "seq")) ")" ) ($#k1_valued_0 :::"^\"::: ) (Num 1) ")" ) ($#k3_normsp_1 :::"-"::: ) (Set (Var "seq1")))))) ; theorem :: CLVECT_3:13 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v1_clvect_3 :::"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_clvect_3 :::"summable"::: ) )))) ; theorem :: CLVECT_3:14 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (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_clvect_3 :::"summable"::: ) ))) "holds" (Bool (Set (Var "seq")) "is" ($#v1_clvect_3 :::"summable"::: ) ))) ; definitionlet "X" be ($#l1_csspace :::"ComplexUnitarySpace":::); 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 :: CLVECT_3:def 3 (Set (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) "seq" ")" ) ($#k1_normsp_1 :::"."::: ) "n"); end; :: deftheorem defines :::"Sum"::: CLVECT_3:def 3 : (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (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 ($#k2_clvect_3 :::"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 :: CLVECT_3:15 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k2_clvect_3 :::"Sum"::: ) "(" (Set (Var "seq")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "seq")) ($#k1_normsp_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ))))) ; theorem :: CLVECT_3:16 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k2_clvect_3 :::"Sum"::: ) "(" (Set (Var "seq")) "," (Num 1) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_clvect_3 :::"Sum"::: ) "(" (Set (Var "seq")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "seq")) ($#k1_normsp_1 :::"."::: ) (Num 1) ")" ))))) ; theorem :: CLVECT_3:17 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k2_clvect_3 :::"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 :: CLVECT_3:18 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (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 ($#k2_clvect_3 :::"Sum"::: ) "(" (Set (Var "seq")) "," (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_clvect_3 :::"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 :: CLVECT_3:19 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (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 (Var "seq")) ($#k1_normsp_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_clvect_3 :::"Sum"::: ) "(" (Set (Var "seq")) "," (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" ($#k2_clvect_3 :::"Sum"::: ) "(" (Set (Var "seq")) "," (Set (Var "n")) ")" ")" )))))) ; theorem :: CLVECT_3:20 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (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 "(" ($#k2_clvect_3 :::"Sum"::: ) "(" (Set (Var "seq")) "," (Num 1) ")" ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" ($#k2_clvect_3 :::"Sum"::: ) "(" (Set (Var "seq")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ")" ))))) ; definitionlet "X" be ($#l1_csspace :::"ComplexUnitarySpace":::); 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 :: CLVECT_3:def 4 (Set (Set "(" ($#k2_clvect_3 :::"Sum"::: ) "(" "seq" "," "n" ")" ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" ($#k2_clvect_3 :::"Sum"::: ) "(" "seq" "," "m" ")" ")" )); end; :: deftheorem defines :::"Sum"::: CLVECT_3:def 4 : (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (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_clvect_3 :::"Sum"::: ) "(" (Set (Var "seq")) "," (Set (Var "n")) "," (Set (Var "m")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_clvect_3 :::"Sum"::: ) "(" (Set (Var "seq")) "," (Set (Var "n")) ")" ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" ($#k2_clvect_3 :::"Sum"::: ) "(" (Set (Var "seq")) "," (Set (Var "m")) ")" ")" )))))); theorem :: CLVECT_3:21 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k3_clvect_3 :::"Sum"::: ) "(" (Set (Var "seq")) "," (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "seq")) ($#k1_normsp_1 :::"."::: ) (Num 1))))) ; theorem :: CLVECT_3:22 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (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_clvect_3 :::"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 :: CLVECT_3:23 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexHilbertSpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "seq")) "is" ($#v1_clvect_3 :::"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 ($#k13_csspace :::"||."::: ) (Set "(" (Set "(" ($#k2_clvect_3 :::"Sum"::: ) "(" (Set (Var "seq")) "," (Set (Var "n")) ")" ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" ($#k2_clvect_3 :::"Sum"::: ) "(" (Set (Var "seq")) "," (Set (Var "m")) ")" ")" ) ")" ) ($#k13_csspace :::".||"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r")))))) ")" ))) ; theorem :: CLVECT_3:24 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexHilbertSpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "seq")) "is" ($#v1_clvect_3 :::"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 ($#k13_csspace :::"||."::: ) (Set "(" ($#k3_clvect_3 :::"Sum"::: ) "(" (Set (Var "seq")) "," (Set (Var "n")) "," (Set (Var "m")) ")" ")" ) ($#k13_csspace :::".||"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r")))))) ")" ))) ; definitionlet "Cseq" be ($#m1_subset_1 :::"Complex_Sequence":::); let "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func :::"Sum"::: "(" "Cseq" "," "n" ")" -> ($#m1_hidden :::"Complex":::) equals :: CLVECT_3:def 5 (Set (Set "(" ($#k10_comseq_3 :::"Partial_Sums"::: ) "Cseq" ")" ) ($#k8_nat_1 :::"."::: ) "n"); end; :: deftheorem defines :::"Sum"::: CLVECT_3:def 5 : (Bool "for" (Set (Var "Cseq")) "being" ($#m1_subset_1 :::"Complex_Sequence":::) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k4_clvect_3 :::"Sum"::: ) "(" (Set (Var "Cseq")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k10_comseq_3 :::"Partial_Sums"::: ) (Set (Var "Cseq")) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n")))))); definitionlet "Cseq" be ($#m1_subset_1 :::"Complex_Sequence":::); let "n", "m" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func :::"Sum"::: "(" "Cseq" "," "n" "," "m" ")" -> ($#m1_hidden :::"Complex":::) equals :: CLVECT_3:def 6 (Set (Set "(" ($#k4_clvect_3 :::"Sum"::: ) "(" "Cseq" "," "n" ")" ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" ($#k4_clvect_3 :::"Sum"::: ) "(" "Cseq" "," "m" ")" ")" )); end; :: deftheorem defines :::"Sum"::: CLVECT_3:def 6 : (Bool "for" (Set (Var "Cseq")) "being" ($#m1_subset_1 :::"Complex_Sequence":::) (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k5_clvect_3 :::"Sum"::: ) "(" (Set (Var "Cseq")) "," (Set (Var "n")) "," (Set (Var "m")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_clvect_3 :::"Sum"::: ) "(" (Set (Var "Cseq")) "," (Set (Var "n")) ")" ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" ($#k4_clvect_3 :::"Sum"::: ) "(" (Set (Var "Cseq")) "," (Set (Var "m")) ")" ")" ))))); definitionlet "X" be ($#l1_csspace :::"ComplexUnitarySpace":::); let "seq" be ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "X")); attr "seq" is :::"absolutely_summable"::: means :: CLVECT_3:def 7 (Bool (Set ($#k2_clvect_2 :::"||."::: ) "seq" ($#k2_clvect_2 :::".||"::: ) ) "is" ($#v1_series_1 :::"summable"::: ) ); end; :: deftheorem defines :::"absolutely_summable"::: CLVECT_3:def 7 : (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "seq")) "is" ($#v2_clvect_3 :::"absolutely_summable"::: ) ) "iff" (Bool (Set ($#k2_clvect_2 :::"||."::: ) (Set (Var "seq")) ($#k2_clvect_2 :::".||"::: ) ) "is" ($#v1_series_1 :::"summable"::: ) ) ")" ))); theorem :: CLVECT_3:25 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (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_clvect_3 :::"absolutely_summable"::: ) ) & (Bool (Set (Var "seq2")) "is" ($#v2_clvect_3 :::"absolutely_summable"::: ) )) "holds" (Bool (Set (Set (Var "seq1")) ($#k16_csspace :::"+"::: ) (Set (Var "seq2"))) "is" ($#v2_clvect_3 :::"absolutely_summable"::: ) ))) ; theorem :: CLVECT_3:26 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "z")) "being" ($#m1_hidden :::"Complex":::) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v2_clvect_3 :::"absolutely_summable"::: ) )) "holds" (Bool (Set (Set (Var "z")) ($#k6_clvect_1 :::"*"::: ) (Set (Var "seq"))) "is" ($#v2_clvect_3 :::"absolutely_summable"::: ) )))) ; theorem :: CLVECT_3:27 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (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":::) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set ($#k2_clvect_2 :::"||."::: ) (Set (Var "seq")) ($#k2_clvect_2 :::".||"::: ) ) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "Rseq")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")))) ")" ) & (Bool (Set (Var "Rseq")) "is" ($#v1_series_1 :::"summable"::: ) )) "holds" (Bool (Set (Var "seq")) "is" ($#v2_clvect_3 :::"absolutely_summable"::: ) )))) ; theorem :: CLVECT_3:28 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (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":::) "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")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k13_csspace :::"||."::: ) (Set "(" (Set (Var "seq")) ($#k1_normsp_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k13_csspace :::".||"::: ) ) ($#k10_real_1 :::"/"::: ) (Set ($#k13_csspace :::"||."::: ) (Set "(" (Set (Var "seq")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k13_csspace :::".||"::: ) ))) ")" ) ")" ) & (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_clvect_3 :::"absolutely_summable"::: ) )))) ; theorem :: CLVECT_3:29 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "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 ($#k13_csspace :::"||."::: ) (Set "(" (Set (Var "seq")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k13_csspace :::".||"::: ) ) ($#r1_xxreal_0 :::">="::: ) (Set (Var "r"))))) & (Bool (Set (Var "seq")) "is" ($#v1_clvect_2 :::"convergent"::: ) )) "holds" (Bool (Set ($#k1_clvect_2 :::"lim"::: ) (Set (Var "seq"))) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X"))))))) ; theorem :: CLVECT_3:30 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (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 ($#k13_csspace :::"||."::: ) (Set "(" (Set (Var "seq")) ($#k1_normsp_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k13_csspace :::".||"::: ) ) ($#k10_real_1 :::"/"::: ) (Set ($#k13_csspace :::"||."::: ) (Set "(" (Set (Var "seq")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k13_csspace :::".||"::: ) )) ($#r1_xxreal_0 :::">="::: ) (Num 1))))) "holds" (Bool "not" (Bool (Set (Var "seq")) "is" ($#v1_clvect_3 :::"summable"::: ) )))) ; theorem :: CLVECT_3:31 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (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":::) "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")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k13_csspace :::"||."::: ) (Set "(" (Set (Var "seq")) ($#k1_normsp_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k13_csspace :::".||"::: ) ) ($#k10_real_1 :::"/"::: ) (Set ($#k13_csspace :::"||."::: ) (Set "(" (Set (Var "seq")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k13_csspace :::".||"::: ) ))) ")" ) & (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_clvect_3 :::"summable"::: ) ))))) ; theorem :: CLVECT_3:32 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (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":::) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "Rseq")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k2_power :::"-root"::: ) (Set ($#k13_csspace :::"||."::: ) (Set "(" (Set (Var "seq")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k13_csspace :::".||"::: ) ))) ")" ) & (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_clvect_3 :::"absolutely_summable"::: ) )))) ; theorem :: CLVECT_3:33 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (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":::) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "Rseq")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k2_power :::"-root"::: ) (Set "(" (Set ($#k2_clvect_2 :::"||."::: ) (Set (Var "seq")) ($#k2_clvect_2 :::".||"::: ) ) ($#k8_nat_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")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::">="::: ) (Num 1))))) "holds" (Bool "not" (Bool (Set (Var "seq")) "is" ($#v1_clvect_3 :::"summable"::: ) ))))) ; theorem :: CLVECT_3:34 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (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":::) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "Rseq")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k2_power :::"-root"::: ) (Set "(" (Set ($#k2_clvect_2 :::"||."::: ) (Set (Var "seq")) ($#k2_clvect_2 :::".||"::: ) ) ($#k8_nat_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_clvect_3 :::"summable"::: ) ))))) ; theorem :: CLVECT_3:35 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k3_series_1 :::"Partial_Sums"::: ) (Set ($#k2_clvect_2 :::"||."::: ) (Set (Var "seq")) ($#k2_clvect_2 :::".||"::: ) )) "is" ($#v7_valued_0 :::"non-decreasing"::: ) ))) ; theorem :: CLVECT_3:36 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (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_clvect_2 :::"||."::: ) (Set (Var "seq")) ($#k2_clvect_2 :::".||"::: ) ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))))) ; theorem :: CLVECT_3:37 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (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 ($#k13_csspace :::"||."::: ) (Set "(" (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set (Var "seq")) ")" ) ($#k1_normsp_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k13_csspace :::".||"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set ($#k2_clvect_2 :::"||."::: ) (Set (Var "seq")) ($#k2_clvect_2 :::".||"::: ) ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))))))) ; theorem :: CLVECT_3:38 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (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 ($#k13_csspace :::"||."::: ) (Set "(" ($#k2_clvect_3 :::"Sum"::: ) "(" (Set (Var "seq")) "," (Set (Var "n")) ")" ")" ) ($#k13_csspace :::".||"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_series_1 :::"Sum"::: ) "(" (Set ($#k2_clvect_2 :::"||."::: ) (Set (Var "seq")) ($#k2_clvect_2 :::".||"::: ) ) "," (Set (Var "n")) ")" ))))) ; theorem :: CLVECT_3:39 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (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 ($#k13_csspace :::"||."::: ) (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")) ")" ) ")" ) ($#k13_csspace :::".||"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set "(" (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set ($#k2_clvect_2 :::"||."::: ) (Set (Var "seq")) ($#k2_clvect_2 :::".||"::: ) ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "m")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set ($#k2_clvect_2 :::"||."::: ) (Set (Var "seq")) ($#k2_clvect_2 :::".||"::: ) ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) ")" )))))) ; theorem :: CLVECT_3:40 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (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 ($#k13_csspace :::"||."::: ) (Set "(" (Set "(" ($#k2_clvect_3 :::"Sum"::: ) "(" (Set (Var "seq")) "," (Set (Var "m")) ")" ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" ($#k2_clvect_3 :::"Sum"::: ) "(" (Set (Var "seq")) "," (Set (Var "n")) ")" ")" ) ")" ) ($#k13_csspace :::".||"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set "(" ($#k6_series_1 :::"Sum"::: ) "(" (Set ($#k2_clvect_2 :::"||."::: ) (Set (Var "seq")) ($#k2_clvect_2 :::".||"::: ) ) "," (Set (Var "m")) ")" ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k6_series_1 :::"Sum"::: ) "(" (Set ($#k2_clvect_2 :::"||."::: ) (Set (Var "seq")) ($#k2_clvect_2 :::".||"::: ) ) "," (Set (Var "n")) ")" ")" ) ")" )))))) ; theorem :: CLVECT_3:41 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (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 ($#k13_csspace :::"||."::: ) (Set "(" ($#k3_clvect_3 :::"Sum"::: ) "(" (Set (Var "seq")) "," (Set (Var "m")) "," (Set (Var "n")) ")" ")" ) ($#k13_csspace :::".||"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k18_complex1 :::"abs"::: ) (Set "(" ($#k7_series_1 :::"Sum"::: ) "(" (Set ($#k2_clvect_2 :::"||."::: ) (Set (Var "seq")) ($#k2_clvect_2 :::".||"::: ) ) "," (Set (Var "m")) "," (Set (Var "n")) ")" ")" )))))) ; theorem :: CLVECT_3:42 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexHilbertSpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v2_clvect_3 :::"absolutely_summable"::: ) )) "holds" (Bool (Set (Var "seq")) "is" ($#v1_clvect_3 :::"summable"::: ) ))) ; definitionlet "X" be ($#l1_csspace :::"ComplexUnitarySpace":::); let "seq" be ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "X")); let "Cseq" be ($#m1_subset_1 :::"Complex_Sequence":::); func "Cseq" :::"*"::: "seq" -> ($#m1_subset_1 :::"sequence":::) "of" "X" means :: CLVECT_3:def 8 (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 "(" "Cseq" ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k1_clvect_1 :::"*"::: ) (Set "(" "seq" ($#k1_normsp_1 :::"."::: ) (Set (Var "n")) ")" )))); end; :: deftheorem defines :::"*"::: CLVECT_3:def 8 : (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "Cseq")) "being" ($#m1_subset_1 :::"Complex_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 "Cseq")) ($#k6_clvect_3 :::"*"::: ) (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 "Cseq")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k1_clvect_1 :::"*"::: ) (Set "(" (Set (Var "seq")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n")) ")" )))) ")" ))))); theorem :: CLVECT_3:43 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (Bool "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "Cseq")) "being" ($#m1_subset_1 :::"Complex_Sequence":::) "holds" (Bool (Set (Set (Var "Cseq")) ($#k6_clvect_3 :::"*"::: ) (Set "(" (Set (Var "seq1")) ($#k16_csspace :::"+"::: ) (Set (Var "seq2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "Cseq")) ($#k6_clvect_3 :::"*"::: ) (Set (Var "seq1")) ")" ) ($#k16_csspace :::"+"::: ) (Set "(" (Set (Var "Cseq")) ($#k6_clvect_3 :::"*"::: ) (Set (Var "seq2")) ")" )))))) ; theorem :: CLVECT_3:44 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "Cseq1")) "," (Set (Var "Cseq2")) "being" ($#m1_subset_1 :::"Complex_Sequence":::) "holds" (Bool (Set (Set "(" (Set (Var "Cseq1")) ($#k1_series_1 :::"+"::: ) (Set (Var "Cseq2")) ")" ) ($#k6_clvect_3 :::"*"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "Cseq1")) ($#k6_clvect_3 :::"*"::: ) (Set (Var "seq")) ")" ) ($#k16_csspace :::"+"::: ) (Set "(" (Set (Var "Cseq2")) ($#k6_clvect_3 :::"*"::: ) (Set (Var "seq")) ")" )))))) ; theorem :: CLVECT_3:45 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "Cseq1")) "," (Set (Var "Cseq2")) "being" ($#m1_subset_1 :::"Complex_Sequence":::) "holds" (Bool (Set (Set "(" (Set (Var "Cseq1")) ($#k19_valued_1 :::"(#)"::: ) (Set (Var "Cseq2")) ")" ) ($#k6_clvect_3 :::"*"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "Cseq1")) ($#k6_clvect_3 :::"*"::: ) (Set "(" (Set (Var "Cseq2")) ($#k6_clvect_3 :::"*"::: ) (Set (Var "seq")) ")" )))))) ; theorem :: CLVECT_3:46 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "Cseq")) "being" ($#m1_subset_1 :::"Complex_Sequence":::) (Bool "for" (Set (Var "z")) "being" ($#m1_hidden :::"Complex":::) "holds" (Bool (Set (Set "(" (Set (Var "z")) ($#k25_valued_1 :::"(#)"::: ) (Set (Var "Cseq")) ")" ) ($#k6_clvect_3 :::"*"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "z")) ($#k6_clvect_1 :::"*"::: ) (Set "(" (Set (Var "Cseq")) ($#k6_clvect_3 :::"*"::: ) (Set (Var "seq")) ")" ))))))) ; theorem :: CLVECT_3:47 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "Cseq")) "being" ($#m1_subset_1 :::"Complex_Sequence":::) "holds" (Bool (Set (Set (Var "Cseq")) ($#k6_clvect_3 :::"*"::: ) (Set "(" ($#k5_vfunct_1 :::"-"::: ) (Set (Var "seq")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k31_valued_1 :::"-"::: ) (Set (Var "Cseq")) ")" ) ($#k6_clvect_3 :::"*"::: ) (Set (Var "seq"))))))) ; theorem :: CLVECT_3:48 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "Cseq")) "being" ($#m1_subset_1 :::"Complex_Sequence":::) "st" (Bool (Bool (Set (Var "Cseq")) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set (Var "seq")) "is" ($#v1_clvect_2 :::"convergent"::: ) )) "holds" (Bool (Set (Set (Var "Cseq")) ($#k6_clvect_3 :::"*"::: ) (Set (Var "seq"))) "is" ($#v1_clvect_2 :::"convergent"::: ) )))) ; theorem :: CLVECT_3:49 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "Cseq")) "being" ($#m1_subset_1 :::"Complex_Sequence":::) "st" (Bool (Bool (Set (Var "Cseq")) "is" ($#v1_comseq_2 :::"bounded"::: ) ) & (Bool (Set (Var "seq")) "is" ($#v3_clvect_2 :::"bounded"::: ) )) "holds" (Bool (Set (Set (Var "Cseq")) ($#k6_clvect_3 :::"*"::: ) (Set (Var "seq"))) "is" ($#v3_clvect_2 :::"bounded"::: ) )))) ; theorem :: CLVECT_3:50 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "Cseq")) "being" ($#m1_subset_1 :::"Complex_Sequence":::) "st" (Bool (Bool (Set (Var "Cseq")) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set (Var "seq")) "is" ($#v1_clvect_2 :::"convergent"::: ) )) "holds" (Bool "(" (Bool (Set (Set (Var "Cseq")) ($#k6_clvect_3 :::"*"::: ) (Set (Var "seq"))) "is" ($#v1_clvect_2 :::"convergent"::: ) ) & (Bool (Set ($#k1_clvect_2 :::"lim"::: ) (Set "(" (Set (Var "Cseq")) ($#k6_clvect_3 :::"*"::: ) (Set (Var "seq")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_comseq_2 :::"lim"::: ) (Set (Var "Cseq")) ")" ) ($#k1_clvect_1 :::"*"::: ) (Set "(" ($#k1_clvect_2 :::"lim"::: ) (Set (Var "seq")) ")" ))) ")" )))) ; definitionlet "Cseq" be ($#m1_subset_1 :::"Complex_Sequence":::); attr "Cseq" is :::"Cauchy"::: means :: CLVECT_3:def 9 (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 ($#k17_complex1 :::"|."::: ) (Set "(" (Set "(" "Cseq" ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k11_complex1 :::"-"::: ) (Set "(" "Cseq" ($#k8_nat_1 :::"."::: ) (Set (Var "m")) ")" ) ")" ) ($#k17_complex1 :::".|"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r")))))); end; :: deftheorem defines :::"Cauchy"::: CLVECT_3:def 9 : (Bool "for" (Set (Var "Cseq")) "being" ($#m1_subset_1 :::"Complex_Sequence":::) "holds" (Bool "(" (Bool (Set (Var "Cseq")) "is" ($#v3_clvect_3 :::"Cauchy"::: ) ) "iff" (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "ex" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Set (Var "k"))) & (Bool (Set (Var "m")) ($#r1_xxreal_0 :::">="::: ) (Set (Var "k")))) "holds" (Bool (Set ($#k17_complex1 :::"|."::: ) (Set "(" (Set "(" (Set (Var "Cseq")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k11_complex1 :::"-"::: ) (Set "(" (Set (Var "Cseq")) ($#k8_nat_1 :::"."::: ) (Set (Var "m")) ")" ) ")" ) ($#k17_complex1 :::".|"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r")))))) ")" )); theorem :: CLVECT_3:51 (Bool "for" (Set (Var "Cseq")) "being" ($#m1_subset_1 :::"Complex_Sequence":::) (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexHilbertSpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v2_clvect_2 :::"Cauchy"::: ) ) & (Bool (Set (Var "Cseq")) "is" ($#v3_clvect_3 :::"Cauchy"::: ) )) "holds" (Bool (Set (Set (Var "Cseq")) ($#k6_clvect_3 :::"*"::: ) (Set (Var "seq"))) "is" ($#v2_clvect_2 :::"Cauchy"::: ) )))) ; theorem :: CLVECT_3:52 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "Cseq")) "being" ($#m1_subset_1 :::"Complex_Sequence":::) (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 "Cseq")) ($#k46_valued_1 :::"-"::: ) (Set "(" (Set (Var "Cseq")) ($#k1_valued_0 :::"^\"::: ) (Num 1) ")" ) ")" ) ($#k6_clvect_3 :::"*"::: ) (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 "Cseq")) ($#k6_clvect_3 :::"*"::: ) (Set (Var "seq")) ")" ) ")" ) ($#k1_normsp_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set "(" (Set (Var "Cseq")) ($#k6_clvect_3 :::"*"::: ) (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set (Var "seq")) ")" ) ")" ) ($#k1_normsp_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ))))))) ; theorem :: CLVECT_3:53 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "Cseq")) "being" ($#m1_subset_1 :::"Complex_Sequence":::) (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 "Cseq")) ($#k6_clvect_3 :::"*"::: ) (Set (Var "seq")) ")" ) ")" ) ($#k1_normsp_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "Cseq")) ($#k6_clvect_3 :::"*"::: ) (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 "Cseq")) ($#k1_valued_0 :::"^\"::: ) (Num 1) ")" ) ($#k46_valued_1 :::"-"::: ) (Set (Var "Cseq")) ")" ) ($#k6_clvect_3 :::"*"::: ) (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set (Var "seq")) ")" ) ")" ) ")" ) ($#k1_normsp_1 :::"."::: ) (Set (Var "n")) ")" ))))))) ; theorem :: CLVECT_3:54 (Bool "for" (Set (Var "X")) "being" ($#l1_csspace :::"ComplexUnitarySpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "Cseq")) "being" ($#m1_subset_1 :::"Complex_Sequence":::) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k2_clvect_3 :::"Sum"::: ) "(" (Set "(" (Set (Var "Cseq")) ($#k6_clvect_3 :::"*"::: ) (Set (Var "seq")) ")" ) "," (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "Cseq")) ($#k6_clvect_3 :::"*"::: ) (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 "(" ($#k2_clvect_3 :::"Sum"::: ) "(" (Set "(" (Set "(" (Set "(" (Set (Var "Cseq")) ($#k1_valued_0 :::"^\"::: ) (Num 1) ")" ) ($#k46_valued_1 :::"-"::: ) (Set (Var "Cseq")) ")" ) ($#k6_clvect_3 :::"*"::: ) (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set (Var "seq")) ")" ) ")" ) "," (Set (Var "n")) ")" ")" ))))))) ;