:: LOPBAN_3 semantic presentation begin theorem :: LOPBAN_3:1 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_normsp_1 :::"NORMSTR"::: ) (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")))) ")" )) "holds" (Bool "for" (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set (Var "seq")) ")" ) ($#k1_normsp_1 :::"."::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X"))))))) ; definitionlet "X" be ($#l1_normsp_1 :::"RealNormSpace":::); let "seq" be ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "X")); attr "seq" is :::"summable"::: means :: LOPBAN_3:def 1 (Bool (Set ($#k1_bhsp_4 :::"Partial_Sums"::: ) "seq") "is" ($#v3_normsp_1 :::"convergent"::: ) ); end; :: deftheorem defines :::"summable"::: LOPBAN_3:def 1 : (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "seq")) "is" ($#v1_lopban_3 :::"summable"::: ) ) "iff" (Bool (Set ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set (Var "seq"))) "is" ($#v3_normsp_1 :::"convergent"::: ) ) ")" ))); registrationlet "X" be ($#l1_normsp_1 :::"RealNormSpace":::); cluster bbbadV1_XBOOLE_0() ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X") ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_PARTFUN1((Set ($#k5_numbers :::"NAT"::: ) )) bbbadV1_FUNCT_2((Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X")) ($#v1_lopban_3 :::"summable"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1((Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X"))))); end; definitionlet "X" be ($#l1_normsp_1 :::"RealNormSpace":::); let "seq" be ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "X")); func :::"Sum"::: "seq" -> ($#m1_subset_1 :::"Element":::) "of" "X" equals :: LOPBAN_3:def 2 (Set ($#k6_normsp_1 :::"lim"::: ) (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) "seq" ")" )); end; :: deftheorem defines :::"Sum"::: LOPBAN_3:def 2 : (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k1_lopban_3 :::"Sum"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set ($#k6_normsp_1 :::"lim"::: ) (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set (Var "seq")) ")" ))))); definitionlet "X" be ($#l1_normsp_1 :::"RealNormSpace":::); let "seq" be ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "X")); attr "seq" is :::"norm_summable"::: means :: LOPBAN_3:def 3 (Bool (Set ($#k4_normsp_0 :::"||."::: ) "seq" ($#k4_normsp_0 :::".||"::: ) ) "is" ($#v1_series_1 :::"summable"::: ) ); end; :: deftheorem defines :::"norm_summable"::: LOPBAN_3:def 3 : (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "seq")) "is" ($#v2_lopban_3 :::"norm_summable"::: ) ) "iff" (Bool (Set ($#k4_normsp_0 :::"||."::: ) (Set (Var "seq")) ($#k4_normsp_0 :::".||"::: ) ) "is" ($#v1_series_1 :::"summable"::: ) ) ")" ))); theorem :: LOPBAN_3:2 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set ($#k4_normsp_0 :::"||."::: ) (Set (Var "seq")) ($#k4_normsp_0 :::".||"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "m"))))))) ; theorem :: LOPBAN_3:3 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set (Var "x")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "y")) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "z")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "z")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "y")) ")" ) ")" ) ($#k1_normsp_0 :::".||"::: ) )))) ; theorem :: LOPBAN_3:4 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v3_normsp_1 :::"convergent"::: ) )) "holds" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "s")))) "holds" (Bool "ex" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "for" (Set (Var "m")) "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 ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set "(" (Set (Var "seq")) ($#k1_normsp_1 :::"."::: ) (Set (Var "m")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "seq")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n")) ")" ) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "s")))))))) ; theorem :: LOPBAN_3:5 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "seq")) "is" ($#v1_rsspace3 :::"Cauchy_sequence_by_Norm"::: ) ) "iff" (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "p")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "ex" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "for" (Set (Var "m")) "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 ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set "(" (Set (Var "seq")) ($#k1_normsp_1 :::"."::: ) (Set (Var "m")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "seq")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n")) ")" ) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "p")))))) ")" ))) ; theorem :: LOPBAN_3:6 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (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")))) ")" )) "holds" (Bool "for" (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set ($#k4_normsp_0 :::"||."::: ) (Set (Var "seq")) ($#k4_normsp_0 :::".||"::: ) ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))))) ; theorem :: LOPBAN_3:7 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "seq")) "," (Set (Var "seq1")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "seq1")) "is" ($#m2_valued_0 :::"subsequence"::: ) "of" (Set (Var "seq"))) & (Bool (Set (Var "seq")) "is" ($#v3_normsp_1 :::"convergent"::: ) )) "holds" (Bool (Set (Var "seq1")) "is" ($#v3_normsp_1 :::"convergent"::: ) ))) ; theorem :: LOPBAN_3:8 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "seq")) "," (Set (Var "seq1")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "seq1")) "is" ($#m2_valued_0 :::"subsequence"::: ) "of" (Set (Var "seq"))) & (Bool (Set (Var "seq")) "is" ($#v3_normsp_1 :::"convergent"::: ) )) "holds" (Bool (Set ($#k6_normsp_1 :::"lim"::: ) (Set (Var "seq1"))) ($#r1_hidden :::"="::: ) (Set ($#k6_normsp_1 :::"lim"::: ) (Set (Var "seq")))))) ; theorem :: LOPBAN_3:9 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "seq")) "," (Set (Var "seq1")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v3_normsp_1 :::"convergent"::: ) )) "holds" (Bool "(" (Bool (Set (Set (Var "seq")) ($#k1_valued_0 :::"^\"::: ) (Set (Var "k"))) "is" ($#v3_normsp_1 :::"convergent"::: ) ) & (Bool (Set ($#k6_normsp_1 :::"lim"::: ) (Set "(" (Set (Var "seq")) ($#k1_valued_0 :::"^\"::: ) (Set (Var "k")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_normsp_1 :::"lim"::: ) (Set (Var "seq")))) ")" )))) ; theorem :: LOPBAN_3:10 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "seq")) "," (Set (Var "seq1")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v3_normsp_1 :::"convergent"::: ) ) & (Bool "ex" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Set (Var "seq")) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "seq1")) ($#k1_valued_0 :::"^\"::: ) (Set (Var "k")))))) "holds" (Bool (Set (Var "seq1")) "is" ($#v3_normsp_1 :::"convergent"::: ) ))) ; theorem :: LOPBAN_3:11 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "seq")) "," (Set (Var "seq1")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v3_normsp_1 :::"convergent"::: ) ) & (Bool "ex" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Set (Var "seq")) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "seq1")) ($#k1_valued_0 :::"^\"::: ) (Set (Var "k")))))) "holds" (Bool (Set ($#k6_normsp_1 :::"lim"::: ) (Set (Var "seq1"))) ($#r1_hidden :::"="::: ) (Set ($#k6_normsp_1 :::"lim"::: ) (Set (Var "seq")))))) ; theorem :: LOPBAN_3:12 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v3_funct_1 :::"constant"::: ) )) "holds" (Bool (Set (Var "seq")) "is" ($#v3_normsp_1 :::"convergent"::: ) ))) ; theorem :: LOPBAN_3:13 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (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")))) ")" )) "holds" (Bool (Set (Var "seq")) "is" ($#v2_lopban_3 :::"norm_summable"::: ) ))) ; registrationlet "X" be ($#l1_normsp_1 :::"RealNormSpace":::); cluster bbbadV1_XBOOLE_0() ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X") ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_PARTFUN1((Set ($#k5_numbers :::"NAT"::: ) )) bbbadV1_FUNCT_2((Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X")) ($#v2_lopban_3 :::"norm_summable"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1((Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X"))))); end; theorem :: LOPBAN_3:14 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "s")) "is" ($#v1_lopban_3 :::"summable"::: ) )) "holds" (Bool "(" (Bool (Set (Var "s")) "is" ($#v3_normsp_1 :::"convergent"::: ) ) & (Bool (Set ($#k6_normsp_1 :::"lim"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X")))) ")" ))) ; theorem :: LOPBAN_3:15 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set (Var "s1")) ")" ) ($#k2_normsp_1 :::"+"::: ) (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set (Var "s2")) ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set "(" (Set (Var "s1")) ($#k2_normsp_1 :::"+"::: ) (Set (Var "s2")) ")" ))))) ; theorem :: LOPBAN_3:16 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set (Var "s1")) ")" ) ($#k3_normsp_1 :::"-"::: ) (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set (Var "s2")) ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set "(" (Set (Var "s1")) ($#k3_normsp_1 :::"-"::: ) (Set (Var "s2")) ")" ))))) ; registrationlet "X" be ($#l1_normsp_1 :::"RealNormSpace":::); let "seq" be ($#v2_lopban_3 :::"norm_summable"::: ) ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "X")); cluster (Set ($#k2_normsp_0 :::"||."::: ) "seq" ($#k2_normsp_0 :::".||"::: ) ) -> ($#v1_series_1 :::"summable"::: ) for ($#m1_subset_1 :::"Real_Sequence":::); end; registrationlet "X" be ($#l1_normsp_1 :::"RealNormSpace":::); cluster ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_FUNCT_2((Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X")) ($#v1_lopban_3 :::"summable"::: ) -> ($#v3_normsp_1 :::"convergent"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1((Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X"))))); end; theorem :: LOPBAN_3:17 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (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_lopban_3 :::"summable"::: ) ) & (Bool (Set (Var "seq2")) "is" ($#v1_lopban_3 :::"summable"::: ) )) "holds" (Bool "(" (Bool (Set (Set (Var "seq1")) ($#k2_normsp_1 :::"+"::: ) (Set (Var "seq2"))) "is" ($#v1_lopban_3 :::"summable"::: ) ) & (Bool (Set ($#k1_lopban_3 :::"Sum"::: ) (Set "(" (Set (Var "seq1")) ($#k2_normsp_1 :::"+"::: ) (Set (Var "seq2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_lopban_3 :::"Sum"::: ) (Set (Var "seq1")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" ($#k1_lopban_3 :::"Sum"::: ) (Set (Var "seq2")) ")" ))) ")" ))) ; theorem :: LOPBAN_3:18 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (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_lopban_3 :::"summable"::: ) ) & (Bool (Set (Var "seq2")) "is" ($#v1_lopban_3 :::"summable"::: ) )) "holds" (Bool "(" (Bool (Set (Set (Var "seq1")) ($#k3_normsp_1 :::"-"::: ) (Set (Var "seq2"))) "is" ($#v1_lopban_3 :::"summable"::: ) ) & (Bool (Set ($#k1_lopban_3 :::"Sum"::: ) (Set "(" (Set (Var "seq1")) ($#k3_normsp_1 :::"-"::: ) (Set (Var "seq2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_lopban_3 :::"Sum"::: ) (Set (Var "seq1")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" ($#k1_lopban_3 :::"Sum"::: ) (Set (Var "seq2")) ")" ))) ")" ))) ; registrationlet "X" be ($#l1_normsp_1 :::"RealNormSpace":::); let "seq1", "seq2" be ($#v1_lopban_3 :::"summable"::: ) ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "X")); cluster (Set "seq1" ($#k2_normsp_1 :::"+"::: ) "seq2") -> ($#v1_lopban_3 :::"summable"::: ) ; cluster (Set "seq1" ($#k3_normsp_1 :::"-"::: ) "seq2") -> ($#v1_lopban_3 :::"summable"::: ) ; end; theorem :: LOPBAN_3:19 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set "(" (Set (Var "z")) ($#k5_normsp_1 :::"*"::: ) (Set (Var "seq")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "z")) ($#k5_normsp_1 :::"*"::: ) (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set (Var "seq")) ")" )))))) ; theorem :: LOPBAN_3:20 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "seq")) "being" ($#v1_lopban_3 :::"summable"::: ) ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" (Bool (Set (Set (Var "z")) ($#k5_normsp_1 :::"*"::: ) (Set (Var "seq"))) "is" ($#v1_lopban_3 :::"summable"::: ) ) & (Bool (Set ($#k1_lopban_3 :::"Sum"::: ) (Set "(" (Set (Var "z")) ($#k5_normsp_1 :::"*"::: ) (Set (Var "seq")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "z")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" ($#k1_lopban_3 :::"Sum"::: ) (Set (Var "seq")) ")" ))) ")" )))) ; registrationlet "X" be ($#l1_normsp_1 :::"RealNormSpace":::); let "z" be ($#m1_subset_1 :::"Real":::); let "seq" be ($#v1_lopban_3 :::"summable"::: ) ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "X")); cluster (Set "z" ($#k5_normsp_1 :::"*"::: ) "seq") -> ($#v1_lopban_3 :::"summable"::: ) ; end; theorem :: LOPBAN_3:21 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "s")) "," (Set (Var "s1")) "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 "s1")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_normsp_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ))) ")" )) "holds" (Bool (Set ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set "(" (Set (Var "s")) ($#k1_valued_0 :::"^\"::: ) (Num 1) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set (Var "s")) ")" ) ($#k1_valued_0 :::"^\"::: ) (Num 1) ")" ) ($#k3_normsp_1 :::"-"::: ) (Set (Var "s1")))))) ; theorem :: LOPBAN_3:22 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "s")) "is" ($#v1_lopban_3 :::"summable"::: ) )) "holds" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "s")) ($#k1_valued_0 :::"^\"::: ) (Set (Var "n"))) "is" ($#v1_lopban_3 :::"summable"::: ) )))) ; registrationlet "X" be ($#l1_normsp_1 :::"RealNormSpace":::); let "seq" be ($#v1_lopban_3 :::"summable"::: ) ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "X")); let "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster (Set "seq" ($#k9_nat_1 :::"^\"::: ) "n") -> ($#v1_lopban_3 :::"summable"::: ) for ($#m1_subset_1 :::"sequence":::) "of" "X"; end; theorem :: LOPBAN_3:23 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set ($#k3_series_1 :::"Partial_Sums"::: ) (Set ($#k4_normsp_0 :::"||."::: ) (Set (Var "seq")) ($#k4_normsp_0 :::".||"::: ) )) "is" ($#v1_seq_2 :::"bounded_above"::: ) ) "iff" (Bool (Set (Var "seq")) "is" ($#v2_lopban_3 :::"norm_summable"::: ) ) ")" ))) ; registrationlet "X" be ($#l1_normsp_1 :::"RealNormSpace":::); let "seq" be ($#v2_lopban_3 :::"norm_summable"::: ) ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "X")); cluster (Set ($#k2_series_1 :::"Partial_Sums"::: ) (Set ($#k4_normsp_0 :::"||."::: ) "seq" ($#k4_normsp_0 :::".||"::: ) )) -> ($#v1_seq_2 :::"bounded_above"::: ) for ($#m1_subset_1 :::"Real_Sequence":::); end; theorem :: LOPBAN_3:24 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealBanachSpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "seq")) "is" ($#v1_lopban_3 :::"summable"::: ) ) "iff" (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "p")))) "holds" (Bool "ex" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "for" (Set (Var "m")) "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 ($#k1_normsp_0 :::"||."::: ) (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")) ")" ) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "p")))))) ")" ))) ; theorem :: LOPBAN_3:25 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "s")) "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"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m")))) "holds" (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set "(" (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set (Var "s")) ")" ) ($#k1_normsp_1 :::"."::: ) (Set (Var "m")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set "(" ($#k1_bhsp_4 :::"Partial_Sums"::: ) (Set (Var "s")) ")" ) ($#k1_normsp_1 :::"."::: ) (Set (Var "n")) ")" ) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set "(" (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set ($#k4_normsp_0 :::"||."::: ) (Set (Var "s")) ($#k4_normsp_0 :::".||"::: ) ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "m")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set ($#k4_normsp_0 :::"||."::: ) (Set (Var "s")) ($#k4_normsp_0 :::".||"::: ) ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "n")) ")" ) ")" )))))) ; theorem :: LOPBAN_3:26 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealBanachSpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v2_lopban_3 :::"norm_summable"::: ) )) "holds" (Bool (Set (Var "seq")) "is" ($#v1_lopban_3 :::"summable"::: ) ))) ; theorem :: LOPBAN_3:27 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "rseq1")) "being" ($#m1_subset_1 :::"Real_Sequence":::) (Bool "for" (Set (Var "seq2")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "rseq1")) "is" ($#v1_series_1 :::"summable"::: ) ) & (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 "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set (Var "seq2")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "rseq1")) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))))))) "holds" (Bool (Set (Var "seq2")) "is" ($#v2_lopban_3 :::"norm_summable"::: ) )))) ; theorem :: LOPBAN_3:28 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "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 ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set ($#k4_normsp_0 :::"||."::: ) (Set (Var "seq1")) ($#k4_normsp_0 :::".||"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Set ($#k4_normsp_0 :::"||."::: ) (Set (Var "seq1")) ($#k4_normsp_0 :::".||"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set ($#k4_normsp_0 :::"||."::: ) (Set (Var "seq2")) ($#k4_normsp_0 :::".||"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "n")))) ")" ) ")" ) & (Bool (Set (Var "seq2")) "is" ($#v2_lopban_3 :::"norm_summable"::: ) )) "holds" (Bool "(" (Bool (Set (Var "seq1")) "is" ($#v2_lopban_3 :::"norm_summable"::: ) ) & (Bool (Set ($#k4_series_1 :::"Sum"::: ) (Set ($#k4_normsp_0 :::"||."::: ) (Set (Var "seq1")) ($#k4_normsp_0 :::".||"::: ) )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k4_series_1 :::"Sum"::: ) (Set ($#k4_normsp_0 :::"||."::: ) (Set (Var "seq2")) ($#k4_normsp_0 :::".||"::: ) ))) ")" ))) ; theorem :: LOPBAN_3:29 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (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 ($#k4_normsp_0 :::"||."::: ) (Set (Var "seq")) ($#k4_normsp_0 :::".||"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#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 (Set "(" (Set ($#k4_normsp_0 :::"||."::: ) (Set (Var "seq")) ($#k4_normsp_0 :::".||"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set ($#k4_normsp_0 :::"||."::: ) (Set (Var "seq")) ($#k4_normsp_0 :::".||"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "n")) ")" )) ($#r1_xxreal_0 :::">="::: ) (Num 1))))) "holds" (Bool "not" (Bool (Set (Var "seq")) "is" ($#v2_lopban_3 :::"norm_summable"::: ) )))) ; theorem :: LOPBAN_3:30 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "rseq1")) "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 "rseq1")) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k2_power :::"-root"::: ) (Set "(" (Set ($#k4_normsp_0 :::"||."::: ) (Set (Var "seq")) ($#k4_normsp_0 :::".||"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "n")) ")" ))) ")" ) & (Bool (Set (Var "rseq1")) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set (Var "rseq1"))) ($#r1_xxreal_0 :::"<"::: ) (Num 1))) "holds" (Bool (Set (Var "seq")) "is" ($#v2_lopban_3 :::"norm_summable"::: ) )))) ; theorem :: LOPBAN_3:31 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "rseq1")) "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 "rseq1")) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k2_power :::"-root"::: ) (Set "(" (Set ($#k4_normsp_0 :::"||."::: ) (Set (Var "seq")) ($#k4_normsp_0 :::".||"::: ) ) ($#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 "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool (Set (Set (Var "rseq1")) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::">="::: ) (Num 1))))) "holds" (Bool "not" (Bool (Set ($#k4_normsp_0 :::"||."::: ) (Set (Var "seq")) ($#k4_normsp_0 :::".||"::: ) ) "is" ($#v1_series_1 :::"summable"::: ) ))))) ; theorem :: LOPBAN_3:32 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "rseq1")) "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 "rseq1")) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k2_power :::"-root"::: ) (Set "(" (Set ($#k4_normsp_0 :::"||."::: ) (Set (Var "seq")) ($#k4_normsp_0 :::".||"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "n")) ")" ))) ")" ) & (Bool (Set (Var "rseq1")) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set (Var "rseq1"))) ($#r1_xxreal_0 :::">"::: ) (Num 1))) "holds" (Bool "not" (Bool (Set (Var "seq")) "is" ($#v2_lopban_3 :::"norm_summable"::: ) ))))) ; theorem :: LOPBAN_3:33 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "rseq1")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set ($#k4_normsp_0 :::"||."::: ) (Set (Var "seq")) ($#k4_normsp_0 :::".||"::: ) ) "is" ($#v8_valued_0 :::"non-increasing"::: ) ) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "rseq1")) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 2) ($#k4_power :::"to_power"::: ) (Set (Var "n")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set ($#k4_normsp_0 :::"||."::: ) (Set (Var "seq")) ($#k4_normsp_0 :::".||"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" (Num 2) ($#k4_power :::"to_power"::: ) (Set (Var "n")) ")" ) ")" ))) ")" )) "holds" (Bool "(" (Bool (Set (Var "seq")) "is" ($#v2_lopban_3 :::"norm_summable"::: ) ) "iff" (Bool (Set (Var "rseq1")) "is" ($#v1_series_1 :::"summable"::: ) ) ")" )))) ; theorem :: LOPBAN_3:34 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "p")) ($#r1_xxreal_0 :::">"::: ) (Num 1)) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Num 1))) "holds" (Bool (Set (Set ($#k4_normsp_0 :::"||."::: ) (Set (Var "seq")) ($#k4_normsp_0 :::".||"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" (Set (Var "n")) ($#k4_power :::"to_power"::: ) (Set (Var "p")) ")" ))) ")" )) "holds" (Bool (Set (Var "seq")) "is" ($#v2_lopban_3 :::"norm_summable"::: ) )))) ; theorem :: LOPBAN_3:35 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "p")) ($#r1_xxreal_0 :::"<="::: ) (Num 1)) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Num 1))) "holds" (Bool (Set (Set ($#k4_normsp_0 :::"||."::: ) (Set (Var "seq")) ($#k4_normsp_0 :::".||"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" (Set (Var "n")) ($#k4_power :::"to_power"::: ) (Set (Var "p")) ")" ))) ")" )) "holds" (Bool "not" (Bool (Set (Var "seq")) "is" ($#v2_lopban_3 :::"norm_summable"::: ) ))))) ; theorem :: LOPBAN_3:36 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "rseq1")) "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 "rseq1")) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k4_normsp_0 :::"||."::: ) (Set (Var "seq")) ($#k4_normsp_0 :::".||"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set ($#k4_normsp_0 :::"||."::: ) (Set (Var "seq")) ($#k4_normsp_0 :::".||"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "n")) ")" ))) ")" ) ")" ) & (Bool (Set (Var "rseq1")) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set (Var "rseq1"))) ($#r1_xxreal_0 :::"<"::: ) (Num 1))) "holds" (Bool (Set (Var "seq")) "is" ($#v2_lopban_3 :::"norm_summable"::: ) )))) ; theorem :: LOPBAN_3:37 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (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 "(" (Set ($#k4_normsp_0 :::"||."::: ) (Set (Var "seq")) ($#k4_normsp_0 :::".||"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set ($#k4_normsp_0 :::"||."::: ) (Set (Var "seq")) ($#k4_normsp_0 :::".||"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "n")) ")" )) ($#r1_xxreal_0 :::">="::: ) (Num 1))))) "holds" (Bool "not" (Bool (Set (Var "seq")) "is" ($#v2_lopban_3 :::"norm_summable"::: ) )))) ; registrationlet "X" be ($#l1_normsp_1 :::"RealBanachSpace":::); cluster ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_FUNCT_2((Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X")) ($#v2_lopban_3 :::"norm_summable"::: ) -> ($#v1_lopban_3 :::"summable"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1((Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X"))))); end; begin theorem :: LOPBAN_3:38 (Bool "for" (Set (Var "X")) "being" ($#l1_lopban_2 :::"Banach_Algebra":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" (Bool (Set (Set (Var "x")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "x")))) & (Bool (Set (Set "(" (Set (Var "x")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "y")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "z")) ")" ))) & (Bool (Set (Set (Var "x")) ($#k3_rlvect_1 :::"+"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool "ex" (Set (Var "t")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "st" (Bool (Set (Set (Var "x")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X"))))) & (Bool (Set (Set "(" (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "y")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "z")) ")" ))) & (Bool (Set (Num 1) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Set ($#k6_numbers :::"0"::: ) ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X")))) & (Bool (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X")))) & (Bool (Set (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set (Var "x")))) & (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set "(" ($#k5_struct_0 :::"1."::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Set "(" ($#k5_struct_0 :::"1."::: ) (Set (Var "X")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "y")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "z")) ")" ))) & (Bool (Set (Set "(" (Set (Var "y")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "z")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "y")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "x")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "z")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "x")) ")" ))) & (Bool (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y")))) & (Bool (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "y")) ")" ))) & (Bool (Set (Set "(" (Set (Var "a")) ($#k7_real_1 :::"+"::: ) (Set (Var "b")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x")) ")" ))) & (Bool (Set (Set "(" (Set (Var "a")) ($#k8_real_1 :::"*"::: ) (Set (Var "b")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set (Var "b")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x")) ")" ))) & (Bool (Set (Set "(" (Set (Var "a")) ($#k8_real_1 :::"*"::: ) (Set (Var "b")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "b")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "y")) ")" ))) & (Bool (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "y")) ")" ))) & (Bool (Set (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X")))) & (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X")))) & (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "y")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "z")) ")" ))) & (Bool (Set (Set "(" (Set (Var "y")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "z")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "y")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "x")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "z")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "x")) ")" ))) & (Bool (Set (Set "(" (Set (Var "x")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "y")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "z")) ")" ))) & (Bool (Set (Set "(" (Set (Var "x")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "y")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "y")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "z")) ")" ))) & (Bool (Set (Set "(" (Set (Var "x")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "y")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "y")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "z")) ")" ))) & (Bool (Set (Set (Var "x")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "z")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "z")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "y")) ")" ))) & (Bool (Set (Set (Var "x")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "z")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "z")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "y")) ")" ))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "y")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "y")))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "y")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "x")) ")" ))) & "(" (Bool (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "x")) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X")))) ")" & "(" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "X"))))) "implies" (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "x")) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" & (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k18_complex1 :::"abs"::: ) (Set (Var "a")) ")" ) ($#k8_real_1 :::"*"::: ) (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "x")) ($#k1_normsp_0 :::".||"::: ) ))) & (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set (Var "x")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "y")) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "x")) ($#k1_normsp_0 :::".||"::: ) ) ($#k7_real_1 :::"+"::: ) (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "y")) ($#k1_normsp_0 :::".||"::: ) ))) & (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y")) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "x")) ($#k1_normsp_0 :::".||"::: ) ) ($#k8_real_1 :::"*"::: ) (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "y")) ($#k1_normsp_0 :::".||"::: ) ))) & (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" ($#k5_struct_0 :::"1."::: ) (Set (Var "X")) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Var "X")) "is" ($#v3_lopban_1 :::"complete"::: ) ) ")" )))) ; registration cluster ($#~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"::: ) ($#v5_rlvect_1 :::"vector-distributive"::: ) ($#v6_rlvect_1 :::"scalar-distributive"::: ) ($#v7_rlvect_1 :::"scalar-associative"::: ) ($#v8_rlvect_1 :::"scalar-unital"::: ) bbbadV3_NORMSP_0() bbbadV4_NORMSP_0() ($#v2_normsp_1 :::"RealNormSpace-like"::: ) bbbadV2_FUNCSDOM() ($#v3_group_1 :::"associative"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#v3_vectsp_1 :::"right_unital"::: ) ($#v5_lopban_2 :::"Banach_Algebra-like"::: ) -> ($#v4_vectsp_1 :::"well-unital"::: ) for ($#l1_lopban_2 :::"Normed_AlgebraStr"::: ) ; end; definitionlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#l4_algstr_0 :::"multLoopStr"::: ) ; let "v" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "X")); redefine attr "v" is :::"invertible"::: means :: LOPBAN_3:def 4 (Bool "ex" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" "X" "st" (Bool "(" (Bool (Set "v" ($#k6_algstr_0 :::"*"::: ) (Set (Var "w"))) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) "X")) & (Bool (Set (Set (Var "w")) ($#k6_algstr_0 :::"*"::: ) "v") ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) "X")) ")" )); end; :: deftheorem defines :::"invertible"::: LOPBAN_3:def 4 : (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#l4_algstr_0 :::"multLoopStr"::: ) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "v")) "is" ($#v25_algstr_0 :::"invertible"::: ) ) "iff" (Bool "ex" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Set (Var "v")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "w"))) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "X")))) & (Bool (Set (Set (Var "w")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "X")))) ")" )) ")" ))); definitionlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_lopban_2 :::"Normed_AlgebraStr"::: ) ; let "S" be ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "X")); let "a" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "X")); func "a" :::"*"::: "S" -> ($#m1_subset_1 :::"sequence":::) "of" "X" means :: LOPBAN_3:def 5 (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 "a" ($#k6_algstr_0 :::"*"::: ) (Set "(" "S" ($#k1_normsp_1 :::"."::: ) (Set (Var "n")) ")" )))); end; :: deftheorem defines :::"*"::: LOPBAN_3:def 5 : (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_lopban_2 :::"Normed_AlgebraStr"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) (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 "a")) ($#k2_lopban_3 :::"*"::: ) (Set (Var "S")))) "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 (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "S")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n")) ")" )))) ")" ))))); definitionlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_lopban_2 :::"Normed_AlgebraStr"::: ) ; let "S" be ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "X")); let "a" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "X")); func "S" :::"*"::: "a" -> ($#m1_subset_1 :::"sequence":::) "of" "X" means :: LOPBAN_3:def 6 (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 "(" "S" ($#k1_normsp_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k6_algstr_0 :::"*"::: ) "a"))); end; :: deftheorem defines :::"*"::: LOPBAN_3:def 6 : (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_lopban_2 :::"Normed_AlgebraStr"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) (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 "S")) ($#k3_lopban_3 :::"*"::: ) (Set (Var "a")))) "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 "S")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "a"))))) ")" ))))); definitionlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_lopban_2 :::"Normed_AlgebraStr"::: ) ; let "seq1", "seq2" be ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "X")); func "seq1" :::"*"::: "seq2" -> ($#m1_subset_1 :::"sequence":::) "of" "X" means :: LOPBAN_3: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 "(" "seq1" ($#k1_normsp_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" "seq2" ($#k1_normsp_1 :::"."::: ) (Set (Var "n")) ")" )))); end; :: deftheorem defines :::"*"::: LOPBAN_3:def 7 : (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_lopban_2 :::"Normed_AlgebraStr"::: ) (Bool "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "," (Set (Var "b4")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "seq1")) ($#k4_lopban_3 :::"*"::: ) (Set (Var "seq2")))) "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 "seq1")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "seq2")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n")) ")" )))) ")" ))); notationlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#l4_algstr_0 :::"multLoopStr"::: ) ; let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "X")); synonym "x" :::"""::: for :::"/"::: "x"; end; definitionlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#l4_algstr_0 :::"multLoopStr"::: ) ; let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "X")); assume (Bool (Set (Const "x")) "is" ($#v25_algstr_0 :::"invertible"::: ) ) ; redefine func :::"/"::: "x" means :: LOPBAN_3:def 8 (Bool "(" (Bool (Set "x" ($#k6_algstr_0 :::"*"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) "X")) & (Bool (Set it ($#k6_algstr_0 :::"*"::: ) "x") ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) "X")) ")" ); end; :: deftheorem defines :::"""::: LOPBAN_3:def 8 : (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#l4_algstr_0 :::"multLoopStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v25_algstr_0 :::"invertible"::: ) )) "holds" (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k9_algstr_0 :::"""::: ) )) "iff" (Bool "(" (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "X")))) & (Bool (Set (Set (Var "b3")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "X")))) ")" ) ")" )))); definitionlet "X" be ($#l1_lopban_2 :::"Banach_Algebra":::); let "z" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "X")); func "z" :::"GeoSeq"::: -> ($#m1_subset_1 :::"sequence":::) "of" "X" means :: LOPBAN_3:def 9 (Bool "(" (Bool (Set it ($#k1_normsp_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) "X")) & (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")) ")" ) ($#k6_algstr_0 :::"*"::: ) "z")) ")" ) ")" ); end; :: deftheorem defines :::"GeoSeq"::: LOPBAN_3:def 9 : (Bool "for" (Set (Var "X")) "being" ($#l1_lopban_2 :::"Banach_Algebra":::) (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "z")) ($#k5_lopban_3 :::"GeoSeq"::: ) )) "iff" (Bool "(" (Bool (Set (Set (Var "b3")) ($#k1_normsp_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "X")))) & (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")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "z")))) ")" ) ")" ) ")" )))); definitionlet "X" be ($#l1_lopban_2 :::"Banach_Algebra":::); let "z" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "X")); let "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func "z" :::"#N"::: "n" -> ($#m1_subset_1 :::"Element":::) "of" "X" equals :: LOPBAN_3:def 10 (Set (Set "(" "z" ($#k5_lopban_3 :::"GeoSeq"::: ) ")" ) ($#k1_normsp_1 :::"."::: ) "n"); end; :: deftheorem defines :::"#N"::: LOPBAN_3:def 10 : (Bool "for" (Set (Var "X")) "being" ($#l1_lopban_2 :::"Banach_Algebra":::) (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "z")) ($#k6_lopban_3 :::"#N"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "z")) ($#k5_lopban_3 :::"GeoSeq"::: ) ")" ) ($#k1_normsp_1 :::"."::: ) (Set (Var "n"))))))); theorem :: LOPBAN_3:39 (Bool "for" (Set (Var "X")) "being" ($#l1_lopban_2 :::"Banach_Algebra":::) (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "z")) ($#k6_lopban_3 :::"#N"::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "X")))))) ; theorem :: LOPBAN_3:40 (Bool "for" (Set (Var "X")) "being" ($#l1_lopban_2 :::"Banach_Algebra":::) (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "z")) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Num 1))) "holds" (Bool "(" (Bool (Set (Set (Var "z")) ($#k5_lopban_3 :::"GeoSeq"::: ) ) "is" ($#v1_lopban_3 :::"summable"::: ) ) & (Bool (Set (Set (Var "z")) ($#k5_lopban_3 :::"GeoSeq"::: ) ) "is" ($#v2_lopban_3 :::"norm_summable"::: ) ) ")" ))) ; theorem :: LOPBAN_3:41 (Bool "for" (Set (Var "X")) "being" ($#l1_lopban_2 :::"Banach_Algebra":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set "(" ($#k5_struct_0 :::"1."::: ) (Set (Var "X")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set (Var "x")) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Num 1))) "holds" (Bool "(" (Bool (Set (Set "(" (Set "(" ($#k5_struct_0 :::"1."::: ) (Set (Var "X")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set (Var "x")) ")" ) ($#k5_lopban_3 :::"GeoSeq"::: ) ) "is" ($#v1_lopban_3 :::"summable"::: ) ) & (Bool (Set (Set "(" (Set "(" ($#k5_struct_0 :::"1."::: ) (Set (Var "X")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set (Var "x")) ")" ) ($#k5_lopban_3 :::"GeoSeq"::: ) ) "is" ($#v2_lopban_3 :::"norm_summable"::: ) ) ")" ))) ; theorem :: LOPBAN_3:42 (Bool "for" (Set (Var "X")) "being" ($#l1_lopban_2 :::"Banach_Algebra":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set "(" ($#k5_struct_0 :::"1."::: ) (Set (Var "X")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set (Var "x")) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Num 1))) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#v25_algstr_0 :::"invertible"::: ) ) & (Bool (Set (Set (Var "x")) ($#k9_algstr_0 :::"""::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_lopban_3 :::"Sum"::: ) (Set "(" (Set "(" (Set "(" ($#k5_struct_0 :::"1."::: ) (Set (Var "X")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set (Var "x")) ")" ) ($#k5_lopban_3 :::"GeoSeq"::: ) ")" ))) ")" ))) ;