:: COMSEQ_3  semantic presentation begin  





















theorem :: COMSEQ_3:1 (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"   (Bool  "("  (Bool (Set (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_hidden :::"<>"::: )  (Set   ($#k5_complex1 :::"0c"::: )  )) & (Bool (Set (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  ($#k7_complex1 :::"<i>"::: ) ))  ($#r1_hidden :::"<>"::: )  (Set   ($#k5_complex1 :::"0c"::: )  ))  ")" )) ; 
 
theorem :: COMSEQ_3:2 (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   ($#k6_numbers :::"0"::: )  ))  ")" )) "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  "("  ($#k56_valued_1 :::"abs"::: )  (Set (Var "rseq")) ")" ) ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "m")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )))) ; 
 
theorem :: COMSEQ_3:3 (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   ($#k6_numbers :::"0"::: )  ))  ")" )) "holds"  (Bool (Set (Var "rseq")) "is"   ($#v2_series_1 :::"absolutely_summable"::: )  )) ; 
 registration
cluster   ($#v1_funct_1 :::"Function-like"::: )   bbbadV1_FUNCT_2((Set   ($#k5_numbers :::"NAT"::: )  ) "," (Set   ($#k1_numbers :::"REAL"::: )  ))   ($#v1_series_1 :::"summable"::: )    ->   ($#v2_comseq_2 :::"convergent"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1((Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) ))))); 
end; registration
cluster   ($#v1_funct_1 :::"Function-like"::: )   bbbadV1_FUNCT_2((Set   ($#k5_numbers :::"NAT"::: )  ) "," (Set   ($#k1_numbers :::"REAL"::: )  ))   ($#v2_series_1 :::"absolutely_summable"::: )    ->   ($#v1_series_1 :::"summable"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1((Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) ))))); 
end; registration
cluster   ($#v1_relat_1 :::"Relation-like"::: )   (Set   ($#k5_numbers :::"NAT"::: )  )  ($#v4_relat_1 :::"-defined"::: )   (Set   ($#k1_numbers :::"REAL"::: )  )  ($#v5_relat_1 :::"-valued"::: )     ($#v1_funct_1 :::"Function-like"::: )    ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"zero"::: )   )    ($#v1_partfun1 :::"total"::: )   bbbadV1_FUNCT_2((Set   ($#k5_numbers :::"NAT"::: )  ) "," (Set   ($#k1_numbers :::"REAL"::: )  ))   ($#v1_valued_0 :::"complex-valued"::: )     ($#v2_valued_0 :::"ext-real-valued"::: )     ($#v3_valued_0 :::"real-valued"::: )     ($#v2_series_1 :::"absolutely_summable"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1((Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) ))))); 
end; 
theorem :: COMSEQ_3:4 (Bool  "for" (Set (Var "rseq")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  "st" (Bool (Bool (Set (Var "rseq")) "is"   ($#v2_comseq_2 :::"convergent"::: )  )) "holds"  (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")) "," (Set (Var "l")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "m"))) & (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "l")))) "holds"  (Bool (Set   ($#k18_complex1 :::"abs"::: )  (Set  "(" (Set  "(" (Set (Var "rseq"))  ($#k8_nat_1 :::"."::: )  (Set (Var "m")) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set (Var "rseq"))  ($#k8_nat_1 :::"."::: )  (Set (Var "l")) ")" ) ")" ))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "p"))))))) ; 
 
theorem :: COMSEQ_3:5 (Bool  "for" (Set (Var "rseq")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Real":::)  "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_xxreal_0 :::"<="::: )  (Set (Var "p")))  ")" )) "holds"  (Bool  "for" (Set (Var "n")) "," (Set (Var "l")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set  "(" (Set  "("  ($#k3_series_1 :::"Partial_Sums"::: )  (Set (Var "rseq")) ")" )  ($#k8_nat_1 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Set (Var "l")) ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set  "("  ($#k3_series_1 :::"Partial_Sums"::: )  (Set (Var "rseq")) ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "n")) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "p"))  ($#k8_real_1 :::"*"::: )  (Set (Var "l"))))))) ; 
 
theorem :: COMSEQ_3:6 (Bool  "for" (Set (Var "rseq")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Real":::)  "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_xxreal_0 :::"<="::: )  (Set (Var "p")))  ")" )) "holds"  (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 (Var "rseq")) ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "p"))  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" )))))) ; 
 
theorem :: COMSEQ_3:7 (Bool  "for" (Set (Var "rseq1")) "," (Set (Var "rseq2")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  (Bool  "for" (Set (Var "m")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (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 "rseq1"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "p"))  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "rseq2"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n")) ")" )))  ")" )) "holds"  (Bool (Set (Set  "("  ($#k3_series_1 :::"Partial_Sums"::: )  (Set (Var "rseq1")) ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "m")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "p"))  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  "("  ($#k3_series_1 :::"Partial_Sums"::: )  (Set (Var "rseq2")) ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "m")) ")" )))))) ; 
 
theorem :: COMSEQ_3:8 (Bool  "for" (Set (Var "rseq1")) "," (Set (Var "rseq2")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  (Bool  "for" (Set (Var "m")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (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 "rseq1"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "p"))  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "rseq2"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n")) ")" )))  ")" )) "holds"  (Bool  "for" (Set (Var "n")) "," (Set (Var "l")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Set (Var "l")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "m")))) "holds"  (Bool (Set (Set  "(" (Set  "("  ($#k3_series_1 :::"Partial_Sums"::: )  (Set (Var "rseq1")) ")" )  ($#k8_nat_1 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Set (Var "l")) ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set  "("  ($#k3_series_1 :::"Partial_Sums"::: )  (Set (Var "rseq1")) ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "n")) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "p"))  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k3_series_1 :::"Partial_Sums"::: )  (Set (Var "rseq2")) ")" )  ($#k8_nat_1 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Set (Var "l")) ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set  "("  ($#k3_series_1 :::"Partial_Sums"::: )  (Set (Var "rseq2")) ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "n")) ")" ) ")" ))))))) ; 
 
theorem :: COMSEQ_3:9 (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   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "rseq"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n"))))  ")" )) "holds"  (Bool  "("  (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   ($#k18_complex1 :::"abs"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k3_series_1 :::"Partial_Sums"::: )  (Set (Var "rseq")) ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "m")) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set  "("  ($#k3_series_1 :::"Partial_Sums"::: )  (Set (Var "rseq")) ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "n")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k3_series_1 :::"Partial_Sums"::: )  (Set (Var "rseq")) ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "m")) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set  "("  ($#k3_series_1 :::"Partial_Sums"::: )  (Set (Var "rseq")) ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "n")) ")" )))  ")" ) & (Bool  "("   "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set   ($#k18_complex1 :::"abs"::: )  (Set  "(" (Set  "("  ($#k3_series_1 :::"Partial_Sums"::: )  (Set (Var "rseq")) ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "n")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_series_1 :::"Partial_Sums"::: )  (Set (Var "rseq")) ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "n"))))  ")" )  ")" )) ; 
 
theorem :: COMSEQ_3:10 (Bool  "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::)  "st" (Bool (Bool (Set (Var "seq1")) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set (Var "seq2")) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set   ($#k3_comseq_2 :::"lim"::: )  (Set  "(" (Set (Var "seq1"))  ($#k46_valued_1 :::"-"::: )  (Set (Var "seq2")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k5_complex1 :::"0c"::: )  ))) "holds"  (Bool (Set   ($#k3_comseq_2 :::"lim"::: )  (Set (Var "seq1")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_comseq_2 :::"lim"::: )  (Set (Var "seq2"))))) ; 
 begin  






definitionlet "z" be   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )  ; func "z" :::"GeoSeq":::  ->   ($#m1_subset_1 :::"Complex_Sequence":::) means :: COMSEQ_3:def 1 (Bool  "("  (Bool (Set it  ($#k8_nat_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_complex1 :::"1r"::: )  )) & (Bool  "("   "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set it  ($#k8_nat_1 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" it  ($#k8_nat_1 :::"."::: )  (Set (Var "n")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  "z"))  ")" )  ")" ); end; 





:: deftheorem    defines :::"GeoSeq"::: COMSEQ_3:def 1 :  (Bool  "for" (Set (Var "z")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "b2")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "z"))  ($#k1_comseq_3 :::"GeoSeq"::: )  )) "iff" (Bool  "("  (Bool (Set (Set (Var "b2"))  ($#k8_nat_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_complex1 :::"1r"::: )  )) & (Bool  "("   "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "b2"))  ($#k8_nat_1 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "b2"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "z"))))  ")" )  ")" )  ")" ))); 
 notationlet "z" be   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )  ; let "n" be   ($#v7_ordinal1 :::"natural"::: )     ($#m1_hidden :::"number"::: )  ; synonym "z" :::"#N"::: "n" for "z" :::"|^"::: "n"; end; definitionlet "z" be   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )  ; let "n" be   ($#v7_ordinal1 :::"natural"::: )     ($#m1_hidden :::"number"::: )  ; :: original: :::"#N"::: redefine func "z" :::"#N"::: "n" ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  ) equals :: COMSEQ_3:def 2 (Set (Set  "(" "z"  ($#k1_comseq_3 :::"GeoSeq"::: )  ")" )  ($#k8_nat_1 :::"."::: )  "n"); end; 






:: deftheorem    defines :::"#N"::: COMSEQ_3:def 2 :  (Bool  "for" (Set (Var "z")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "n")) "being"   ($#v7_ordinal1 :::"natural"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "z"))  ($#k2_comseq_3 :::"#N"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "z"))  ($#k1_comseq_3 :::"GeoSeq"::: )  ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "n")))))); 
 
theorem :: COMSEQ_3:11 (Bool  "for" (Set (Var "z")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  ) "holds"  (Bool (Set (Set (Var "z"))  ($#k2_comseq_3 :::"#N"::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_complex1 :::"1r"::: )  ))) ; 
 definitionlet "f" be   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"Function":::); func  :::"Re"::: "f" ->   ($#m1_hidden :::"Function":::) means :: COMSEQ_3:def 3 (Bool  "("  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  it)  ($#r1_hidden :::"="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  "f")) & (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  it))) "holds"  (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_complex1 :::"Re"::: )  (Set  "(" "f"  ($#k1_funct_1 :::"."::: )  (Set (Var "x")) ")" )))  ")" )  ")" ); func  :::"Im"::: "f" ->   ($#m1_hidden :::"Function":::) means :: COMSEQ_3:def 4 (Bool  "("  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  it)  ($#r1_hidden :::"="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  "f")) & (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  it))) "holds"  (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_complex1 :::"Im"::: )  (Set  "(" "f"  ($#k1_funct_1 :::"."::: )  (Set (Var "x")) ")" )))  ")" )  ")" ); end; 










:: deftheorem    defines :::"Re"::: COMSEQ_3:def 3 :  (Bool  "for" (Set (Var "f")) "being"   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"Function":::)  (Bool  "for" (Set (Var "b2")) "being"   ($#m1_hidden :::"Function":::) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_comseq_3 :::"Re"::: )  (Set (Var "f")))) "iff" (Bool  "("  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "b2")))  ($#r1_hidden :::"="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f")))) & (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "b2"))))) "holds"  (Bool (Set (Set (Var "b2"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_complex1 :::"Re"::: )  (Set  "(" (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x")) ")" )))  ")" )  ")" )  ")" ))); 
 
:: deftheorem    defines :::"Im"::: COMSEQ_3:def 4 :  (Bool  "for" (Set (Var "f")) "being"   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"Function":::)  (Bool  "for" (Set (Var "b2")) "being"   ($#m1_hidden :::"Function":::) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_comseq_3 :::"Im"::: )  (Set (Var "f")))) "iff" (Bool  "("  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "b2")))  ($#r1_hidden :::"="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f")))) & (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "b2"))))) "holds"  (Bool (Set (Set (Var "b2"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_complex1 :::"Im"::: )  (Set  "(" (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x")) ")" )))  ")" )  ")" )  ")" ))); 
 registrationlet "f" be   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"Function":::); 
cluster (Set   ($#k3_comseq_3 :::"Re"::: )  "f") ->   ($#v3_valued_0 :::"real-valued"::: )   ; 

cluster (Set   ($#k4_comseq_3 :::"Im"::: )  "f") ->   ($#v3_valued_0 :::"real-valued"::: )   ; 
end; definitionlet "X" be    ($#m1_hidden :::"set"::: )  ; let "f" be   ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set  ($#k2_numbers :::"COMPLEX"::: ) ); :: original: :::"Re"::: redefine func  :::"Re"::: "f" ->   ($#m1_subset_1 :::"PartFunc":::) "of" "X" "," (Set  ($#k1_numbers :::"REAL"::: ) ); :: original: :::"Im"::: redefine func  :::"Im"::: "f" ->   ($#m1_subset_1 :::"PartFunc":::) "of" "X" "," (Set  ($#k1_numbers :::"REAL"::: ) ); end; definitionlet "c" be   ($#m1_subset_1 :::"Complex_Sequence":::); :: original: :::"Re"::: redefine func  :::"Re"::: "c" ->   ($#m1_subset_1 :::"Real_Sequence":::) means :: COMSEQ_3:def 5 (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set it  ($#k8_nat_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_complex1 :::"Re"::: )  (Set  "(" "c"  ($#k8_nat_1 :::"."::: )  (Set (Var "n")) ")" )))); :: original: :::"Im"::: redefine func  :::"Im"::: "c" ->   ($#m1_subset_1 :::"Real_Sequence":::) means :: COMSEQ_3:def 6 (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set it  ($#k8_nat_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_complex1 :::"Im"::: )  (Set  "(" "c"  ($#k8_nat_1 :::"."::: )  (Set (Var "n")) ")" )))); end; 










:: deftheorem    defines :::"Re"::: COMSEQ_3:def 5 :  (Bool  "for" (Set (Var "c")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::)  (Bool  "for" (Set (Var "b2")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k7_comseq_3 :::"Re"::: )  (Set (Var "c")))) "iff" (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "b2"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_complex1 :::"Re"::: )  (Set  "(" (Set (Var "c"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n")) ")" ))))  ")" ))); 
 
:: deftheorem    defines :::"Im"::: COMSEQ_3:def 6 :  (Bool  "for" (Set (Var "c")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::)  (Bool  "for" (Set (Var "b2")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k8_comseq_3 :::"Im"::: )  (Set (Var "c")))) "iff" (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "b2"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_complex1 :::"Im"::: )  (Set  "(" (Set (Var "c"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n")) ")" ))))  ")" ))); 
 
theorem :: COMSEQ_3:12 (Bool  "for" (Set (Var "z")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  ) "holds"  (Bool (Set  ($#k17_complex1 :::"|."::: ) (Set (Var "z")) ($#k17_complex1 :::".|"::: ) )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "("  ($#k18_complex1 :::"abs"::: )  (Set  "("  ($#k3_complex1 :::"Re"::: )  (Set (Var "z")) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "("  ($#k18_complex1 :::"abs"::: )  (Set  "("  ($#k4_complex1 :::"Im"::: )  (Set (Var "z")) ")" ) ")" )))) ; 
 
theorem :: COMSEQ_3:13 (Bool  "for" (Set (Var "z")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  ) "holds"   (Bool  "("  (Bool (Set   ($#k18_complex1 :::"abs"::: )  (Set  "("  ($#k3_complex1 :::"Re"::: )  (Set (Var "z")) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set (Var "z")) ($#k17_complex1 :::".|"::: ) )) & (Bool (Set   ($#k18_complex1 :::"abs"::: )  (Set  "("  ($#k4_complex1 :::"Im"::: )  (Set (Var "z")) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set (Var "z")) ($#k17_complex1 :::".|"::: ) ))  ")" )) ; 
 
theorem :: COMSEQ_3:14 (Bool  "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::)  "st" (Bool (Bool (Set   ($#k7_comseq_3 :::"Re"::: )  (Set (Var "seq1")))  ($#r2_funct_2 :::"="::: )  (Set   ($#k7_comseq_3 :::"Re"::: )  (Set (Var "seq2")))) & (Bool (Set   ($#k8_comseq_3 :::"Im"::: )  (Set (Var "seq1")))  ($#r2_funct_2 :::"="::: )  (Set   ($#k8_comseq_3 :::"Im"::: )  (Set (Var "seq2"))))) "holds"  (Bool (Set (Var "seq1"))  ($#r2_funct_2 :::"="::: )  (Set (Var "seq2")))) ; 
 
theorem :: COMSEQ_3:15 (Bool  "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::) "holds"   (Bool  "("  (Bool (Set (Set  "("  ($#k7_comseq_3 :::"Re"::: )  (Set (Var "seq1")) ")" )  ($#k1_series_1 :::"+"::: )  (Set  "("  ($#k7_comseq_3 :::"Re"::: )  (Set (Var "seq2")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set   ($#k7_comseq_3 :::"Re"::: )  (Set  "(" (Set (Var "seq1"))  ($#k1_series_1 :::"+"::: )  (Set (Var "seq2")) ")" ))) & (Bool (Set (Set  "("  ($#k8_comseq_3 :::"Im"::: )  (Set (Var "seq1")) ")" )  ($#k1_series_1 :::"+"::: )  (Set  "("  ($#k8_comseq_3 :::"Im"::: )  (Set (Var "seq2")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set   ($#k8_comseq_3 :::"Im"::: )  (Set  "(" (Set (Var "seq1"))  ($#k1_series_1 :::"+"::: )  (Set (Var "seq2")) ")" )))  ")" )) ; 
 
theorem :: COMSEQ_3:16 (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::) "holds"   (Bool  "("  (Bool (Set   ($#k32_valued_1 :::"-"::: )  (Set  "("  ($#k7_comseq_3 :::"Re"::: )  (Set (Var "seq")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set   ($#k7_comseq_3 :::"Re"::: )  (Set  "("  ($#k31_valued_1 :::"-"::: )  (Set (Var "seq")) ")" ))) & (Bool (Set   ($#k32_valued_1 :::"-"::: )  (Set  "("  ($#k8_comseq_3 :::"Im"::: )  (Set (Var "seq")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set   ($#k8_comseq_3 :::"Im"::: )  (Set  "("  ($#k31_valued_1 :::"-"::: )  (Set (Var "seq")) ")" )))  ")" )) ; 
 
theorem :: COMSEQ_3:17 (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "z")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  ) "holds"   (Bool  "("  (Bool (Set (Set (Var "r"))  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k3_complex1 :::"Re"::: )  (Set (Var "z")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k3_complex1 :::"Re"::: )  (Set  "(" (Set (Var "r"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "z")) ")" ))) & (Bool (Set (Set (Var "r"))  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k4_complex1 :::"Im"::: )  (Set (Var "z")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_complex1 :::"Im"::: )  (Set  "(" (Set (Var "r"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "z")) ")" )))  ")" ))) ; 
 
theorem :: COMSEQ_3:18 (Bool  "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::) "holds"   (Bool  "("  (Bool (Set (Set  "("  ($#k7_comseq_3 :::"Re"::: )  (Set (Var "seq1")) ")" )  ($#k47_valued_1 :::"-"::: )  (Set  "("  ($#k7_comseq_3 :::"Re"::: )  (Set (Var "seq2")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set   ($#k7_comseq_3 :::"Re"::: )  (Set  "(" (Set (Var "seq1"))  ($#k46_valued_1 :::"-"::: )  (Set (Var "seq2")) ")" ))) & (Bool (Set (Set  "("  ($#k8_comseq_3 :::"Im"::: )  (Set (Var "seq1")) ")" )  ($#k47_valued_1 :::"-"::: )  (Set  "("  ($#k8_comseq_3 :::"Im"::: )  (Set (Var "seq2")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set   ($#k8_comseq_3 :::"Im"::: )  (Set  "(" (Set (Var "seq1"))  ($#k46_valued_1 :::"-"::: )  (Set (Var "seq2")) ")" )))  ")" )) ; 
 
theorem :: COMSEQ_3:19 (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::)  (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::) "holds"   (Bool  "("  (Bool (Set (Set (Var "r"))  ($#k26_valued_1 :::"(#)"::: )  (Set  "("  ($#k7_comseq_3 :::"Re"::: )  (Set (Var "seq")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set   ($#k7_comseq_3 :::"Re"::: )  (Set  "(" (Set (Var "r"))  ($#k25_valued_1 :::"(#)"::: )  (Set (Var "seq")) ")" ))) & (Bool (Set (Set (Var "r"))  ($#k26_valued_1 :::"(#)"::: )  (Set  "("  ($#k8_comseq_3 :::"Im"::: )  (Set (Var "seq")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set   ($#k8_comseq_3 :::"Im"::: )  (Set  "(" (Set (Var "r"))  ($#k25_valued_1 :::"(#)"::: )  (Set (Var "seq")) ")" )))  ")" ))) ; 
 
theorem :: COMSEQ_3:20 (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::)  (Bool  "for" (Set (Var "z")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  ) "holds"   (Bool  "("  (Bool (Set   ($#k7_comseq_3 :::"Re"::: )  (Set  "(" (Set (Var "z"))  ($#k25_valued_1 :::"(#)"::: )  (Set (Var "seq")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set (Set  "(" (Set  "("  ($#k3_complex1 :::"Re"::: )  (Set (Var "z")) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set  "("  ($#k7_comseq_3 :::"Re"::: )  (Set (Var "seq")) ")" ) ")" )  ($#k47_valued_1 :::"-"::: )  (Set  "(" (Set  "("  ($#k4_complex1 :::"Im"::: )  (Set (Var "z")) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set  "("  ($#k8_comseq_3 :::"Im"::: )  (Set (Var "seq")) ")" ) ")" ))) & (Bool (Set   ($#k8_comseq_3 :::"Im"::: )  (Set  "(" (Set (Var "z"))  ($#k25_valued_1 :::"(#)"::: )  (Set (Var "seq")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set (Set  "(" (Set  "("  ($#k3_complex1 :::"Re"::: )  (Set (Var "z")) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set  "("  ($#k8_comseq_3 :::"Im"::: )  (Set (Var "seq")) ")" ) ")" )  ($#k1_series_1 :::"+"::: )  (Set  "(" (Set  "("  ($#k4_complex1 :::"Im"::: )  (Set (Var "z")) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set  "("  ($#k7_comseq_3 :::"Re"::: )  (Set (Var "seq")) ")" ) ")" )))  ")" ))) ; 
 
theorem :: COMSEQ_3:21 (Bool  "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::) "holds"   (Bool  "("  (Bool (Set   ($#k7_comseq_3 :::"Re"::: )  (Set  "(" (Set (Var "seq1"))  ($#k19_valued_1 :::"(#)"::: )  (Set (Var "seq2")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set (Set  "(" (Set  "("  ($#k7_comseq_3 :::"Re"::: )  (Set (Var "seq1")) ")" )  ($#k20_valued_1 :::"(#)"::: )  (Set  "("  ($#k7_comseq_3 :::"Re"::: )  (Set (Var "seq2")) ")" ) ")" )  ($#k47_valued_1 :::"-"::: )  (Set  "(" (Set  "("  ($#k8_comseq_3 :::"Im"::: )  (Set (Var "seq1")) ")" )  ($#k20_valued_1 :::"(#)"::: )  (Set  "("  ($#k8_comseq_3 :::"Im"::: )  (Set (Var "seq2")) ")" ) ")" ))) & (Bool (Set   ($#k8_comseq_3 :::"Im"::: )  (Set  "(" (Set (Var "seq1"))  ($#k19_valued_1 :::"(#)"::: )  (Set (Var "seq2")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set (Set  "(" (Set  "("  ($#k7_comseq_3 :::"Re"::: )  (Set (Var "seq1")) ")" )  ($#k20_valued_1 :::"(#)"::: )  (Set  "("  ($#k8_comseq_3 :::"Im"::: )  (Set (Var "seq2")) ")" ) ")" )  ($#k1_series_1 :::"+"::: )  (Set  "(" (Set  "("  ($#k8_comseq_3 :::"Im"::: )  (Set (Var "seq1")) ")" )  ($#k20_valued_1 :::"(#)"::: )  (Set  "("  ($#k7_comseq_3 :::"Re"::: )  (Set (Var "seq2")) ")" ) ")" )))  ")" )) ; 
 definitionlet "Nseq" be   ($#v5_valued_0 :::"increasing"::: )    ($#m1_subset_1 :::"sequence":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) ); let "seq" be   ($#m1_subset_1 :::"Complex_Sequence":::); :: original: :::"(#)"::: redefine func "seq" :::"*"::: "Nseq" ->   ($#m1_subset_1 :::"Complex_Sequence":::); end; 
theorem :: COMSEQ_3:22 (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::)  (Bool  "for" (Set (Var "Nseq")) "being"   ($#v5_valued_0 :::"increasing"::: )    ($#m1_subset_1 :::"sequence":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) ) "holds"   (Bool  "("  (Bool (Set   ($#k7_comseq_3 :::"Re"::: )  (Set  "(" (Set (Var "seq"))  ($#k9_comseq_3 :::"*"::: )  (Set (Var "Nseq")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set (Set  "("  ($#k7_comseq_3 :::"Re"::: )  (Set (Var "seq")) ")" )  ($#k2_valued_0 :::"*"::: )  (Set (Var "Nseq")))) & (Bool (Set   ($#k8_comseq_3 :::"Im"::: )  (Set  "(" (Set (Var "seq"))  ($#k9_comseq_3 :::"*"::: )  (Set (Var "Nseq")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set (Set  "("  ($#k8_comseq_3 :::"Im"::: )  (Set (Var "seq")) ")" )  ($#k2_valued_0 :::"*"::: )  (Set (Var "Nseq"))))  ")" ))) ; 
 
theorem :: COMSEQ_3:23 (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::)  (Bool  "for" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"   (Bool  "("  (Bool (Set (Set  "("  ($#k7_comseq_3 :::"Re"::: )  (Set (Var "seq")) ")" )  ($#k1_valued_0 :::"^\"::: )  (Set (Var "k")))  ($#r2_funct_2 :::"="::: )  (Set   ($#k7_comseq_3 :::"Re"::: )  (Set  "(" (Set (Var "seq"))  ($#k1_valued_0 :::"^\"::: )  (Set (Var "k")) ")" ))) & (Bool (Set (Set  "("  ($#k8_comseq_3 :::"Im"::: )  (Set (Var "seq")) ")" )  ($#k1_valued_0 :::"^\"::: )  (Set (Var "k")))  ($#r2_funct_2 :::"="::: )  (Set   ($#k8_comseq_3 :::"Im"::: )  (Set  "(" (Set (Var "seq"))  ($#k1_valued_0 :::"^\"::: )  (Set (Var "k")) ")" )))  ")" ))) ; 
 definitionlet "s" be   ($#m1_subset_1 :::"Complex_Sequence":::); :: original: :::"Partial_Sums"::: redefine func  :::"Partial_Sums"::: "s" ->   ($#m1_subset_1 :::"Complex_Sequence":::); end; definitionlet "seq" be   ($#m1_subset_1 :::"Complex_Sequence":::); func  :::"Sum"::: "seq" ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  ) equals :: COMSEQ_3:def 7 (Set   ($#k3_comseq_2 :::"lim"::: )  (Set  "("  ($#k10_comseq_3 :::"Partial_Sums"::: )  "seq" ")" )); end; 





:: deftheorem    defines :::"Sum"::: COMSEQ_3:def 7 :  (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::) "holds"  (Bool (Set   ($#k11_comseq_3 :::"Sum"::: )  (Set (Var "seq")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_comseq_2 :::"lim"::: )  (Set  "("  ($#k10_comseq_3 :::"Partial_Sums"::: )  (Set (Var "seq")) ")" )))); 
 
theorem :: COMSEQ_3:24 (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::)  "st" (Bool (Bool  "("   "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "seq"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set   ($#k5_complex1 :::"0c"::: )  ))  ")" )) "holds"  (Bool  "for" (Set (Var "m")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set  "("  ($#k10_comseq_3 :::"Partial_Sums"::: )  (Set (Var "seq")) ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "m")))  ($#r1_hidden :::"="::: )  (Set   ($#k5_complex1 :::"0c"::: )  )))) ; 
 
theorem :: COMSEQ_3:25 (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::)  "st" (Bool (Bool  "("   "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "seq"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set   ($#k5_complex1 :::"0c"::: )  ))  ")" )) "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  ($#k55_valued_1 :::"|."::: ) (Set (Var "seq")) ($#k55_valued_1 :::".|"::: ) ) ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "m")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )))) ; 
 
theorem :: COMSEQ_3:26 (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::) "holds"   (Bool  "("  (Bool (Set   ($#k3_series_1 :::"Partial_Sums"::: )  (Set  "("  ($#k7_comseq_3 :::"Re"::: )  (Set (Var "seq")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set   ($#k7_comseq_3 :::"Re"::: )  (Set  "("  ($#k10_comseq_3 :::"Partial_Sums"::: )  (Set (Var "seq")) ")" ))) & (Bool (Set   ($#k3_series_1 :::"Partial_Sums"::: )  (Set  "("  ($#k8_comseq_3 :::"Im"::: )  (Set (Var "seq")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set   ($#k8_comseq_3 :::"Im"::: )  (Set  "("  ($#k10_comseq_3 :::"Partial_Sums"::: )  (Set (Var "seq")) ")" )))  ")" )) ; 
 
theorem :: COMSEQ_3:27 (Bool  "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::) "holds"  (Bool (Set (Set  "("  ($#k10_comseq_3 :::"Partial_Sums"::: )  (Set (Var "seq1")) ")" )  ($#k1_series_1 :::"+"::: )  (Set  "("  ($#k10_comseq_3 :::"Partial_Sums"::: )  (Set (Var "seq2")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set   ($#k10_comseq_3 :::"Partial_Sums"::: )  (Set  "(" (Set (Var "seq1"))  ($#k1_series_1 :::"+"::: )  (Set (Var "seq2")) ")" )))) ; 
 
theorem :: COMSEQ_3:28 (Bool  "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::) "holds"  (Bool (Set (Set  "("  ($#k10_comseq_3 :::"Partial_Sums"::: )  (Set (Var "seq1")) ")" )  ($#k46_valued_1 :::"-"::: )  (Set  "("  ($#k10_comseq_3 :::"Partial_Sums"::: )  (Set (Var "seq2")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set   ($#k10_comseq_3 :::"Partial_Sums"::: )  (Set  "(" (Set (Var "seq1"))  ($#k46_valued_1 :::"-"::: )  (Set (Var "seq2")) ")" )))) ; 
 
theorem :: COMSEQ_3:29 (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::)  (Bool  "for" (Set (Var "z")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k10_comseq_3 :::"Partial_Sums"::: )  (Set  "(" (Set (Var "z"))  ($#k25_valued_1 :::"(#)"::: )  (Set (Var "seq")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set (Set (Var "z"))  ($#k25_valued_1 :::"(#)"::: )  (Set  "("  ($#k10_comseq_3 :::"Partial_Sums"::: )  (Set (Var "seq")) ")" ))))) ; 
 
theorem :: COMSEQ_3:30 (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::)  (Bool  "for" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set  "("  ($#k10_comseq_3 :::"Partial_Sums"::: )  (Set (Var "seq")) ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "k")) ")" ) ($#k17_complex1 :::".|"::: ) )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "("  ($#k3_series_1 :::"Partial_Sums"::: )  (Set  ($#k55_valued_1 :::"|."::: ) (Set (Var "seq")) ($#k55_valued_1 :::".|"::: ) ) ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "k")))))) ; 
 
theorem :: COMSEQ_3:31 (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::)  (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set  "(" (Set  "("  ($#k10_comseq_3 :::"Partial_Sums"::: )  (Set (Var "seq")) ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "m")) ")" )  ($#k11_complex1 :::"-"::: )  (Set  "(" (Set  "("  ($#k10_comseq_3 :::"Partial_Sums"::: )  (Set (Var "seq")) ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "n")) ")" ) ")" ) ($#k17_complex1 :::".|"::: ) )  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k18_complex1 :::"abs"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k3_series_1 :::"Partial_Sums"::: )  (Set  ($#k55_valued_1 :::"|."::: ) (Set (Var "seq")) ($#k55_valued_1 :::".|"::: ) ) ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "m")) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set  "("  ($#k3_series_1 :::"Partial_Sums"::: )  (Set  ($#k55_valued_1 :::"|."::: ) (Set (Var "seq")) ($#k55_valued_1 :::".|"::: ) ) ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "n")) ")" ) ")" ))))) ; 
 
theorem :: COMSEQ_3:32 (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::)  (Bool  "for" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"   (Bool  "("  (Bool (Set (Set  "("  ($#k3_series_1 :::"Partial_Sums"::: )  (Set  "("  ($#k7_comseq_3 :::"Re"::: )  (Set (Var "seq")) ")" ) ")" )  ($#k1_valued_0 :::"^\"::: )  (Set (Var "k")))  ($#r2_funct_2 :::"="::: )  (Set   ($#k7_comseq_3 :::"Re"::: )  (Set  "(" (Set  "("  ($#k10_comseq_3 :::"Partial_Sums"::: )  (Set (Var "seq")) ")" )  ($#k1_valued_0 :::"^\"::: )  (Set (Var "k")) ")" ))) & (Bool (Set (Set  "("  ($#k3_series_1 :::"Partial_Sums"::: )  (Set  "("  ($#k8_comseq_3 :::"Im"::: )  (Set (Var "seq")) ")" ) ")" )  ($#k1_valued_0 :::"^\"::: )  (Set (Var "k")))  ($#r2_funct_2 :::"="::: )  (Set   ($#k8_comseq_3 :::"Im"::: )  (Set  "(" (Set  "("  ($#k10_comseq_3 :::"Partial_Sums"::: )  (Set (Var "seq")) ")" )  ($#k1_valued_0 :::"^\"::: )  (Set (Var "k")) ")" )))  ")" ))) ; 
 
theorem :: COMSEQ_3:33 (Bool  "for" (Set (Var "seq1")) "," (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::)  "st" (Bool (Bool  "("   "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "seq1"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "seq"))  ($#k8_nat_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) )))  ")" )) "holds"  (Bool (Set   ($#k10_comseq_3 :::"Partial_Sums"::: )  (Set  "(" (Set (Var "seq"))  ($#k1_valued_0 :::"^\"::: )  (Num 1) ")" ))  ($#r2_funct_2 :::"="::: )  (Set (Set  "(" (Set  "("  ($#k10_comseq_3 :::"Partial_Sums"::: )  (Set (Var "seq")) ")" )  ($#k1_valued_0 :::"^\"::: )  (Num 1) ")" )  ($#k46_valued_1 :::"-"::: )  (Set (Var "seq1"))))) ; 
 
theorem :: COMSEQ_3:34 (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::) "holds"  (Bool (Set   ($#k3_series_1 :::"Partial_Sums"::: )  (Set  ($#k55_valued_1 :::"|."::: ) (Set (Var "seq")) ($#k55_valued_1 :::".|"::: ) )) "is"   ($#v7_valued_0 :::"non-decreasing"::: )  )) ; 
 registrationlet "seq" be   ($#m1_subset_1 :::"Complex_Sequence":::); 
cluster (Set   ($#k2_series_1 :::"Partial_Sums"::: )  (Set  ($#k55_valued_1 :::"|."::: ) "seq" ($#k55_valued_1 :::".|"::: ) )) ->   ($#v7_valued_0 :::"non-decreasing"::: )    for  ($#m1_subset_1 :::"Real_Sequence":::); 
end; 
theorem :: COMSEQ_3:35 (Bool  "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::)  (Bool  "for" (Set (Var "m")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (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 "seq1"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "seq2"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n"))))  ")" )) "holds"  (Bool (Set (Set  "("  ($#k10_comseq_3 :::"Partial_Sums"::: )  (Set (Var "seq1")) ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "m")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k10_comseq_3 :::"Partial_Sums"::: )  (Set (Var "seq2")) ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "m")))))) ; 
 
theorem :: COMSEQ_3:36 (Bool  "for" (Set (Var "z")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  )  "st" (Bool (Bool (Set   ($#k6_complex1 :::"1r"::: )  )  ($#r1_hidden :::"<>"::: )  (Set (Var "z")))) "holds"  (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set  "("  ($#k10_comseq_3 :::"Partial_Sums"::: )  (Set  "(" (Set (Var "z"))  ($#k1_comseq_3 :::"GeoSeq"::: )  ")" ) ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  ($#k6_complex1 :::"1r"::: ) )  ($#k11_complex1 :::"-"::: )  (Set  "(" (Set (Var "z"))  ($#k2_comseq_3 :::"#N"::: )  (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Set  "(" (Set  ($#k6_complex1 :::"1r"::: ) )  ($#k11_complex1 :::"-"::: )  (Set (Var "z")) ")" ))))) ; 
 
theorem :: COMSEQ_3:37 (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::)  (Bool  "for" (Set (Var "z")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  )  "st" (Bool (Bool (Set (Var "z"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_complex1 :::"1r"::: )  )) & (Bool  "("   "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "seq"))  ($#k8_nat_1 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "z"))  ($#k9_complex1 :::"*"::: )  (Set  "(" (Set (Var "seq"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n")) ")" )))  ")" )) "holds"  (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set  "("  ($#k10_comseq_3 :::"Partial_Sums"::: )  (Set (Var "seq")) ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "seq"))  ($#k8_nat_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" )  ($#k9_complex1 :::"*"::: )  (Set  "(" (Set  "(" (Set  ($#k6_complex1 :::"1r"::: ) )  ($#k11_complex1 :::"-"::: )  (Set  "(" (Set (Var "z"))  ($#k2_comseq_3 :::"#N"::: )  (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Set  "(" (Set  ($#k6_complex1 :::"1r"::: ) )  ($#k11_complex1 :::"-"::: )  (Set (Var "z")) ")" ) ")" )))))) ; 
 begin  
theorem :: COMSEQ_3:38 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  (Bool  "for" (Set (Var "c")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::)  "st" (Bool (Bool  "("   "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"   (Bool  "("  (Bool (Set   ($#k3_complex1 :::"Re"::: )  (Set  "(" (Set (Var "c"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n")))) & (Bool (Set   ($#k4_complex1 :::"Im"::: )  (Set  "(" (Set (Var "c"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "b"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n"))))  ")" )  ")" )) "holds"  (Bool  "("  (Bool  "("  (Bool (Set (Var "a")) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set (Var "b")) "is"   ($#v2_comseq_2 :::"convergent"::: )  )  ")" ) "iff" (Bool (Set (Var "c")) "is"   ($#v2_comseq_2 :::"convergent"::: )  )  ")" ))) ; 
 
theorem :: COMSEQ_3:39 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v2_comseq_2 :::"convergent"::: )    ($#m1_subset_1 :::"Real_Sequence":::)  (Bool  "for" (Set (Var "c")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::)  "st" (Bool (Bool  "("   "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"   (Bool  "("  (Bool (Set   ($#k3_complex1 :::"Re"::: )  (Set  "(" (Set (Var "c"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n")))) & (Bool (Set   ($#k4_complex1 :::"Im"::: )  (Set  "(" (Set (Var "c"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "b"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n"))))  ")" )  ")" )) "holds"  (Bool  "("  (Bool (Set (Var "c")) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set   ($#k3_comseq_2 :::"lim"::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_seq_2 :::"lim"::: )  (Set (Var "a")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  "("  ($#k2_seq_2 :::"lim"::: )  (Set (Var "b")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  ($#k7_complex1 :::"<i>"::: ) ) ")" )))  ")" ))) ; 
 
theorem :: COMSEQ_3:40 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  (Bool  "for" (Set (Var "c")) "being"   ($#v2_comseq_2 :::"convergent"::: )    ($#m1_subset_1 :::"Complex_Sequence":::)  "st" (Bool (Bool  "("   "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"   (Bool  "("  (Bool (Set   ($#k3_complex1 :::"Re"::: )  (Set  "(" (Set (Var "c"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n")))) & (Bool (Set   ($#k4_complex1 :::"Im"::: )  (Set  "(" (Set (Var "c"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "b"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n"))))  ")" )  ")" )) "holds"  (Bool  "("  (Bool (Set (Var "a")) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set (Var "b")) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set   ($#k2_seq_2 :::"lim"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_complex1 :::"Re"::: )  (Set  "("  ($#k3_comseq_2 :::"lim"::: )  (Set (Var "c")) ")" ))) & (Bool (Set   ($#k2_seq_2 :::"lim"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_complex1 :::"Im"::: )  (Set  "("  ($#k3_comseq_2 :::"lim"::: )  (Set (Var "c")) ")" )))  ")" ))) ; 
 
theorem :: COMSEQ_3:41 (Bool  "for" (Set (Var "c")) "being"   ($#v2_comseq_2 :::"convergent"::: )    ($#m1_subset_1 :::"Complex_Sequence":::) "holds"   (Bool  "("  (Bool (Set   ($#k7_comseq_3 :::"Re"::: )  (Set (Var "c"))) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set   ($#k8_comseq_3 :::"Im"::: )  (Set (Var "c"))) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set   ($#k2_seq_2 :::"lim"::: )  (Set  "("  ($#k7_comseq_3 :::"Re"::: )  (Set (Var "c")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k3_complex1 :::"Re"::: )  (Set  "("  ($#k3_comseq_2 :::"lim"::: )  (Set (Var "c")) ")" ))) & (Bool (Set   ($#k2_seq_2 :::"lim"::: )  (Set  "("  ($#k8_comseq_3 :::"Im"::: )  (Set (Var "c")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_complex1 :::"Im"::: )  (Set  "("  ($#k3_comseq_2 :::"lim"::: )  (Set (Var "c")) ")" )))  ")" )) ; 
 registrationlet "c" be   ($#v2_comseq_2 :::"convergent"::: )    ($#m1_subset_1 :::"Complex_Sequence":::); 
cluster (Set   ($#k3_comseq_3 :::"Re"::: )  "c") ->   ($#v2_comseq_2 :::"convergent"::: )    for  ($#m1_subset_1 :::"Real_Sequence":::); 

cluster (Set   ($#k4_comseq_3 :::"Im"::: )  "c") ->   ($#v2_comseq_2 :::"convergent"::: )    for  ($#m1_subset_1 :::"Real_Sequence":::); 
end; 
theorem :: COMSEQ_3:42 (Bool  "for" (Set (Var "c")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::)  "st" (Bool (Bool (Set   ($#k7_comseq_3 :::"Re"::: )  (Set (Var "c"))) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set   ($#k8_comseq_3 :::"Im"::: )  (Set (Var "c"))) "is"   ($#v2_comseq_2 :::"convergent"::: )  )) "holds"  (Bool  "("  (Bool (Set (Var "c")) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set   ($#k3_complex1 :::"Re"::: )  (Set  "("  ($#k3_comseq_2 :::"lim"::: )  (Set (Var "c")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_seq_2 :::"lim"::: )  (Set  "("  ($#k7_comseq_3 :::"Re"::: )  (Set (Var "c")) ")" ))) & (Bool (Set   ($#k4_complex1 :::"Im"::: )  (Set  "("  ($#k3_comseq_2 :::"lim"::: )  (Set (Var "c")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_seq_2 :::"lim"::: )  (Set  "("  ($#k8_comseq_3 :::"Im"::: )  (Set (Var "c")) ")" )))  ")" )) ; 
 
theorem :: COMSEQ_3:43 (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::)  (Bool  "for" (Set (Var "z")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  )  "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set (Var "z")) ($#k17_complex1 :::".|"::: ) )) & (Bool (Set  ($#k17_complex1 :::"|."::: ) (Set (Var "z")) ($#k17_complex1 :::".|"::: ) )  ($#r1_xxreal_0 :::"<"::: )  (Num 1)) & (Bool (Set (Set (Var "seq"))  ($#k8_nat_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "z"))) & (Bool  "("   "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "seq"))  ($#k8_nat_1 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "seq"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n")) ")" )  ($#k9_complex1 :::"*"::: )  (Set (Var "z"))))  ")" )) "holds"  (Bool  "("  (Bool (Set (Var "seq")) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set   ($#k3_comseq_2 :::"lim"::: )  (Set (Var "seq")))  ($#r1_hidden :::"="::: )  (Set   ($#k5_complex1 :::"0c"::: )  ))  ")" ))) ; 
 
theorem :: COMSEQ_3:44 (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::)  (Bool  "for" (Set (Var "z")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  )  "st" (Bool (Bool (Set  ($#k17_complex1 :::"|."::: ) (Set (Var "z")) ($#k17_complex1 :::".|"::: ) )  ($#r1_xxreal_0 :::"<"::: )  (Num 1)) & (Bool  "("   "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "seq"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "z"))  ($#k2_comseq_3 :::"#N"::: )  (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" )))  ")" )) "holds"  (Bool  "("  (Bool (Set (Var "seq")) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set   ($#k3_comseq_2 :::"lim"::: )  (Set (Var "seq")))  ($#r1_hidden :::"="::: )  (Set   ($#k5_complex1 :::"0c"::: )  ))  ")" ))) ; 
 
theorem :: COMSEQ_3:45 (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::)  (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  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set (Var "seq"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n")) ")" ) ($#k17_complex1 :::".|"::: ) )  ($#r1_xxreal_0 :::">="::: )  (Set (Var "r"))))) & (Bool (Set  ($#k55_valued_1 :::"|."::: ) (Set (Var "seq")) ($#k55_valued_1 :::".|"::: ) ) "is"   ($#v2_comseq_2 :::"convergent"::: )  )) "holds"  (Bool (Set   ($#k2_seq_2 :::"lim"::: )  (Set  ($#k55_valued_1 :::"|."::: ) (Set (Var "seq")) ($#k55_valued_1 :::".|"::: ) ))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )))) ; 
 
theorem :: COMSEQ_3:46 (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::) "holds"   (Bool  "("  (Bool (Set (Var "seq")) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) "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  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set  "(" (Set (Var "seq"))  ($#k8_nat_1 :::"."::: )  (Set (Var "m")) ")" )  ($#k11_complex1 :::"-"::: )  (Set  "(" (Set (Var "seq"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n")) ")" ) ")" ) ($#k17_complex1 :::".|"::: ) )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "p"))))))  ")" )) ; 
 
theorem :: COMSEQ_3:47 (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::)  "st" (Bool (Bool (Set (Var "seq")) "is"   ($#v2_comseq_2 :::"convergent"::: )  )) "holds"  (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")) "," (Set (Var "l")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "m"))) & (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "l")))) "holds"  (Bool (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set  "(" (Set (Var "seq"))  ($#k8_nat_1 :::"."::: )  (Set (Var "m")) ")" )  ($#k11_complex1 :::"-"::: )  (Set  "(" (Set (Var "seq"))  ($#k8_nat_1 :::"."::: )  (Set (Var "l")) ")" ) ")" ) ($#k17_complex1 :::".|"::: ) )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "p"))))))) ; 
 
theorem :: COMSEQ_3:48 (Bool  "for" (Set (Var "rseq")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::)  "st" (Bool (Bool  "("   "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set (Var "seq"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n")) ")" ) ($#k17_complex1 :::".|"::: ) )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "rseq"))  ($#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_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "("  (Bool (Set (Var "seq")) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set   ($#k3_comseq_2 :::"lim"::: )  (Set (Var "seq")))  ($#r1_hidden :::"="::: )  (Set   ($#k5_complex1 :::"0c"::: )  ))  ")" ))) ; 
 begin  
theorem :: COMSEQ_3:49 (Bool  "for" (Set (Var "seq")) "," (Set (Var "seq1")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::)  "st" (Bool (Bool (Set (Var "seq")) "is"    ($#m2_valued_0 :::"subsequence"::: )   "of" (Set (Var "seq1")))) "holds"  (Bool  "("  (Bool (Set   ($#k7_comseq_3 :::"Re"::: )  (Set (Var "seq"))) "is"    ($#m2_valued_0 :::"subsequence"::: )   "of" (Set   ($#k7_comseq_3 :::"Re"::: )  (Set (Var "seq1")))) & (Bool (Set   ($#k8_comseq_3 :::"Im"::: )  (Set (Var "seq"))) "is"    ($#m2_valued_0 :::"subsequence"::: )   "of" (Set   ($#k8_comseq_3 :::"Im"::: )  (Set (Var "seq1"))))  ")" )) ; 
 
theorem :: COMSEQ_3:50 (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::)  "st" (Bool (Bool (Set (Var "seq")) "is"   ($#v1_comseq_2 :::"bounded"::: )  )) "holds"  (Bool  "ex" (Set (Var "seq1")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::) "st"  (Bool  "("  (Bool (Set (Var "seq1")) "is"    ($#m2_valued_0 :::"subsequence"::: )   "of" (Set (Var "seq"))) & (Bool (Set (Var "seq1")) "is"   ($#v2_comseq_2 :::"convergent"::: )  )  ")" ))) ; 
 definitionlet "seq" be   ($#m1_subset_1 :::"Complex_Sequence":::); attr "seq" is  :::"summable":::  means :: COMSEQ_3:def 8 (Bool (Set   ($#k10_comseq_3 :::"Partial_Sums"::: )  "seq") "is"   ($#v2_comseq_2 :::"convergent"::: )  ); end; 




:: deftheorem    defines :::"summable"::: COMSEQ_3:def 8 :  (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::) "holds"   (Bool  "("  (Bool (Set (Var "seq")) "is"   ($#v1_comseq_3 :::"summable"::: )  ) "iff" (Bool (Set   ($#k10_comseq_3 :::"Partial_Sums"::: )  (Set (Var "seq"))) "is"   ($#v2_comseq_2 :::"convergent"::: )  )  ")" )); 
 registration
cluster   ($#v1_relat_1 :::"Relation-like"::: )   (Set   ($#k5_numbers :::"NAT"::: )  )  ($#v4_relat_1 :::"-defined"::: )   (Set   ($#k2_numbers :::"COMPLEX"::: )  )  ($#v5_relat_1 :::"-valued"::: )     ($#v1_funct_1 :::"Function-like"::: )    ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"zero"::: )   )    ($#v1_partfun1 :::"total"::: )   bbbadV1_FUNCT_2((Set   ($#k5_numbers :::"NAT"::: )  ) "," (Set   ($#k2_numbers :::"COMPLEX"::: )  ))   ($#v1_valued_0 :::"complex-valued"::: )     ($#v1_comseq_3 :::"summable"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1((Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  ($#k2_numbers :::"COMPLEX"::: ) ))))); 
end; registrationlet "seq" be   ($#v1_comseq_3 :::"summable"::: )    ($#m1_subset_1 :::"Complex_Sequence":::); 
cluster (Set   ($#k2_series_1 :::"Partial_Sums"::: )  "seq") ->   ($#v2_comseq_2 :::"convergent"::: )    for  ($#m1_subset_1 :::"Complex_Sequence":::); 
end; definitionlet "seq" be   ($#m1_subset_1 :::"Complex_Sequence":::); attr "seq" is  :::"absolutely_summable":::  means :: COMSEQ_3:def 9 (Bool (Set  ($#k55_valued_1 :::"|."::: ) "seq" ($#k55_valued_1 :::".|"::: ) ) "is"   ($#v1_series_1 :::"summable"::: )  ); end; 




:: deftheorem    defines :::"absolutely_summable"::: COMSEQ_3:def 9 :  (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::) "holds"   (Bool  "("  (Bool (Set (Var "seq")) "is"   ($#v2_comseq_3 :::"absolutely_summable"::: )  ) "iff" (Bool (Set  ($#k55_valued_1 :::"|."::: ) (Set (Var "seq")) ($#k55_valued_1 :::".|"::: ) ) "is"   ($#v1_series_1 :::"summable"::: )  )  ")" )); 
 
theorem :: COMSEQ_3:51 (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::)  "st" (Bool (Bool  "("   "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "seq"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set   ($#k5_complex1 :::"0c"::: )  ))  ")" )) "holds"  (Bool (Set (Var "seq")) "is"   ($#v2_comseq_3 :::"absolutely_summable"::: )  )) ; 
 registration
cluster   ($#v1_relat_1 :::"Relation-like"::: )   (Set   ($#k5_numbers :::"NAT"::: )  )  ($#v4_relat_1 :::"-defined"::: )   (Set   ($#k2_numbers :::"COMPLEX"::: )  )  ($#v5_relat_1 :::"-valued"::: )     ($#v1_funct_1 :::"Function-like"::: )    ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"zero"::: )   )    ($#v1_partfun1 :::"total"::: )   bbbadV1_FUNCT_2((Set   ($#k5_numbers :::"NAT"::: )  ) "," (Set   ($#k2_numbers :::"COMPLEX"::: )  ))   ($#v1_valued_0 :::"complex-valued"::: )     ($#v2_comseq_3 :::"absolutely_summable"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1((Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  ($#k2_numbers :::"COMPLEX"::: ) ))))); 
end; registrationlet "seq" be   ($#v2_comseq_3 :::"absolutely_summable"::: )    ($#m1_subset_1 :::"Complex_Sequence":::); 
cluster (Set  ($#k54_valued_1 :::"|."::: ) "seq" ($#k54_valued_1 :::".|"::: ) ) ->   ($#v1_series_1 :::"summable"::: )    for  ($#m1_subset_1 :::"Real_Sequence":::); 
end; 
theorem :: COMSEQ_3:52 (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::)  "st" (Bool (Bool (Set (Var "seq")) "is"   ($#v1_comseq_3 :::"summable"::: )  )) "holds"  (Bool  "("  (Bool (Set (Var "seq")) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set   ($#k3_comseq_2 :::"lim"::: )  (Set (Var "seq")))  ($#r1_hidden :::"="::: )  (Set   ($#k5_complex1 :::"0c"::: )  ))  ")" )) ; 
 registration
cluster   ($#v1_funct_1 :::"Function-like"::: )   bbbadV1_FUNCT_2((Set   ($#k5_numbers :::"NAT"::: )  ) "," (Set   ($#k2_numbers :::"COMPLEX"::: )  ))   ($#v1_comseq_3 :::"summable"::: )    ->   ($#v2_comseq_2 :::"convergent"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1((Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  ($#k2_numbers :::"COMPLEX"::: ) ))))); 
end; 
theorem :: COMSEQ_3:53 (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::)  "st" (Bool (Bool (Set (Var "seq")) "is"   ($#v1_comseq_3 :::"summable"::: )  )) "holds"  (Bool  "("  (Bool (Set   ($#k7_comseq_3 :::"Re"::: )  (Set (Var "seq"))) "is"   ($#v1_series_1 :::"summable"::: )  ) & (Bool (Set   ($#k8_comseq_3 :::"Im"::: )  (Set (Var "seq"))) "is"   ($#v1_series_1 :::"summable"::: )  ) & (Bool (Set   ($#k11_comseq_3 :::"Sum"::: )  (Set (Var "seq")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_series_1 :::"Sum"::: )  (Set  "("  ($#k7_comseq_3 :::"Re"::: )  (Set (Var "seq")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  "("  ($#k4_series_1 :::"Sum"::: )  (Set  "("  ($#k8_comseq_3 :::"Im"::: )  (Set (Var "seq")) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  ($#k7_complex1 :::"<i>"::: ) ) ")" )))  ")" )) ; 
 registrationlet "seq" be   ($#v1_comseq_3 :::"summable"::: )    ($#m1_subset_1 :::"Complex_Sequence":::); 
cluster (Set   ($#k3_comseq_3 :::"Re"::: )  "seq") ->   ($#v1_series_1 :::"summable"::: )    for  ($#m1_subset_1 :::"Real_Sequence":::); 

cluster (Set   ($#k4_comseq_3 :::"Im"::: )  "seq") ->   ($#v1_series_1 :::"summable"::: )    for  ($#m1_subset_1 :::"Real_Sequence":::); 
end; 
theorem :: COMSEQ_3:54 (Bool  "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::)  "st" (Bool (Bool (Set (Var "seq1")) "is"   ($#v1_comseq_3 :::"summable"::: )  ) & (Bool (Set (Var "seq2")) "is"   ($#v1_comseq_3 :::"summable"::: )  )) "holds"  (Bool  "("  (Bool (Set (Set (Var "seq1"))  ($#k1_series_1 :::"+"::: )  (Set (Var "seq2"))) "is"   ($#v1_comseq_3 :::"summable"::: )  ) & (Bool (Set   ($#k11_comseq_3 :::"Sum"::: )  (Set  "(" (Set (Var "seq1"))  ($#k1_series_1 :::"+"::: )  (Set (Var "seq2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k11_comseq_3 :::"Sum"::: )  (Set (Var "seq1")) ")" )  ($#k8_complex1 :::"+"::: )  (Set  "("  ($#k11_comseq_3 :::"Sum"::: )  (Set (Var "seq2")) ")" )))  ")" )) ; 
 
theorem :: COMSEQ_3:55 (Bool  "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::)  "st" (Bool (Bool (Set (Var "seq1")) "is"   ($#v1_comseq_3 :::"summable"::: )  ) & (Bool (Set (Var "seq2")) "is"   ($#v1_comseq_3 :::"summable"::: )  )) "holds"  (Bool  "("  (Bool (Set (Set (Var "seq1"))  ($#k46_valued_1 :::"-"::: )  (Set (Var "seq2"))) "is"   ($#v1_comseq_3 :::"summable"::: )  ) & (Bool (Set   ($#k11_comseq_3 :::"Sum"::: )  (Set  "(" (Set (Var "seq1"))  ($#k46_valued_1 :::"-"::: )  (Set (Var "seq2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k11_comseq_3 :::"Sum"::: )  (Set (Var "seq1")) ")" )  ($#k11_complex1 :::"-"::: )  (Set  "("  ($#k11_comseq_3 :::"Sum"::: )  (Set (Var "seq2")) ")" )))  ")" )) ; 
 registrationlet "seq1", "seq2" be   ($#v1_comseq_3 :::"summable"::: )    ($#m1_subset_1 :::"Complex_Sequence":::); 
cluster (Set "seq1"  ($#k1_valued_1 :::"+"::: )  "seq2") ->   ($#v1_comseq_3 :::"summable"::: )    for  ($#m1_subset_1 :::"Complex_Sequence":::); 

cluster (Set "seq1"  ($#k45_valued_1 :::"-"::: )  "seq2") ->   ($#v1_comseq_3 :::"summable"::: )    for  ($#m1_subset_1 :::"Complex_Sequence":::); 
end; 
theorem :: COMSEQ_3:56 (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::)  "st" (Bool (Bool (Set (Var "seq")) "is"   ($#v1_comseq_3 :::"summable"::: )  )) "holds"  (Bool  "for" (Set (Var "z")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("  (Bool (Set (Set (Var "z"))  ($#k25_valued_1 :::"(#)"::: )  (Set (Var "seq"))) "is"   ($#v1_comseq_3 :::"summable"::: )  ) & (Bool (Set   ($#k11_comseq_3 :::"Sum"::: )  (Set  "(" (Set (Var "z"))  ($#k25_valued_1 :::"(#)"::: )  (Set (Var "seq")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "z"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k11_comseq_3 :::"Sum"::: )  (Set (Var "seq")) ")" )))  ")" ))) ; 
 registrationlet "z" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  ); let "seq" be   ($#v1_comseq_3 :::"summable"::: )    ($#m1_subset_1 :::"Complex_Sequence":::); 
cluster (Set "z"  ($#k24_valued_1 :::"(#)"::: )  "seq") ->   ($#v1_comseq_3 :::"summable"::: )    for  ($#m1_subset_1 :::"Complex_Sequence":::); 
end; 
theorem :: COMSEQ_3:57 (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::)  "st" (Bool (Bool (Set   ($#k7_comseq_3 :::"Re"::: )  (Set (Var "seq"))) "is"   ($#v1_series_1 :::"summable"::: )  ) & (Bool (Set   ($#k8_comseq_3 :::"Im"::: )  (Set (Var "seq"))) "is"   ($#v1_series_1 :::"summable"::: )  )) "holds"  (Bool  "("  (Bool (Set (Var "seq")) "is"   ($#v1_comseq_3 :::"summable"::: )  ) & (Bool (Set   ($#k11_comseq_3 :::"Sum"::: )  (Set (Var "seq")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_series_1 :::"Sum"::: )  (Set  "("  ($#k7_comseq_3 :::"Re"::: )  (Set (Var "seq")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  "("  ($#k4_series_1 :::"Sum"::: )  (Set  "("  ($#k8_comseq_3 :::"Im"::: )  (Set (Var "seq")) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  ($#k7_complex1 :::"<i>"::: ) ) ")" )))  ")" )) ; 
 
theorem :: COMSEQ_3:58 (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::)  "st" (Bool (Bool (Set (Var "seq")) "is"   ($#v1_comseq_3 :::"summable"::: )  )) "holds"  (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "seq"))  ($#k1_valued_0 :::"^\"::: )  (Set (Var "n"))) "is"   ($#v1_comseq_3 :::"summable"::: )  ))) ; 
 registrationlet "seq" be   ($#v1_comseq_3 :::"summable"::: )    ($#m1_subset_1 :::"Complex_Sequence":::); let "n" be    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); 
cluster (Set "seq"  ($#k9_nat_1 :::"^\"::: )  "n") ->   ($#v1_comseq_3 :::"summable"::: )    for  ($#m1_subset_1 :::"Complex_Sequence":::); 
end; 
theorem :: COMSEQ_3:59 (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::)  "st" (Bool (Bool  "ex" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st" (Bool (Set (Set (Var "seq"))  ($#k1_valued_0 :::"^\"::: )  (Set (Var "n"))) "is"   ($#v1_comseq_3 :::"summable"::: )  ))) "holds"  (Bool (Set (Var "seq")) "is"   ($#v1_comseq_3 :::"summable"::: )  )) ; 
 
theorem :: COMSEQ_3:60 (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::)  "st" (Bool (Bool (Set (Var "seq")) "is"   ($#v1_comseq_3 :::"summable"::: )  )) "holds"  (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set   ($#k11_comseq_3 :::"Sum"::: )  (Set (Var "seq")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k10_comseq_3 :::"Partial_Sums"::: )  (Set (Var "seq")) ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "n")) ")" )  ($#k8_complex1 :::"+"::: )  (Set  "("  ($#k11_comseq_3 :::"Sum"::: )  (Set  "(" (Set (Var "seq"))  ($#k1_valued_0 :::"^\"::: )  (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" ) ")" ))))) ; 
 
theorem :: COMSEQ_3:61 (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::) "holds"   (Bool  "("  (Bool (Set   ($#k3_series_1 :::"Partial_Sums"::: )  (Set  ($#k55_valued_1 :::"|."::: ) (Set (Var "seq")) ($#k55_valued_1 :::".|"::: ) )) "is"   ($#v1_seq_2 :::"bounded_above"::: )  ) "iff" (Bool (Set (Var "seq")) "is"   ($#v2_comseq_3 :::"absolutely_summable"::: )  )  ")" )) ; 
 registrationlet "seq" be   ($#v2_comseq_3 :::"absolutely_summable"::: )    ($#m1_subset_1 :::"Complex_Sequence":::); 
cluster (Set   ($#k2_series_1 :::"Partial_Sums"::: )  (Set  ($#k55_valued_1 :::"|."::: ) "seq" ($#k55_valued_1 :::".|"::: ) )) ->   ($#v1_seq_2 :::"bounded_above"::: )    for  ($#m1_subset_1 :::"Real_Sequence":::); 
end; 
theorem :: COMSEQ_3:62 (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::) "holds"   (Bool  "("  (Bool (Set (Var "seq")) "is"   ($#v1_comseq_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  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set  "(" (Set  "("  ($#k10_comseq_3 :::"Partial_Sums"::: )  (Set (Var "seq")) ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "m")) ")" )  ($#k11_complex1 :::"-"::: )  (Set  "(" (Set  "("  ($#k10_comseq_3 :::"Partial_Sums"::: )  (Set (Var "seq")) ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "n")) ")" ) ")" ) ($#k17_complex1 :::".|"::: ) )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "p"))))))  ")" )) ; 
 
theorem :: COMSEQ_3:63 (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::)  "st" (Bool (Bool (Set (Var "seq")) "is"   ($#v2_comseq_3 :::"absolutely_summable"::: )  )) "holds"  (Bool (Set (Var "seq")) "is"   ($#v1_comseq_3 :::"summable"::: )  )) ; 
 registration
cluster   ($#v1_funct_1 :::"Function-like"::: )   bbbadV1_FUNCT_2((Set   ($#k5_numbers :::"NAT"::: )  ) "," (Set   ($#k2_numbers :::"COMPLEX"::: )  ))   ($#v2_comseq_3 :::"absolutely_summable"::: )    ->   ($#v1_comseq_3 :::"summable"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1((Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  ($#k2_numbers :::"COMPLEX"::: ) ))))); 
end; registration
cluster   ($#v1_relat_1 :::"Relation-like"::: )   (Set   ($#k5_numbers :::"NAT"::: )  )  ($#v4_relat_1 :::"-defined"::: )   (Set   ($#k2_numbers :::"COMPLEX"::: )  )  ($#v5_relat_1 :::"-valued"::: )     ($#v1_funct_1 :::"Function-like"::: )    ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"zero"::: )   )    ($#v1_partfun1 :::"total"::: )   bbbadV1_FUNCT_2((Set   ($#k5_numbers :::"NAT"::: )  ) "," (Set   ($#k2_numbers :::"COMPLEX"::: )  ))   ($#v1_valued_0 :::"complex-valued"::: )     ($#v2_comseq_3 :::"absolutely_summable"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1((Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  ($#k2_numbers :::"COMPLEX"::: ) ))))); 
end; 
theorem :: COMSEQ_3:64 (Bool  "for" (Set (Var "z")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  )  "st" (Bool (Bool (Set  ($#k17_complex1 :::"|."::: ) (Set (Var "z")) ($#k17_complex1 :::".|"::: ) )  ($#r1_xxreal_0 :::"<"::: )  (Num 1))) "holds"  (Bool  "("  (Bool (Set (Set (Var "z"))  ($#k1_comseq_3 :::"GeoSeq"::: )  ) "is"   ($#v1_comseq_3 :::"summable"::: )  ) & (Bool (Set   ($#k11_comseq_3 :::"Sum"::: )  (Set  "(" (Set (Var "z"))  ($#k1_comseq_3 :::"GeoSeq"::: )  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k6_complex1 :::"1r"::: ) )  ($#k13_complex1 :::"/"::: )  (Set  "(" (Set  ($#k6_complex1 :::"1r"::: ) )  ($#k11_complex1 :::"-"::: )  (Set (Var "z")) ")" )))  ")" )) ; 
 
theorem :: COMSEQ_3:65 (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::)  (Bool  "for" (Set (Var "z")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  )  "st" (Bool (Bool (Set  ($#k17_complex1 :::"|."::: ) (Set (Var "z")) ($#k17_complex1 :::".|"::: ) )  ($#r1_xxreal_0 :::"<"::: )  (Num 1)) & (Bool  "("   "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "seq"))  ($#k8_nat_1 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "z"))  ($#k9_complex1 :::"*"::: )  (Set  "(" (Set (Var "seq"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n")) ")" )))  ")" )) "holds"  (Bool  "("  (Bool (Set (Var "seq")) "is"   ($#v1_comseq_3 :::"summable"::: )  ) & (Bool (Set   ($#k11_comseq_3 :::"Sum"::: )  (Set (Var "seq")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "seq"))  ($#k8_nat_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" )  ($#k13_complex1 :::"/"::: )  (Set  "(" (Set  ($#k6_complex1 :::"1r"::: ) )  ($#k11_complex1 :::"-"::: )  (Set (Var "z")) ")" )))  ")" ))) ; 
 
theorem :: COMSEQ_3:66 (Bool  "for" (Set (Var "rseq1")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  (Bool  "for" (Set (Var "seq2")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::)  "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  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set (Var "seq2"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n")) ")" ) ($#k17_complex1 :::".|"::: ) )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "rseq1"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n"))))))) "holds"  (Bool (Set (Var "seq2")) "is"   ($#v2_comseq_3 :::"absolutely_summable"::: )  ))) ; 
 
theorem :: COMSEQ_3:67 (Bool  "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::)  "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  ($#k55_valued_1 :::"|."::: ) (Set (Var "seq1")) ($#k55_valued_1 :::".|"::: ) )  ($#k8_nat_1 :::"."::: )  (Set (Var "n")))) & (Bool (Set (Set  ($#k55_valued_1 :::"|."::: ) (Set (Var "seq1")) ($#k55_valued_1 :::".|"::: ) )  ($#k8_nat_1 :::"."::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  ($#k55_valued_1 :::"|."::: ) (Set (Var "seq2")) ($#k55_valued_1 :::".|"::: ) )  ($#k8_nat_1 :::"."::: )  (Set (Var "n"))))  ")" )  ")" ) & (Bool (Set (Var "seq2")) "is"   ($#v2_comseq_3 :::"absolutely_summable"::: )  )) "holds"  (Bool  "("  (Bool (Set (Var "seq1")) "is"   ($#v2_comseq_3 :::"absolutely_summable"::: )  ) & (Bool (Set   ($#k4_series_1 :::"Sum"::: )  (Set  ($#k55_valued_1 :::"|."::: ) (Set (Var "seq1")) ($#k55_valued_1 :::".|"::: ) ))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k4_series_1 :::"Sum"::: )  (Set  ($#k55_valued_1 :::"|."::: ) (Set (Var "seq2")) ($#k55_valued_1 :::".|"::: ) )))  ")" )) ; 
 
theorem :: COMSEQ_3:68 (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::)  "st" (Bool (Bool  "("   "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "holds" (Bool (Set (Set  ($#k55_valued_1 :::"|."::: ) (Set (Var "seq")) ($#k55_valued_1 :::".|"::: ) )  ($#k8_nat_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  ($#k55_valued_1 :::"|."::: ) (Set (Var "seq")) ($#k55_valued_1 :::".|"::: ) )  ($#k8_nat_1 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  ($#k55_valued_1 :::"|."::: ) (Set (Var "seq")) ($#k55_valued_1 :::".|"::: ) )  ($#k8_nat_1 :::"."::: )  (Set (Var "n")) ")" ))  ($#r1_xxreal_0 :::">="::: )  (Num 1))))) "holds"  (Bool  "not" (Bool (Set (Var "seq")) "is"   ($#v2_comseq_3 :::"absolutely_summable"::: )  ))) ; 
 
theorem :: COMSEQ_3:69 (Bool  "for" (Set (Var "rseq1")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::)  "st" (Bool (Bool  "("   "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "rseq1"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k2_power :::"-root"::: )  (Set  "(" (Set  ($#k55_valued_1 :::"|."::: ) (Set (Var "seq")) ($#k55_valued_1 :::".|"::: ) )  ($#k8_nat_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_comseq_3 :::"absolutely_summable"::: )  ))) ; 
 
theorem :: COMSEQ_3:70 (Bool  "for" (Set (Var "rseq1")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::)  "st" (Bool (Bool  "("   "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "rseq1"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k2_power :::"-root"::: )  (Set  "(" (Set  ($#k55_valued_1 :::"|."::: ) (Set (Var "seq")) ($#k55_valued_1 :::".|"::: ) )  ($#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 "m"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool (Set (Set (Var "rseq1"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::">="::: )  (Num 1))))) "holds"  (Bool  "not" (Bool (Set  ($#k55_valued_1 :::"|."::: ) (Set (Var "seq")) ($#k55_valued_1 :::".|"::: ) ) "is"   ($#v1_series_1 :::"summable"::: )  )))) ; 
 
theorem :: COMSEQ_3:71 (Bool  "for" (Set (Var "rseq1")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::)  "st" (Bool (Bool  "("   "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "rseq1"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k2_power :::"-root"::: )  (Set  "(" (Set  ($#k55_valued_1 :::"|."::: ) (Set (Var "seq")) ($#k55_valued_1 :::".|"::: ) )  ($#k8_nat_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_comseq_3 :::"absolutely_summable"::: )  )))) ; 
 
theorem :: COMSEQ_3:72 (Bool  "for" (Set (Var "rseq1")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::)  "st" (Bool (Bool (Set  ($#k55_valued_1 :::"|."::: ) (Set (Var "seq")) ($#k55_valued_1 :::".|"::: ) ) "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"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 2)  ($#k4_power :::"to_power"::: )  (Set (Var "n")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  ($#k55_valued_1 :::"|."::: ) (Set (Var "seq")) ($#k55_valued_1 :::".|"::: ) )  ($#k8_nat_1 :::"."::: )  (Set  "(" (Num 2)  ($#k4_power :::"to_power"::: )  (Set (Var "n")) ")" ) ")" )))  ")" )) "holds"  (Bool  "("  (Bool (Set (Var "seq")) "is"   ($#v2_comseq_3 :::"absolutely_summable"::: )  ) "iff" (Bool (Set (Var "rseq1")) "is"   ($#v1_series_1 :::"summable"::: )  )  ")" ))) ; 
 
theorem :: COMSEQ_3:73 (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::)  (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  ($#k55_valued_1 :::"|."::: ) (Set (Var "seq")) ($#k55_valued_1 :::".|"::: ) )  ($#k8_nat_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_comseq_3 :::"absolutely_summable"::: )  ))) ; 
 
theorem :: COMSEQ_3:74 (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::)  (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  ($#k55_valued_1 :::"|."::: ) (Set (Var "seq")) ($#k55_valued_1 :::".|"::: ) )  ($#k8_nat_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_comseq_3 :::"absolutely_summable"::: )  )))) ; 
 
theorem :: COMSEQ_3:75 (Bool  "for" (Set (Var "rseq1")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Complex_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"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k5_complex1 :::"0c"::: )  )) & (Bool (Set (Set (Var "rseq1"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  ($#k55_valued_1 :::"|."::: ) (Set (Var "seq")) ($#k55_valued_1 :::".|"::: ) )  ($#k8_nat_1 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  ($#k55_valued_1 :::"|."::: ) (Set (Var "seq")) ($#k55_valued_1 :::".|"::: ) )  ($#k8_nat_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_comseq_3 :::"absolutely_summable"::: )  ))) ; 
 
theorem :: COMSEQ_3:76 (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::)  "st" (Bool (Bool  "("   "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "holds" (Bool (Set (Set (Var "seq"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k5_complex1 :::"0c"::: )  ))  ")" ) & (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  ($#k55_valued_1 :::"|."::: ) (Set (Var "seq")) ($#k55_valued_1 :::".|"::: ) )  ($#k8_nat_1 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  ($#k55_valued_1 :::"|."::: ) (Set (Var "seq")) ($#k55_valued_1 :::".|"::: ) )  ($#k8_nat_1 :::"."::: )  (Set (Var "n")) ")" ))  ($#r1_xxreal_0 :::">="::: )  (Num 1))))) "holds"  (Bool  "not" (Bool (Set (Var "seq")) "is"   ($#v2_comseq_3 :::"absolutely_summable"::: )  ))) ;