:: COMSEQ_2  semantic presentation begin  






















theorem :: COMSEQ_2:1 (Bool  "for" (Set (Var "g")) "," (Set (Var "r")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  )  "st" (Bool (Bool (Set (Var "g"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k5_complex1 :::"0c"::: )  )) & (Bool (Set (Var "r"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k5_complex1 :::"0c"::: )  ))) "holds"  (Bool (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set  "(" (Set (Var "g"))  ($#k12_complex1 :::"""::: )  ")" )  ($#k11_complex1 :::"-"::: )  (Set  "(" (Set (Var "r"))  ($#k12_complex1 :::"""::: )  ")" ) ")" ) ($#k17_complex1 :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set (Var "g"))  ($#k11_complex1 :::"-"::: )  (Set (Var "r")) ")" ) ($#k17_complex1 :::".|"::: ) )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  ($#k17_complex1 :::"|."::: ) (Set (Var "g")) ($#k17_complex1 :::".|"::: ) )  ($#k8_real_1 :::"*"::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set (Var "r")) ($#k17_complex1 :::".|"::: ) ) ")" )))) ; 
 
theorem :: COMSEQ_2:2 (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::)  (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) (Bool  "ex" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::) "st"  (Bool  "("  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r"))) & (Bool  "("   "for" (Set (Var "m")) "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 "s"))  ($#k8_nat_1 :::"."::: )  (Set (Var "m")) ")" ) ($#k17_complex1 :::".|"::: ) )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r")))  ")" )  ")" )))) ; 
 begin  definitionlet "f" be   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"Function":::); func "f" :::"*'":::  ->   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"Function":::) means :: COMSEQ_2:def 1 (Bool  "("  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  it)  ($#r1_hidden :::"="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  "f")) & (Bool  "("   "for" (Set (Var "c")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "c"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  it))) "holds"  (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" "f"  ($#k1_funct_1 :::"."::: )  (Set (Var "c")) ")" )  ($#k15_complex1 :::"*'"::: )  ))  ")" )  ")" ); involutiveness  
(Bool  "for" (Set (Var "b1")) "," (Set (Var "b2")) "being"   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "b1")))  ($#r1_hidden :::"="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "b2")))) & (Bool  "("   "for" (Set (Var "c")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "c"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "b1"))))) "holds"  (Bool (Set (Set (Var "b1"))  ($#k1_funct_1 :::"."::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "b2"))  ($#k1_funct_1 :::"."::: )  (Set (Var "c")) ")" )  ($#k15_complex1 :::"*'"::: )  ))  ")" )) "holds"  (Bool  "("  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "b2")))  ($#r1_hidden :::"="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "b1")))) & (Bool  "("   "for" (Set (Var "c")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "c"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "b2"))))) "holds"  (Bool (Set (Set (Var "b2"))  ($#k1_funct_1 :::"."::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "b1"))  ($#k1_funct_1 :::"."::: )  (Set (Var "c")) ")" )  ($#k15_complex1 :::"*'"::: )  ))  ")" )  ")" ))
 ; end; 





:: deftheorem    defines :::"*'"::: COMSEQ_2:def 1 :  (Bool  "for" (Set (Var "f")) "," (Set (Var "b2")) "being"   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"Function":::) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_comseq_2 :::"*'"::: )  )) "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 "c")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "c"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "b2"))))) "holds"  (Bool (Set (Set (Var "b2"))  ($#k1_funct_1 :::"."::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "c")) ")" )  ($#k15_complex1 :::"*'"::: )  ))  ")" )  ")" )  ")" )); 
 definitionlet "C" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "f" be   ($#m1_subset_1 :::"Function":::) "of" (Set (Const "C")) "," (Set  ($#k2_numbers :::"COMPLEX"::: ) ); :: original: :::"*'"::: redefine func "f" :::"*'":::  ->   ($#m1_subset_1 :::"Function":::) "of" "C" "," (Set  ($#k2_numbers :::"COMPLEX"::: ) ) means :: COMSEQ_2:def 2 (Bool  "("  (Bool (Set   ($#k1_relset_1 :::"dom"::: )  it)  ($#r1_hidden :::"="::: )  "C") & (Bool  "("   "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" "C" "holds"  (Bool (Set it  ($#k3_funct_2 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" "f"  ($#k3_funct_2 :::"."::: )  (Set (Var "n")) ")" )  ($#k15_complex1 :::"*'"::: )  ))  ")" )  ")" ); end; 






:: deftheorem    defines :::"*'"::: COMSEQ_2:def 2 :  (Bool  "for" (Set (Var "C")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "," (Set (Var "b3")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C")) "," (Set  ($#k2_numbers :::"COMPLEX"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k2_comseq_2 :::"*'"::: )  )) "iff" (Bool  "("  (Bool (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "b3")))  ($#r1_hidden :::"="::: )  (Set (Var "C"))) & (Bool  "("   "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "C")) "holds"  (Bool (Set (Set (Var "b3"))  ($#k3_funct_2 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "n")) ")" )  ($#k15_complex1 :::"*'"::: )  ))  ")" )  ")" )  ")" ))); 
 registrationlet "C" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "s" be   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "C")); 
cluster (Set "s"  ($#k1_comseq_2 :::"*'"::: )  ) -> "C"  ($#v4_relat_1 :::"-defined"::: )     ($#v1_valued_0 :::"complex-valued"::: )   ; 
end; registrationlet "C" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "seq" be   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "C")); 
cluster (Set "seq"  ($#k1_comseq_2 :::"*'"::: )  ) -> "C"  ($#v4_relat_1 :::"-defined"::: )     ($#v1_partfun1 :::"total"::: )    for"C"  ($#v4_relat_1 :::"-defined"::: )    ($#m1_hidden :::"Function":::); 
end; 
theorem :: COMSEQ_2:3 (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::)  "st" (Bool (Bool (Set (Var "s")) "is"   ($#v2_relat_1 :::"non-zero"::: )  )) "holds"  (Bool (Set (Set (Var "s"))  ($#k2_comseq_2 :::"*'"::: )  ) "is"   ($#v2_relat_1 :::"non-zero"::: )  )) ; 
 
theorem :: COMSEQ_2:4 (Bool  "for" (Set (Var "r")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  )  (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::) "holds"  (Bool (Set (Set  "(" (Set (Var "r"))  ($#k25_valued_1 :::"(#)"::: )  (Set (Var "s")) ")" )  ($#k2_comseq_2 :::"*'"::: )  )  ($#r2_funct_2 :::"="::: )  (Set (Set  "(" (Set (Var "r"))  ($#k15_complex1 :::"*'"::: )  ")" )  ($#k25_valued_1 :::"(#)"::: )  (Set  "(" (Set (Var "s"))  ($#k2_comseq_2 :::"*'"::: )  ")" ))))) ; 
 
theorem :: COMSEQ_2:5 (Bool  "for" (Set (Var "s")) "," (Set (Var "s9")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::) "holds"  (Bool (Set (Set  "(" (Set (Var "s"))  ($#k19_valued_1 :::"(#)"::: )  (Set (Var "s9")) ")" )  ($#k2_comseq_2 :::"*'"::: )  )  ($#r2_funct_2 :::"="::: )  (Set (Set  "(" (Set (Var "s"))  ($#k2_comseq_2 :::"*'"::: )  ")" )  ($#k19_valued_1 :::"(#)"::: )  (Set  "(" (Set (Var "s9"))  ($#k2_comseq_2 :::"*'"::: )  ")" )))) ; 
 
theorem :: COMSEQ_2:6 (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::) "holds"  (Bool (Set (Set  "(" (Set (Var "s"))  ($#k2_comseq_2 :::"*'"::: )  ")" )  ($#k36_valued_1 :::"""::: )  )  ($#r2_funct_2 :::"="::: )  (Set (Set  "(" (Set (Var "s"))  ($#k36_valued_1 :::"""::: )  ")" )  ($#k2_comseq_2 :::"*'"::: )  ))) ; 
 
theorem :: COMSEQ_2:7 (Bool  "for" (Set (Var "s9")) "," (Set (Var "s")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::) "holds"  (Bool (Set (Set  "(" (Set (Var "s9"))  ($#k51_valued_1 :::"/""::: )  (Set (Var "s")) ")" )  ($#k2_comseq_2 :::"*'"::: )  )  ($#r2_funct_2 :::"="::: )  (Set (Set  "(" (Set (Var "s9"))  ($#k2_comseq_2 :::"*'"::: )  ")" )  ($#k51_valued_1 :::"/""::: )  (Set  "(" (Set (Var "s"))  ($#k2_comseq_2 :::"*'"::: )  ")" )))) ; 
 begin  definitionlet "f" be   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"Function":::); attr "f" is  :::"bounded":::  means :: COMSEQ_2:def 3 (Bool  "ex" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "for" (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  "f"))) "holds"  (Bool (Set   ($#k18_complex1 :::"abs"::: )  (Set  "(" "f"  ($#k1_funct_1 :::"."::: )  (Set (Var "y")) ")" ))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r"))))); end; 




:: deftheorem    defines :::"bounded"::: COMSEQ_2:def 3 :  (Bool  "for" (Set (Var "f")) "being"   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"Function":::) "holds"   (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v1_comseq_2 :::"bounded"::: )  ) "iff" (Bool  "ex" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "for" (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f"))))) "holds"  (Bool (Set   ($#k18_complex1 :::"abs"::: )  (Set  "(" (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "y")) ")" ))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r")))))  ")" )); 
 definitionlet "s" be   ($#m1_subset_1 :::"Complex_Sequence":::); redefine attr "s" is  :::"bounded":::  means :: COMSEQ_2:def 4 (Bool  "ex" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::) "st"  (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "holds" (Bool (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" "s"  ($#k8_nat_1 :::"."::: )  (Set (Var "n")) ")" ) ($#k17_complex1 :::".|"::: ) )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r"))))); end; 




:: deftheorem    defines :::"bounded"::: COMSEQ_2:def 4 :  (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::) "holds"   (Bool  "("  (Bool (Set (Var "s")) "is"   ($#v1_comseq_2 :::"bounded"::: )  ) "iff" (Bool  "ex" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::) "st"  (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "holds" (Bool (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set (Var "s"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n")) ")" ) ($#k17_complex1 :::".|"::: ) )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r")))))  ")" )); 
 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 :::"empty"::: )   )    ($#v1_partfun1 :::"total"::: )   bbbadV1_FUNCT_2((Set   ($#k5_numbers :::"NAT"::: )  ) "," (Set   ($#k2_numbers :::"COMPLEX"::: )  ))   ($#v1_valued_0 :::"complex-valued"::: )     ($#v1_comseq_2 :::"bounded"::: )    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_2:8 (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::) "holds"   (Bool  "("  (Bool (Set (Var "s")) "is"   ($#v1_comseq_2 :::"bounded"::: )  ) "iff" (Bool  "ex" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::) "st"  (Bool  "("  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r"))) & (Bool  "("   "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "holds" (Bool (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set (Var "s"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n")) ")" ) ($#k17_complex1 :::".|"::: ) )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r")))  ")" )  ")" ))  ")" )) ; 
 begin  definitionlet "s" be   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"ManySortedSet":::) "of" (Set   ($#k5_numbers :::"NAT"::: )  ); attr "s" is  :::"convergent":::  means :: COMSEQ_2:def 5 (Bool  "ex" (Set (Var "g")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  ) "st"  (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  "(" "s"  ($#k1_funct_1 :::"."::: )  (Set (Var "m")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "g")) ")" ) ($#k17_complex1 :::".|"::: ) )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "p"))))))); end; 




:: deftheorem    defines :::"convergent"::: COMSEQ_2:def 5 :  (Bool  "for" (Set (Var "s")) "being"   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"ManySortedSet":::) "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"   (Bool  "("  (Bool (Set (Var "s")) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) "iff" (Bool  "ex" (Set (Var "g")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  ) "st"  (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 "s"))  ($#k1_funct_1 :::"."::: )  (Set (Var "m")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "g")) ")" ) ($#k17_complex1 :::".|"::: ) )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "p")))))))  ")" )); 
 definitionlet "s" be   ($#m1_subset_1 :::"Complex_Sequence":::); assume 
(Bool (Set (Const "s")) "is"   ($#v2_comseq_2 :::"convergent"::: )  )
 ; func  :::"lim"::: "s" ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  ) means :: COMSEQ_2:def 6 (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  "(" "s"  ($#k8_nat_1 :::"."::: )  (Set (Var "m")) ")" )  ($#k11_complex1 :::"-"::: )  it ")" ) ($#k17_complex1 :::".|"::: ) )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "p")))))); end; 






:: deftheorem    defines :::"lim"::: COMSEQ_2:def 6 :  (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::)  "st" (Bool (Bool (Set (Var "s")) "is"   ($#v2_comseq_2 :::"convergent"::: )  )) "holds"  (Bool  "for" (Set (Var "b2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  ) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_comseq_2 :::"lim"::: )  (Set (Var "s")))) "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 "s"))  ($#k8_nat_1 :::"."::: )  (Set (Var "m")) ")" )  ($#k11_complex1 :::"-"::: )  (Set (Var "b2")) ")" ) ($#k17_complex1 :::".|"::: ) )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "p"))))))  ")" ))); 
 
theorem :: COMSEQ_2:9 (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::)  "st" (Bool (Bool  "ex" (Set (Var "g")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  ) "st"  (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "s"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Var "g")))))) "holds"  (Bool (Set (Var "s")) "is"   ($#v2_comseq_2 :::"convergent"::: )  )) ; 
 
theorem :: COMSEQ_2:10 (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::)  (Bool  "for" (Set (Var "g")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  )  "st" (Bool (Bool  "("   "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "s"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Var "g")))  ")" )) "holds"  (Bool (Set   ($#k3_comseq_2 :::"lim"::: )  (Set (Var "s")))  ($#r1_hidden :::"="::: )  (Set (Var "g"))))) ; 
 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 :::"empty"::: )   )    ($#v1_partfun1 :::"total"::: )   bbbadV1_FUNCT_2((Set   ($#k5_numbers :::"NAT"::: )  ) "," (Set   ($#k2_numbers :::"COMPLEX"::: )  ))   ($#v1_valued_0 :::"complex-valued"::: )     ($#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; registrationlet "s" be   ($#v2_comseq_2 :::"convergent"::: )    ($#m1_subset_1 :::"Complex_Sequence":::); 
cluster (Set "s"  ($#k1_comseq_2 :::"*'"::: )  ) ->   ($#v2_comseq_2 :::"convergent"::: )    for  ($#m1_subset_1 :::"Complex_Sequence":::); 
end; 
theorem :: COMSEQ_2:11 canceled; 
 
theorem :: COMSEQ_2:12 (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::)  "st" (Bool (Bool (Set (Var "s")) "is"   ($#v2_comseq_2 :::"convergent"::: )  )) "holds"  (Bool (Set   ($#k3_comseq_2 :::"lim"::: )  (Set  "(" (Set (Var "s"))  ($#k2_comseq_2 :::"*'"::: )  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_comseq_2 :::"lim"::: )  (Set (Var "s")) ")" )  ($#k15_complex1 :::"*'"::: )  ))) ; 
 begin  registrationlet "s1", "s2" be   ($#v2_comseq_2 :::"convergent"::: )    ($#m1_subset_1 :::"Complex_Sequence":::); 
cluster (Set "s1"  ($#k1_valued_1 :::"+"::: )  "s2") ->   ($#v2_comseq_2 :::"convergent"::: )    for  ($#m1_subset_1 :::"Complex_Sequence":::); 
end; 
theorem :: COMSEQ_2:13 canceled; 
 
theorem :: COMSEQ_2:14 (Bool  "for" (Set (Var "s")) "," (Set (Var "s9")) "being"   ($#v2_comseq_2 :::"convergent"::: )    ($#m1_subset_1 :::"Complex_Sequence":::) "holds"  (Bool (Set   ($#k3_comseq_2 :::"lim"::: )  (Set  "(" (Set (Var "s"))  ($#k2_valued_1 :::"+"::: )  (Set (Var "s9")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_comseq_2 :::"lim"::: )  (Set (Var "s")) ")" )  ($#k8_complex1 :::"+"::: )  (Set  "("  ($#k3_comseq_2 :::"lim"::: )  (Set (Var "s9")) ")" )))) ; 
 
theorem :: COMSEQ_2:15 canceled; 
 
theorem :: COMSEQ_2:16 (Bool  "for" (Set (Var "s")) "," (Set (Var "s9")) "being"   ($#v2_comseq_2 :::"convergent"::: )    ($#m1_subset_1 :::"Complex_Sequence":::) "holds"  (Bool (Set   ($#k3_comseq_2 :::"lim"::: )  (Set  "(" (Set  "(" (Set (Var "s"))  ($#k2_valued_1 :::"+"::: )  (Set (Var "s9")) ")" )  ($#k2_comseq_2 :::"*'"::: )  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k3_comseq_2 :::"lim"::: )  (Set (Var "s")) ")" )  ($#k15_complex1 :::"*'"::: )  ")" )  ($#k8_complex1 :::"+"::: )  (Set  "(" (Set  "("  ($#k3_comseq_2 :::"lim"::: )  (Set (Var "s9")) ")" )  ($#k15_complex1 :::"*'"::: )  ")" )))) ; 
 registrationlet "s" be   ($#v2_comseq_2 :::"convergent"::: )    ($#m1_subset_1 :::"Complex_Sequence":::); let "c" be   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set "c"  ($#k24_valued_1 :::"(#)"::: )  "s") ->   ($#v2_comseq_2 :::"convergent"::: )    for  ($#m1_subset_1 :::"Complex_Sequence":::); 
end; 
theorem :: COMSEQ_2:17 canceled; 
 
theorem :: COMSEQ_2:18 (Bool  "for" (Set (Var "s")) "being"   ($#v2_comseq_2 :::"convergent"::: )    ($#m1_subset_1 :::"Complex_Sequence":::)  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k3_comseq_2 :::"lim"::: )  (Set  "(" (Set (Var "r"))  ($#k25_valued_1 :::"(#)"::: )  (Set (Var "s")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "r"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k3_comseq_2 :::"lim"::: )  (Set (Var "s")) ")" ))))) ; 
 
theorem :: COMSEQ_2:19 canceled; 
 
theorem :: COMSEQ_2:20 (Bool  "for" (Set (Var "r")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_numbers :::"COMPLEX"::: )  )  (Bool  "for" (Set (Var "s")) "being"   ($#v2_comseq_2 :::"convergent"::: )    ($#m1_subset_1 :::"Complex_Sequence":::) "holds"  (Bool (Set   ($#k3_comseq_2 :::"lim"::: )  (Set  "(" (Set  "(" (Set (Var "r"))  ($#k25_valued_1 :::"(#)"::: )  (Set (Var "s")) ")" )  ($#k2_comseq_2 :::"*'"::: )  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "r"))  ($#k15_complex1 :::"*'"::: )  ")" )  ($#k9_complex1 :::"*"::: )  (Set  "(" (Set  "("  ($#k3_comseq_2 :::"lim"::: )  (Set (Var "s")) ")" )  ($#k15_complex1 :::"*'"::: )  ")" ))))) ; 
 registrationlet "s" be   ($#v2_comseq_2 :::"convergent"::: )    ($#m1_subset_1 :::"Complex_Sequence":::); 
cluster (Set   ($#k30_valued_1 :::"-"::: )  "s") ->   ($#v2_comseq_2 :::"convergent"::: )    for  ($#m1_subset_1 :::"Complex_Sequence":::); 
end; 
theorem :: COMSEQ_2:21 canceled; 
 
theorem :: COMSEQ_2:22 (Bool  "for" (Set (Var "s")) "being"   ($#v2_comseq_2 :::"convergent"::: )    ($#m1_subset_1 :::"Complex_Sequence":::) "holds"  (Bool (Set   ($#k3_comseq_2 :::"lim"::: )  (Set  "("  ($#k31_valued_1 :::"-"::: )  (Set (Var "s")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k10_complex1 :::"-"::: )  (Set  "("  ($#k3_comseq_2 :::"lim"::: )  (Set (Var "s")) ")" )))) ; 
 
theorem :: COMSEQ_2:23 canceled; 
 
theorem :: COMSEQ_2:24 (Bool  "for" (Set (Var "s")) "being"   ($#v2_comseq_2 :::"convergent"::: )    ($#m1_subset_1 :::"Complex_Sequence":::) "holds"  (Bool (Set   ($#k3_comseq_2 :::"lim"::: )  (Set  "(" (Set  "("  ($#k31_valued_1 :::"-"::: )  (Set (Var "s")) ")" )  ($#k2_comseq_2 :::"*'"::: )  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k10_complex1 :::"-"::: )  (Set  "(" (Set  "("  ($#k3_comseq_2 :::"lim"::: )  (Set (Var "s")) ")" )  ($#k15_complex1 :::"*'"::: )  ")" )))) ; 
 registrationlet "s1", "s2" be   ($#v2_comseq_2 :::"convergent"::: )    ($#m1_subset_1 :::"Complex_Sequence":::); 
cluster (Set "s1"  ($#k45_valued_1 :::"-"::: )  "s2") ->   ($#v2_comseq_2 :::"convergent"::: )    for  ($#m1_subset_1 :::"Complex_Sequence":::); 
end; 
theorem :: COMSEQ_2:25 canceled; 
 
theorem :: COMSEQ_2:26 (Bool  "for" (Set (Var "s")) "," (Set (Var "s9")) "being"   ($#v2_comseq_2 :::"convergent"::: )    ($#m1_subset_1 :::"Complex_Sequence":::) "holds"  (Bool (Set   ($#k3_comseq_2 :::"lim"::: )  (Set  "(" (Set (Var "s"))  ($#k46_valued_1 :::"-"::: )  (Set (Var "s9")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_comseq_2 :::"lim"::: )  (Set (Var "s")) ")" )  ($#k11_complex1 :::"-"::: )  (Set  "("  ($#k3_comseq_2 :::"lim"::: )  (Set (Var "s9")) ")" )))) ; 
 
theorem :: COMSEQ_2:27 canceled; 
 
theorem :: COMSEQ_2:28 (Bool  "for" (Set (Var "s")) "," (Set (Var "s9")) "being"   ($#v2_comseq_2 :::"convergent"::: )    ($#m1_subset_1 :::"Complex_Sequence":::) "holds"  (Bool (Set   ($#k3_comseq_2 :::"lim"::: )  (Set  "(" (Set  "(" (Set (Var "s"))  ($#k46_valued_1 :::"-"::: )  (Set (Var "s9")) ")" )  ($#k2_comseq_2 :::"*'"::: )  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k3_comseq_2 :::"lim"::: )  (Set (Var "s")) ")" )  ($#k15_complex1 :::"*'"::: )  ")" )  ($#k11_complex1 :::"-"::: )  (Set  "(" (Set  "("  ($#k3_comseq_2 :::"lim"::: )  (Set (Var "s9")) ")" )  ($#k15_complex1 :::"*'"::: )  ")" )))) ; 
 registration
cluster   ($#v1_funct_1 :::"Function-like"::: )   bbbadV1_FUNCT_2((Set   ($#k5_numbers :::"NAT"::: )  ) "," (Set   ($#k2_numbers :::"COMPLEX"::: )  ))   ($#v2_comseq_2 :::"convergent"::: )    ->   ($#v1_comseq_2 :::"bounded"::: )    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_funct_1 :::"Function-like"::: )   bbbadV1_FUNCT_2((Set   ($#k5_numbers :::"NAT"::: )  ) "," (Set   ($#k2_numbers :::"COMPLEX"::: )  ))  ($#~v1_comseq_2  "non"   ($#v1_comseq_2 :::"bounded"::: )   )   ->  ($#~v2_comseq_2  "non"   ($#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; registrationlet "s1", "s2" be   ($#v2_comseq_2 :::"convergent"::: )    ($#m1_subset_1 :::"Complex_Sequence":::); 
cluster (Set "s1"  ($#k18_valued_1 :::"(#)"::: )  "s2") ->   ($#v2_comseq_2 :::"convergent"::: )    for  ($#m1_subset_1 :::"Complex_Sequence":::); 
end; 
theorem :: COMSEQ_2:29 canceled; 
 
theorem :: COMSEQ_2:30 (Bool  "for" (Set (Var "s")) "," (Set (Var "s9")) "being"   ($#v2_comseq_2 :::"convergent"::: )    ($#m1_subset_1 :::"Complex_Sequence":::) "holds"  (Bool (Set   ($#k3_comseq_2 :::"lim"::: )  (Set  "(" (Set (Var "s"))  ($#k19_valued_1 :::"(#)"::: )  (Set (Var "s9")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_comseq_2 :::"lim"::: )  (Set (Var "s")) ")" )  ($#k9_complex1 :::"*"::: )  (Set  "("  ($#k3_comseq_2 :::"lim"::: )  (Set (Var "s9")) ")" )))) ; 
 
theorem :: COMSEQ_2:31 canceled; 
 
theorem :: COMSEQ_2:32 (Bool  "for" (Set (Var "s")) "," (Set (Var "s9")) "being"   ($#v2_comseq_2 :::"convergent"::: )    ($#m1_subset_1 :::"Complex_Sequence":::) "holds"  (Bool (Set   ($#k3_comseq_2 :::"lim"::: )  (Set  "(" (Set  "(" (Set (Var "s"))  ($#k19_valued_1 :::"(#)"::: )  (Set (Var "s9")) ")" )  ($#k2_comseq_2 :::"*'"::: )  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k3_comseq_2 :::"lim"::: )  (Set (Var "s")) ")" )  ($#k15_complex1 :::"*'"::: )  ")" )  ($#k9_complex1 :::"*"::: )  (Set  "(" (Set  "("  ($#k3_comseq_2 :::"lim"::: )  (Set (Var "s9")) ")" )  ($#k15_complex1 :::"*'"::: )  ")" )))) ; 
 
theorem :: COMSEQ_2:33 (Bool  "for" (Set (Var "s")) "being"   ($#v2_comseq_2 :::"convergent"::: )    ($#m1_subset_1 :::"Complex_Sequence":::)  "st" (Bool (Bool (Set   ($#k3_comseq_2 :::"lim"::: )  (Set (Var "s")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k5_complex1 :::"0c"::: )  ))) "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 (Set  ($#k17_complex1 :::"|."::: ) (Set  "("  ($#k3_comseq_2 :::"lim"::: )  (Set (Var "s")) ")" ) ($#k17_complex1 :::".|"::: ) )  ($#k10_real_1 :::"/"::: )  (Num 2))  ($#r1_xxreal_0 :::"<"::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set (Var "s"))  ($#k8_nat_1 :::"."::: )  (Set (Var "m")) ")" ) ($#k17_complex1 :::".|"::: ) ))))) ; 
 
theorem :: COMSEQ_2:34 (Bool  "for" (Set (Var "s")) "being"   ($#v2_comseq_2 :::"convergent"::: )    ($#m1_subset_1 :::"Complex_Sequence":::)  "st" (Bool (Bool (Set   ($#k3_comseq_2 :::"lim"::: )  (Set (Var "s")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k5_complex1 :::"0c"::: )  )) & (Bool (Set (Var "s")) "is"   ($#v2_relat_1 :::"non-zero"::: )  )) "holds"  (Bool (Set (Set (Var "s"))  ($#k36_valued_1 :::"""::: )  ) "is"   ($#v2_comseq_2 :::"convergent"::: )  )) ; 
 
theorem :: COMSEQ_2:35 (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::)  "st" (Bool (Bool (Set (Var "s")) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set   ($#k3_comseq_2 :::"lim"::: )  (Set (Var "s")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k5_complex1 :::"0c"::: )  )) & (Bool (Set (Var "s")) "is"   ($#v2_relat_1 :::"non-zero"::: )  )) "holds"  (Bool (Set   ($#k3_comseq_2 :::"lim"::: )  (Set  "(" (Set (Var "s"))  ($#k36_valued_1 :::"""::: )  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_comseq_2 :::"lim"::: )  (Set (Var "s")) ")" )  ($#k12_complex1 :::"""::: )  ))) ; 
 
theorem :: COMSEQ_2:36 canceled; 
 
theorem :: COMSEQ_2:37 (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::)  "st" (Bool (Bool (Set (Var "s")) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set   ($#k3_comseq_2 :::"lim"::: )  (Set (Var "s")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k5_complex1 :::"0c"::: )  )) & (Bool (Set (Var "s")) "is"   ($#v2_relat_1 :::"non-zero"::: )  )) "holds"  (Bool (Set   ($#k3_comseq_2 :::"lim"::: )  (Set  "(" (Set  "(" (Set (Var "s"))  ($#k36_valued_1 :::"""::: )  ")" )  ($#k2_comseq_2 :::"*'"::: )  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k3_comseq_2 :::"lim"::: )  (Set (Var "s")) ")" )  ($#k15_complex1 :::"*'"::: )  ")" )  ($#k12_complex1 :::"""::: )  ))) ; 
 
theorem :: COMSEQ_2:38 (Bool  "for" (Set (Var "s9")) "," (Set (Var "s")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::)  "st" (Bool (Bool (Set (Var "s9")) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set (Var "s")) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set   ($#k3_comseq_2 :::"lim"::: )  (Set (Var "s")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k5_complex1 :::"0c"::: )  )) & (Bool (Set (Var "s")) "is"   ($#v2_relat_1 :::"non-zero"::: )  )) "holds"  (Bool (Set (Set (Var "s9"))  ($#k51_valued_1 :::"/""::: )  (Set (Var "s"))) "is"   ($#v2_comseq_2 :::"convergent"::: )  )) ; 
 
theorem :: COMSEQ_2:39 (Bool  "for" (Set (Var "s9")) "," (Set (Var "s")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::)  "st" (Bool (Bool (Set (Var "s9")) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set (Var "s")) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set   ($#k3_comseq_2 :::"lim"::: )  (Set (Var "s")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k5_complex1 :::"0c"::: )  )) & (Bool (Set (Var "s")) "is"   ($#v2_relat_1 :::"non-zero"::: )  )) "holds"  (Bool (Set   ($#k3_comseq_2 :::"lim"::: )  (Set  "(" (Set (Var "s9"))  ($#k51_valued_1 :::"/""::: )  (Set (Var "s")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_comseq_2 :::"lim"::: )  (Set (Var "s9")) ")" )  ($#k13_complex1 :::"/"::: )  (Set  "("  ($#k3_comseq_2 :::"lim"::: )  (Set (Var "s")) ")" )))) ; 
 
theorem :: COMSEQ_2:40 canceled; 
 
theorem :: COMSEQ_2:41 (Bool  "for" (Set (Var "s9")) "," (Set (Var "s")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::)  "st" (Bool (Bool (Set (Var "s9")) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set (Var "s")) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set   ($#k3_comseq_2 :::"lim"::: )  (Set (Var "s")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k5_complex1 :::"0c"::: )  )) & (Bool (Set (Var "s")) "is"   ($#v2_relat_1 :::"non-zero"::: )  )) "holds"  (Bool (Set   ($#k3_comseq_2 :::"lim"::: )  (Set  "(" (Set  "(" (Set (Var "s9"))  ($#k51_valued_1 :::"/""::: )  (Set (Var "s")) ")" )  ($#k2_comseq_2 :::"*'"::: )  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k3_comseq_2 :::"lim"::: )  (Set (Var "s9")) ")" )  ($#k15_complex1 :::"*'"::: )  ")" )  ($#k13_complex1 :::"/"::: )  (Set  "(" (Set  "("  ($#k3_comseq_2 :::"lim"::: )  (Set (Var "s")) ")" )  ($#k15_complex1 :::"*'"::: )  ")" )))) ; 
 
theorem :: COMSEQ_2:42 (Bool  "for" (Set (Var "s")) "," (Set (Var "s1")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::)  "st" (Bool (Bool (Set (Var "s")) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set (Var "s1")) "is"   ($#v1_comseq_2 :::"bounded"::: )  ) & (Bool (Set   ($#k3_comseq_2 :::"lim"::: )  (Set (Var "s")))  ($#r1_hidden :::"="::: )  (Set   ($#k5_complex1 :::"0c"::: )  ))) "holds"  (Bool (Set (Set (Var "s"))  ($#k19_valued_1 :::"(#)"::: )  (Set (Var "s1"))) "is"   ($#v2_comseq_2 :::"convergent"::: )  )) ; 
 
theorem :: COMSEQ_2:43 (Bool  "for" (Set (Var "s")) "," (Set (Var "s1")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::)  "st" (Bool (Bool (Set (Var "s")) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set (Var "s1")) "is"   ($#v1_comseq_2 :::"bounded"::: )  ) & (Bool (Set   ($#k3_comseq_2 :::"lim"::: )  (Set (Var "s")))  ($#r1_hidden :::"="::: )  (Set   ($#k5_complex1 :::"0c"::: )  ))) "holds"  (Bool (Set   ($#k3_comseq_2 :::"lim"::: )  (Set  "(" (Set (Var "s"))  ($#k19_valued_1 :::"(#)"::: )  (Set (Var "s1")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k5_complex1 :::"0c"::: )  ))) ; 
 
theorem :: COMSEQ_2:44 canceled; 
 
theorem :: COMSEQ_2:45 (Bool  "for" (Set (Var "s")) "," (Set (Var "s1")) "being"   ($#m1_subset_1 :::"Complex_Sequence":::)  "st" (Bool (Bool (Set (Var "s")) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set (Var "s1")) "is"   ($#v1_comseq_2 :::"bounded"::: )  ) & (Bool (Set   ($#k3_comseq_2 :::"lim"::: )  (Set (Var "s")))  ($#r1_hidden :::"="::: )  (Set   ($#k5_complex1 :::"0c"::: )  ))) "holds"  (Bool (Set   ($#k3_comseq_2 :::"lim"::: )  (Set  "(" (Set  "(" (Set (Var "s"))  ($#k19_valued_1 :::"(#)"::: )  (Set (Var "s1")) ")" )  ($#k2_comseq_2 :::"*'"::: )  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k5_complex1 :::"0c"::: )  ))) ;