:: SEQ_2  semantic presentation begin  























theorem :: SEQ_2:1 (Bool  "for" (Set (Var "g")) "," (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("  (Bool  "("  (Bool (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "g")))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r"))) & (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "g")))  ")" ) "iff" (Bool (Set   ($#k18_complex1 :::"abs"::: )  (Set (Var "r")))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "g")))  ")" )) ; 
 
theorem :: SEQ_2:2 (Bool  "for" (Set (Var "g")) "," (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "g"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "r"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set   ($#k18_complex1 :::"abs"::: )  (Set  "(" (Set  "(" (Set (Var "g"))  ($#k5_xcmplx_0 :::"""::: )  ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "r"))  ($#k5_xcmplx_0 :::"""::: )  ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k18_complex1 :::"abs"::: )  (Set  "(" (Set (Var "g"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "r")) ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set  "("  ($#k18_complex1 :::"abs"::: )  (Set (Var "g")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k18_complex1 :::"abs"::: )  (Set (Var "r")) ")" ) ")" )))) ; 
 definitionlet "f" be   ($#v3_valued_0 :::"real-valued"::: )    ($#m1_hidden :::"Function":::); attr "f" is  :::"bounded_above":::  means :: SEQ_2:def 1 (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 "f"  ($#k1_seq_1 :::"."::: )  (Set (Var "y")))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r"))))); attr "f" is  :::"bounded_below":::  means :: SEQ_2:def 2 (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 (Var "r"))  ($#r1_xxreal_0 :::"<"::: )  (Set "f"  ($#k1_seq_1 :::"."::: )  (Set (Var "y")))))); end; 








:: deftheorem    defines :::"bounded_above"::: SEQ_2:def 1 :  (Bool  "for" (Set (Var "f")) "being"   ($#v3_valued_0 :::"real-valued"::: )    ($#m1_hidden :::"Function":::) "holds"   (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v1_seq_2 :::"bounded_above"::: )  ) "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 (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "y")))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r")))))  ")" )); 
 
:: deftheorem    defines :::"bounded_below"::: SEQ_2:def 2 :  (Bool  "for" (Set (Var "f")) "being"   ($#v3_valued_0 :::"real-valued"::: )    ($#m1_hidden :::"Function":::) "holds"   (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v2_seq_2 :::"bounded_below"::: )  ) "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 (Var "r"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "y"))))))  ")" )); 
 definitionlet "seq" be   ($#m1_subset_1 :::"Real_Sequence":::); redefine attr "seq" is  :::"bounded_above":::  means :: SEQ_2:def 3 (Bool  "ex" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "holds" (Bool (Set "seq"  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r"))))); redefine attr "seq" is  :::"bounded_below":::  means :: SEQ_2:def 4 (Bool  "ex" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "holds" (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<"::: )  (Set "seq"  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))))); end; 








:: deftheorem    defines :::"bounded_above"::: SEQ_2:def 3 :  (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "holds"   (Bool  "("  (Bool (Set (Var "seq")) "is"   ($#v1_seq_2 :::"bounded_above"::: )  ) "iff" (Bool  "ex" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "holds" (Bool (Set (Set (Var "seq"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r")))))  ")" )); 
 
:: deftheorem    defines :::"bounded_below"::: SEQ_2:def 4 :  (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "holds"   (Bool  "("  (Bool (Set (Var "seq")) "is"   ($#v2_seq_2 :::"bounded_below"::: )  ) "iff" (Bool  "ex" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "holds" (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "seq"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n"))))))  ")" )); 
 registration
cluster   ($#v1_relat_1 :::"Relation-like"::: )     ($#v1_funct_1 :::"Function-like"::: )     ($#v3_valued_0 :::"real-valued"::: )     ($#v1_comseq_2 :::"bounded"::: )    ->   ($#v3_valued_0 :::"real-valued"::: )     ($#v1_seq_2 :::"bounded_above"::: )     ($#v2_seq_2 :::"bounded_below"::: )    for    ($#m1_hidden :::"set"::: )  ; 

cluster   ($#v1_relat_1 :::"Relation-like"::: )     ($#v1_funct_1 :::"Function-like"::: )     ($#v3_valued_0 :::"real-valued"::: )     ($#v1_seq_2 :::"bounded_above"::: )     ($#v2_seq_2 :::"bounded_below"::: )    ->   ($#v3_valued_0 :::"real-valued"::: )     ($#v1_comseq_2 :::"bounded"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; 
theorem :: SEQ_2:3 (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "holds"   (Bool  "("  (Bool (Set (Var "seq")) "is"   ($#v1_comseq_2 :::"bounded"::: )  ) "iff" (Bool  "ex" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "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   ($#k18_complex1 :::"abs"::: )  (Set  "(" (Set (Var "seq"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" ))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r")))  ")" )  ")" ))  ")" )) ; 
 
theorem :: SEQ_2:4 (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) (Bool  "ex" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "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   ($#k18_complex1 :::"abs"::: )  (Set  "(" (Set (Var "seq"))  ($#k1_seq_1 :::"."::: )  (Set (Var "m")) ")" ))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r")))  ")" )  ")" )))) ; 
 definitioncanceled; let "seq" be   ($#m1_subset_1 :::"Real_Sequence":::); redefine attr "seq" is  :::"convergent":::  means :: SEQ_2:def 6 (Bool  "ex" (Set (Var "g")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "for" (Set (Var "p")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "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   ($#k18_complex1 :::"abs"::: )  (Set  "(" (Set  "(" "seq"  ($#k1_seq_1 :::"."::: )  (Set (Var "m")) ")" )  ($#k9_real_1 :::"-"::: )  (Set (Var "g")) ")" ))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "p"))))))); end; 




:: deftheorem   SEQ_2:def 5 :  canceled;  
 
:: deftheorem    defines :::"convergent"::: SEQ_2:def 6 :  (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "holds"   (Bool  "("  (Bool (Set (Var "seq")) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) "iff" (Bool  "ex" (Set (Var "g")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "for" (Set (Var "p")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "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   ($#k18_complex1 :::"abs"::: )  (Set  "(" (Set  "(" (Set (Var "seq"))  ($#k1_seq_1 :::"."::: )  (Set (Var "m")) ")" )  ($#k9_real_1 :::"-"::: )  (Set (Var "g")) ")" ))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "p")))))))  ")" )); 
 definitionlet "seq" be   ($#m1_subset_1 :::"Real_Sequence":::); assume 
(Bool (Set (Const "seq")) "is"   ($#v2_comseq_2 :::"convergent"::: )  )
 ; func  :::"lim"::: "seq" ->   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   means :: SEQ_2:def 7 (Bool  "for" (Set (Var "p")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "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   ($#k18_complex1 :::"abs"::: )  (Set  "(" (Set  "(" "seq"  ($#k1_seq_1 :::"."::: )  (Set (Var "m")) ")" )  ($#k9_real_1 :::"-"::: )  it ")" ))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "p")))))); end; 






:: deftheorem    defines :::"lim"::: SEQ_2:def 7 :  (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  "st" (Bool (Bool (Set (Var "seq")) "is"   ($#v2_comseq_2 :::"convergent"::: )  )) "holds"  (Bool  "for" (Set (Var "b2")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_seq_2 :::"lim"::: )  (Set (Var "seq")))) "iff" (Bool  "for" (Set (Var "p")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "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   ($#k18_complex1 :::"abs"::: )  (Set  "(" (Set  "(" (Set (Var "seq"))  ($#k1_seq_1 :::"."::: )  (Set (Var "m")) ")" )  ($#k9_real_1 :::"-"::: )  (Set (Var "b2")) ")" ))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "p"))))))  ")" ))); 
 definitionlet "f" be   ($#v3_valued_0 :::"real-valued"::: )    ($#m1_hidden :::"Function":::); redefine attr "f" is  :::"bounded":::  means :: SEQ_2:def 8 (Bool  "("  (Bool "f" "is"   ($#v1_seq_2 :::"bounded_above"::: )  ) & (Bool "f" "is"   ($#v2_seq_2 :::"bounded_below"::: )  )  ")" ); end; 




:: deftheorem    defines :::"bounded"::: SEQ_2:def 8 :  (Bool  "for" (Set (Var "f")) "being"   ($#v3_valued_0 :::"real-valued"::: )    ($#m1_hidden :::"Function":::) "holds"   (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v1_comseq_2 :::"bounded"::: )  ) "iff" (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v1_seq_2 :::"bounded_above"::: )  ) & (Bool (Set (Var "f")) "is"   ($#v2_seq_2 :::"bounded_below"::: )  )  ")" )  ")" )); 
 definitionlet "seq" be   ($#m1_subset_1 :::"Real_Sequence":::); :: original: :::"lim"::: redefine func  :::"lim"::: "seq" ->   ($#m1_subset_1 :::"Real":::); end; registration
cluster   ($#v1_funct_1 :::"Function-like"::: )     ($#v3_funct_1 :::"constant"::: )   bbbadV1_FUNCT_2((Set   ($#k5_numbers :::"NAT"::: )  ) "," (Set   ($#k1_numbers :::"REAL"::: )  ))  ->   ($#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_xboole_0  "non"   ($#v1_xboole_0 :::"zero"::: )   )    ($#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"::: )     ($#v3_funct_1 :::"constant"::: )   bbbadV1_PARTFUN1((Set   ($#k5_numbers :::"NAT"::: )  )) 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"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1((Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) ))))); 
end; 
theorem :: SEQ_2:5 (Bool  "for" (Set (Var "seq")) "," (Set (Var "seq9")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  "st" (Bool (Bool (Set (Var "seq")) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set (Var "seq9")) "is"   ($#v2_comseq_2 :::"convergent"::: )  )) "holds"  (Bool (Set (Set (Var "seq"))  ($#k3_valued_1 :::"+"::: )  (Set (Var "seq9"))) "is"   ($#v2_comseq_2 :::"convergent"::: )  )) ; 
 registrationlet "seq1", "seq2" be   ($#v2_comseq_2 :::"convergent"::: )    ($#m1_subset_1 :::"Real_Sequence":::); 
cluster (Set "seq1"  ($#k1_valued_1 :::"+"::: )  "seq2") ->   ($#v2_comseq_2 :::"convergent"::: )    for  ($#m1_subset_1 :::"Real_Sequence":::); 
end; 
theorem :: SEQ_2:6 (Bool  "for" (Set (Var "seq")) "," (Set (Var "seq9")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  "st" (Bool (Bool (Set (Var "seq")) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set (Var "seq9")) "is"   ($#v2_comseq_2 :::"convergent"::: )  )) "holds"  (Bool (Set   ($#k2_seq_2 :::"lim"::: )  (Set  "(" (Set (Var "seq"))  ($#k3_valued_1 :::"+"::: )  (Set (Var "seq9")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_seq_2 :::"lim"::: )  (Set (Var "seq")) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "("  ($#k2_seq_2 :::"lim"::: )  (Set (Var "seq9")) ")" )))) ; 
 
theorem :: SEQ_2:7 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  "st" (Bool (Bool (Set (Var "seq")) "is"   ($#v2_comseq_2 :::"convergent"::: )  )) "holds"  (Bool (Set (Set (Var "r"))  ($#k26_valued_1 :::"(#)"::: )  (Set (Var "seq"))) "is"   ($#v2_comseq_2 :::"convergent"::: )  ))) ; 
 registrationlet "r" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; let "seq" be   ($#v2_comseq_2 :::"convergent"::: )    ($#m1_subset_1 :::"Real_Sequence":::); 
cluster (Set "r"  ($#k24_valued_1 :::"(#)"::: )  "seq") ->   ($#v2_comseq_2 :::"convergent"::: )    for  ($#m1_subset_1 :::"Real_Sequence":::); 
end; 
theorem :: SEQ_2:8 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  "st" (Bool (Bool (Set (Var "seq")) "is"   ($#v2_comseq_2 :::"convergent"::: )  )) "holds"  (Bool (Set   ($#k2_seq_2 :::"lim"::: )  (Set  "(" (Set (Var "r"))  ($#k26_valued_1 :::"(#)"::: )  (Set (Var "seq")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "r"))  ($#k4_real_1 :::"*"::: )  (Set  "("  ($#k2_seq_2 :::"lim"::: )  (Set (Var "seq")) ")" ))))) ; 
 
theorem :: SEQ_2:9 (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  "st" (Bool (Bool (Set (Var "seq")) "is"   ($#v2_comseq_2 :::"convergent"::: )  )) "holds"  (Bool (Set   ($#k32_valued_1 :::"-"::: )  (Set (Var "seq"))) "is"   ($#v2_comseq_2 :::"convergent"::: )  )) ; 
 registrationlet "seq" be   ($#v2_comseq_2 :::"convergent"::: )    ($#m1_subset_1 :::"Real_Sequence":::); 
cluster (Set   ($#k30_valued_1 :::"-"::: )  "seq") ->   ($#v2_comseq_2 :::"convergent"::: )    for  ($#m1_subset_1 :::"Real_Sequence":::); 
end; 
theorem :: SEQ_2:10 (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  "st" (Bool (Bool (Set (Var "seq")) "is"   ($#v2_comseq_2 :::"convergent"::: )  )) "holds"  (Bool (Set   ($#k2_seq_2 :::"lim"::: )  (Set  "("  ($#k32_valued_1 :::"-"::: )  (Set (Var "seq")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Set  "("  ($#k2_seq_2 :::"lim"::: )  (Set (Var "seq")) ")" )))) ; 
 
theorem :: SEQ_2:11 (Bool  "for" (Set (Var "seq")) "," (Set (Var "seq9")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  "st" (Bool (Bool (Set (Var "seq")) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set (Var "seq9")) "is"   ($#v2_comseq_2 :::"convergent"::: )  )) "holds"  (Bool (Set (Set (Var "seq"))  ($#k47_valued_1 :::"-"::: )  (Set (Var "seq9"))) "is"   ($#v2_comseq_2 :::"convergent"::: )  )) ; 
 registrationlet "seq1", "seq2" be   ($#v2_comseq_2 :::"convergent"::: )    ($#m1_subset_1 :::"Real_Sequence":::); 
cluster (Set "seq1"  ($#k45_valued_1 :::"-"::: )  "seq2") ->   ($#v2_comseq_2 :::"convergent"::: )    for  ($#m1_subset_1 :::"Real_Sequence":::); 
end; 
theorem :: SEQ_2:12 (Bool  "for" (Set (Var "seq")) "," (Set (Var "seq9")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  "st" (Bool (Bool (Set (Var "seq")) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set (Var "seq9")) "is"   ($#v2_comseq_2 :::"convergent"::: )  )) "holds"  (Bool (Set   ($#k2_seq_2 :::"lim"::: )  (Set  "(" (Set (Var "seq"))  ($#k47_valued_1 :::"-"::: )  (Set (Var "seq9")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_seq_2 :::"lim"::: )  (Set (Var "seq")) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "("  ($#k2_seq_2 :::"lim"::: )  (Set (Var "seq9")) ")" )))) ; 
 
theorem :: SEQ_2:13 (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  "st" (Bool (Bool (Set (Var "seq")) "is"   ($#v2_comseq_2 :::"convergent"::: )  )) "holds"  (Bool (Set (Var "seq")) "is"   ($#v1_comseq_2 :::"bounded"::: )  )) ; 
 registration
cluster   ($#v1_funct_1 :::"Function-like"::: )   bbbadV1_FUNCT_2((Set   ($#k5_numbers :::"NAT"::: )  ) "," (Set   ($#k1_numbers :::"REAL"::: )  ))   ($#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  ($#k1_numbers :::"REAL"::: ) ))))); 
end; 
theorem :: SEQ_2:14 (Bool  "for" (Set (Var "seq")) "," (Set (Var "seq9")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  "st" (Bool (Bool (Set (Var "seq")) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set (Var "seq9")) "is"   ($#v2_comseq_2 :::"convergent"::: )  )) "holds"  (Bool (Set (Set (Var "seq"))  ($#k20_valued_1 :::"(#)"::: )  (Set (Var "seq9"))) "is"   ($#v2_comseq_2 :::"convergent"::: )  )) ; 
 registrationlet "seq1", "seq2" be   ($#v2_comseq_2 :::"convergent"::: )    ($#m1_subset_1 :::"Real_Sequence":::); 
cluster (Set "seq1"  ($#k18_valued_1 :::"(#)"::: )  "seq2") ->   ($#v2_comseq_2 :::"convergent"::: )    for  ($#m1_subset_1 :::"Real_Sequence":::); 
end; 
theorem :: SEQ_2:15 (Bool  "for" (Set (Var "seq")) "," (Set (Var "seq9")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  "st" (Bool (Bool (Set (Var "seq")) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set (Var "seq9")) "is"   ($#v2_comseq_2 :::"convergent"::: )  )) "holds"  (Bool (Set   ($#k2_seq_2 :::"lim"::: )  (Set  "(" (Set (Var "seq"))  ($#k20_valued_1 :::"(#)"::: )  (Set (Var "seq9")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_seq_2 :::"lim"::: )  (Set (Var "seq")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k2_seq_2 :::"lim"::: )  (Set (Var "seq9")) ")" )))) ; 
 
theorem :: SEQ_2:16 (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  "st" (Bool (Bool (Set (Var "seq")) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set   ($#k2_seq_2 :::"lim"::: )  (Set (Var "seq")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "ex" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "for" (Set (Var "m")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "m")))) "holds"  (Bool (Set (Set  "("  ($#k18_complex1 :::"abs"::: )  (Set  "("  ($#k2_seq_2 :::"lim"::: )  (Set (Var "seq")) ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Num 2))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k18_complex1 :::"abs"::: )  (Set  "(" (Set (Var "seq"))  ($#k1_seq_1 :::"."::: )  (Set (Var "m")) ")" )))))) ; 
 
theorem :: SEQ_2:17 (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  "st" (Bool (Bool (Set (Var "seq")) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (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 "seq"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n"))))  ")" )) "holds"  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k2_seq_2 :::"lim"::: )  (Set (Var "seq"))))) ; 
 
theorem :: SEQ_2:18 (Bool  "for" (Set (Var "seq")) "," (Set (Var "seq9")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  "st" (Bool (Bool (Set (Var "seq")) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set (Var "seq9")) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool  "("   "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "seq"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "seq9"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n"))))  ")" )) "holds"  (Bool (Set   ($#k2_seq_2 :::"lim"::: )  (Set (Var "seq")))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k2_seq_2 :::"lim"::: )  (Set (Var "seq9"))))) ; 
 
theorem :: SEQ_2:19 (Bool  "for" (Set (Var "seq")) "," (Set (Var "seq9")) "," (Set (Var "seq1")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  "st" (Bool (Bool (Set (Var "seq")) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set (Var "seq9")) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool  "("   "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"   (Bool  "("  (Bool (Set (Set (Var "seq"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "seq1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))) & (Bool (Set (Set (Var "seq1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "seq9"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n"))))  ")" )  ")" ) & (Bool (Set   ($#k2_seq_2 :::"lim"::: )  (Set (Var "seq")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_seq_2 :::"lim"::: )  (Set (Var "seq9"))))) "holds"  (Bool (Set (Var "seq1")) "is"   ($#v2_comseq_2 :::"convergent"::: )  )) ; 
 
theorem :: SEQ_2:20 (Bool  "for" (Set (Var "seq")) "," (Set (Var "seq9")) "," (Set (Var "seq1")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  "st" (Bool (Bool (Set (Var "seq")) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set (Var "seq9")) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool  "("   "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"   (Bool  "("  (Bool (Set (Set (Var "seq"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "seq1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))) & (Bool (Set (Set (Var "seq1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "seq9"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n"))))  ")" )  ")" ) & (Bool (Set   ($#k2_seq_2 :::"lim"::: )  (Set (Var "seq")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_seq_2 :::"lim"::: )  (Set (Var "seq9"))))) "holds"  (Bool (Set   ($#k2_seq_2 :::"lim"::: )  (Set (Var "seq1")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_seq_2 :::"lim"::: )  (Set (Var "seq"))))) ; 
 
theorem :: SEQ_2:21 (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  "st" (Bool (Bool (Set (Var "seq")) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set   ($#k2_seq_2 :::"lim"::: )  (Set (Var "seq")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "seq")) "is"   ($#v2_relat_1 :::"non-zero"::: )  )) "holds"  (Bool (Set (Set (Var "seq"))  ($#k37_valued_1 :::"""::: )  ) "is"   ($#v2_comseq_2 :::"convergent"::: )  )) ; 
 
theorem :: SEQ_2:22 (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  "st" (Bool (Bool (Set (Var "seq")) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set   ($#k2_seq_2 :::"lim"::: )  (Set (Var "seq")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "seq")) "is"   ($#v2_relat_1 :::"non-zero"::: )  )) "holds"  (Bool (Set   ($#k2_seq_2 :::"lim"::: )  (Set  "(" (Set (Var "seq"))  ($#k37_valued_1 :::"""::: )  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_seq_2 :::"lim"::: )  (Set (Var "seq")) ")" )  ($#k2_real_1 :::"""::: )  ))) ; 
 
theorem :: SEQ_2:23 (Bool  "for" (Set (Var "seq9")) "," (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  "st" (Bool (Bool (Set (Var "seq9")) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set (Var "seq")) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set   ($#k2_seq_2 :::"lim"::: )  (Set (Var "seq")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "seq")) "is"   ($#v2_relat_1 :::"non-zero"::: )  )) "holds"  (Bool (Set (Set (Var "seq9"))  ($#k52_valued_1 :::"/""::: )  (Set (Var "seq"))) "is"   ($#v2_comseq_2 :::"convergent"::: )  )) ; 
 
theorem :: SEQ_2:24 (Bool  "for" (Set (Var "seq9")) "," (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  "st" (Bool (Bool (Set (Var "seq9")) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set (Var "seq")) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set   ($#k2_seq_2 :::"lim"::: )  (Set (Var "seq")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "seq")) "is"   ($#v2_relat_1 :::"non-zero"::: )  )) "holds"  (Bool (Set   ($#k2_seq_2 :::"lim"::: )  (Set  "(" (Set (Var "seq9"))  ($#k52_valued_1 :::"/""::: )  (Set (Var "seq")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_seq_2 :::"lim"::: )  (Set (Var "seq9")) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "("  ($#k2_seq_2 :::"lim"::: )  (Set (Var "seq")) ")" )))) ; 
 
theorem :: SEQ_2:25 (Bool  "for" (Set (Var "seq")) "," (Set (Var "seq1")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  "st" (Bool (Bool (Set (Var "seq")) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set (Var "seq1")) "is"   ($#v1_comseq_2 :::"bounded"::: )  ) & (Bool (Set   ($#k2_seq_2 :::"lim"::: )  (Set (Var "seq")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "seq"))  ($#k20_valued_1 :::"(#)"::: )  (Set (Var "seq1"))) "is"   ($#v2_comseq_2 :::"convergent"::: )  )) ; 
 
theorem :: SEQ_2:26 (Bool  "for" (Set (Var "seq")) "," (Set (Var "seq1")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  "st" (Bool (Bool (Set (Var "seq")) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set (Var "seq1")) "is"   ($#v1_comseq_2 :::"bounded"::: )  ) & (Bool (Set   ($#k2_seq_2 :::"lim"::: )  (Set (Var "seq")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set   ($#k2_seq_2 :::"lim"::: )  (Set  "(" (Set (Var "seq"))  ($#k20_valued_1 :::"(#)"::: )  (Set (Var "seq1")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 


registrationlet "s" be   ($#v2_comseq_2 :::"convergent"::: )    ($#m1_subset_1 :::"Complex_Sequence":::); 
cluster (Set  ($#k54_valued_1 :::"|."::: ) "s" ($#k54_valued_1 :::".|"::: ) ) ->   ($#v2_comseq_2 :::"convergent"::: )    for  ($#m1_subset_1 :::"Real_Sequence":::); 
end; 





theorem :: SEQ_2:27 (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   ($#k2_seq_2 :::"lim"::: )  (Set  ($#k55_valued_1 :::"|."::: ) (Set (Var "s")) ($#k55_valued_1 :::".|"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set  "("  ($#k3_comseq_2 :::"lim"::: )  (Set (Var "s")) ")" ) ($#k17_complex1 :::".|"::: ) ))) ; 
 
theorem :: SEQ_2:28 (Bool  "for" (Set (Var "s")) "," (Set (Var "s9")) "being"   ($#v2_comseq_2 :::"convergent"::: )    ($#m1_subset_1 :::"Complex_Sequence":::) "holds"  (Bool (Set   ($#k2_seq_2 :::"lim"::: )  (Set  ($#k55_valued_1 :::"|."::: ) (Set  "(" (Set (Var "s"))  ($#k2_valued_1 :::"+"::: )  (Set (Var "s9")) ")" ) ($#k55_valued_1 :::".|"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set  "("  ($#k3_comseq_2 :::"lim"::: )  (Set (Var "s")) ")" )  ($#k8_complex1 :::"+"::: )  (Set  "("  ($#k3_comseq_2 :::"lim"::: )  (Set (Var "s9")) ")" ) ")" ) ($#k17_complex1 :::".|"::: ) ))) ; 
 
theorem :: SEQ_2:29 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "s")) "being"   ($#v2_comseq_2 :::"convergent"::: )    ($#m1_subset_1 :::"Complex_Sequence":::) "holds"  (Bool (Set   ($#k2_seq_2 :::"lim"::: )  (Set  ($#k55_valued_1 :::"|."::: ) (Set  "(" (Set (Var "r"))  ($#k25_valued_1 :::"(#)"::: )  (Set (Var "s")) ")" ) ($#k55_valued_1 :::".|"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k17_complex1 :::"|."::: ) (Set (Var "r")) ($#k17_complex1 :::".|"::: ) )  ($#k8_real_1 :::"*"::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set  "("  ($#k3_comseq_2 :::"lim"::: )  (Set (Var "s")) ")" ) ($#k17_complex1 :::".|"::: ) ))))) ; 
 
theorem :: SEQ_2:30 (Bool  "for" (Set (Var "s")) "being"   ($#v2_comseq_2 :::"convergent"::: )    ($#m1_subset_1 :::"Complex_Sequence":::) "holds"  (Bool (Set   ($#k2_seq_2 :::"lim"::: )  (Set  ($#k55_valued_1 :::"|."::: ) (Set  "("  ($#k31_valued_1 :::"-"::: )  (Set (Var "s")) ")" ) ($#k55_valued_1 :::".|"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set  "("  ($#k3_comseq_2 :::"lim"::: )  (Set (Var "s")) ")" ) ($#k17_complex1 :::".|"::: ) ))) ; 
 
theorem :: SEQ_2:31 (Bool  "for" (Set (Var "s")) "," (Set (Var "s9")) "being"   ($#v2_comseq_2 :::"convergent"::: )    ($#m1_subset_1 :::"Complex_Sequence":::) "holds"  (Bool (Set   ($#k2_seq_2 :::"lim"::: )  (Set  ($#k55_valued_1 :::"|."::: ) (Set  "(" (Set (Var "s"))  ($#k46_valued_1 :::"-"::: )  (Set (Var "s9")) ")" ) ($#k55_valued_1 :::".|"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set  "(" (Set  "("  ($#k3_comseq_2 :::"lim"::: )  (Set (Var "s")) ")" )  ($#k11_complex1 :::"-"::: )  (Set  "("  ($#k3_comseq_2 :::"lim"::: )  (Set (Var "s9")) ")" ) ")" ) ($#k17_complex1 :::".|"::: ) ))) ; 
 
theorem :: SEQ_2:32 (Bool  "for" (Set (Var "s")) "," (Set (Var "s9")) "being"   ($#v2_comseq_2 :::"convergent"::: )    ($#m1_subset_1 :::"Complex_Sequence":::) "holds"  (Bool (Set   ($#k2_seq_2 :::"lim"::: )  (Set  ($#k55_valued_1 :::"|."::: ) (Set  "(" (Set (Var "s"))  ($#k19_valued_1 :::"(#)"::: )  (Set (Var "s9")) ")" ) ($#k55_valued_1 :::".|"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k17_complex1 :::"|."::: ) (Set  "("  ($#k3_comseq_2 :::"lim"::: )  (Set (Var "s")) ")" ) ($#k17_complex1 :::".|"::: ) )  ($#k8_real_1 :::"*"::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set  "("  ($#k3_comseq_2 :::"lim"::: )  (Set (Var "s9")) ")" ) ($#k17_complex1 :::".|"::: ) )))) ; 
 
theorem :: SEQ_2:33 (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   ($#k2_seq_2 :::"lim"::: )  (Set  ($#k55_valued_1 :::"|."::: ) (Set  "(" (Set (Var "s"))  ($#k36_valued_1 :::"""::: )  ")" ) ($#k55_valued_1 :::".|"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k17_complex1 :::"|."::: ) (Set  "("  ($#k3_comseq_2 :::"lim"::: )  (Set (Var "s")) ")" ) ($#k17_complex1 :::".|"::: ) )  ($#k2_real_1 :::"""::: )  ))) ; 
 
theorem :: SEQ_2:34 (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   ($#k2_seq_2 :::"lim"::: )  (Set  ($#k55_valued_1 :::"|."::: ) (Set  "(" (Set (Var "s9"))  ($#k51_valued_1 :::"/""::: )  (Set (Var "s")) ")" ) ($#k55_valued_1 :::".|"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k17_complex1 :::"|."::: ) (Set  "("  ($#k3_comseq_2 :::"lim"::: )  (Set (Var "s9")) ")" ) ($#k17_complex1 :::".|"::: ) )  ($#k10_real_1 :::"/"::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set  "("  ($#k3_comseq_2 :::"lim"::: )  (Set (Var "s")) ")" ) ($#k17_complex1 :::".|"::: ) )))) ; 
 
theorem :: SEQ_2:35 (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   ($#k2_seq_2 :::"lim"::: )  (Set  ($#k55_valued_1 :::"|."::: ) (Set  "(" (Set (Var "s"))  ($#k19_valued_1 :::"(#)"::: )  (Set (Var "s1")) ")" ) ($#k55_valued_1 :::".|"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ;