:: TOPRNS_1  semantic presentation begin  definitionlet "N" be   ($#m1_hidden :::"Nat":::); mode Real_Sequence of "N" is   ($#m1_subset_1 :::"sequence":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  "N" ")" ); end; 
































theorem :: TOPRNS_1:1 (Bool  "for" (Set (Var "N")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::) "holds"   (Bool  "("  (Bool (Set (Var "f")) "is"   ($#m1_subset_1 :::"Real_Sequence":::) "of" (Set (Var "N"))) "iff" (Bool  "("  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set   ($#k5_numbers :::"NAT"::: )  )) & (Bool  "("   "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "n"))) "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "N")) ")" ))  ")" )  ")" )  ")" ))) ; 
 definitionlet "N" be    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "IT" be   ($#m1_subset_1 :::"Real_Sequence":::) "of" (Set (Const "N")); attr "IT" is  :::"non-zero":::  means :: TOPRNS_1:def 1 (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  "IT")  ($#r1_tarski :::"c="::: )  (Set   ($#k8_struct_0 :::"NonZero"::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  "N" ")" ))); end; 





:: deftheorem    defines :::"non-zero"::: TOPRNS_1:def 1 :  (Bool  "for" (Set (Var "N")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "IT")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "of" (Set (Var "N")) "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v1_toprns_1 :::"non-zero"::: )  ) "iff" (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "IT")))  ($#r1_tarski :::"c="::: )  (Set   ($#k8_struct_0 :::"NonZero"::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "N")) ")" )))  ")" ))); 
 
theorem :: TOPRNS_1:2 (Bool  "for" (Set (Var "N")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "of" (Set (Var "N")) "holds"   (Bool  "("  (Bool (Set (Var "seq")) "is"   ($#v1_toprns_1 :::"non-zero"::: )  ) "iff" (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k5_numbers :::"NAT"::: )  ))) "holds"  (Bool (Set (Set (Var "seq"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "N")) ")" ))))  ")" ))) ; 
 
theorem :: TOPRNS_1:3 (Bool  "for" (Set (Var "N")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "of" (Set (Var "N")) "holds"   (Bool  "("  (Bool (Set (Var "seq")) "is"   ($#v1_toprns_1 :::"non-zero"::: )  ) "iff" (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   ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "N")) ")" ))))  ")" ))) ; 
 definitionlet "N" be   ($#m1_hidden :::"Nat":::); let "seq1", "seq2" be   ($#m1_subset_1 :::"Real_Sequence":::) "of" (Set (Const "N")); func "seq1" :::"+"::: "seq2" ->   ($#m1_subset_1 :::"Real_Sequence":::) "of" "N" equals :: TOPRNS_1:def 2 (Set "seq1"  ($#k1_vfunct_1 :::"+"::: )  "seq2"); end; 







:: deftheorem    defines :::"+"::: TOPRNS_1:def 2 :  (Bool  "for" (Set (Var "N")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "of" (Set (Var "N")) "holds"  (Bool (Set (Set (Var "seq1"))  ($#k1_toprns_1 :::"+"::: )  (Set (Var "seq2")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "seq1"))  ($#k1_vfunct_1 :::"+"::: )  (Set (Var "seq2")))))); 
 definitionlet "r" be   ($#m1_subset_1 :::"Real":::); let "N" be   ($#m1_hidden :::"Nat":::); let "seq" be   ($#m1_subset_1 :::"Real_Sequence":::) "of" (Set (Const "N")); func "r" :::"*"::: "seq" ->   ($#m1_subset_1 :::"Real_Sequence":::) "of" "N" equals :: TOPRNS_1:def 3 (Set "r"  ($#k4_vfunct_1 :::"(#)"::: )  "seq"); end; 







:: deftheorem    defines :::"*"::: TOPRNS_1:def 3 :  (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "N")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "of" (Set (Var "N")) "holds"  (Bool (Set (Set (Var "r"))  ($#k2_toprns_1 :::"*"::: )  (Set (Var "seq")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "r"))  ($#k4_vfunct_1 :::"(#)"::: )  (Set (Var "seq"))))))); 
 definitionlet "N" be   ($#m1_hidden :::"Nat":::); let "seq" be   ($#m1_subset_1 :::"Real_Sequence":::) "of" (Set (Const "N")); func  :::"-"::: "seq" ->   ($#m1_subset_1 :::"Real_Sequence":::) "of" "N" equals :: TOPRNS_1:def 4 (Set   ($#k5_vfunct_1 :::"-"::: )  "seq"); end; 






:: deftheorem    defines :::"-"::: TOPRNS_1:def 4 :  (Bool  "for" (Set (Var "N")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "of" (Set (Var "N")) "holds"  (Bool (Set   ($#k3_toprns_1 :::"-"::: )  (Set (Var "seq")))  ($#r1_hidden :::"="::: )  (Set   ($#k5_vfunct_1 :::"-"::: )  (Set (Var "seq")))))); 
 definitionlet "N" be   ($#m1_hidden :::"Nat":::); let "seq1", "seq2" be   ($#m1_subset_1 :::"Real_Sequence":::) "of" (Set (Const "N")); func "seq1" :::"-"::: "seq2" ->   ($#m1_subset_1 :::"Real_Sequence":::) "of" "N" equals :: TOPRNS_1:def 5 (Set "seq1"  ($#k1_toprns_1 :::"+"::: )  (Set  "("  ($#k3_toprns_1 :::"-"::: )  "seq2" ")" )); end; 







:: deftheorem    defines :::"-"::: TOPRNS_1:def 5 :  (Bool  "for" (Set (Var "N")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "of" (Set (Var "N")) "holds"  (Bool (Set (Set (Var "seq1"))  ($#k4_toprns_1 :::"-"::: )  (Set (Var "seq2")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "seq1"))  ($#k1_toprns_1 :::"+"::: )  (Set  "("  ($#k3_toprns_1 :::"-"::: )  (Set (Var "seq2")) ")" ))))); 
 definitionlet "N" be   ($#m1_hidden :::"Nat":::); let "seq" be   ($#m1_subset_1 :::"Real_Sequence":::) "of" (Set (Const "N")); func :::"|.":::"seq":::".|"::: ->   ($#m1_subset_1 :::"Real_Sequence":::) means :: TOPRNS_1:def 6 (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set it  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set  ($#k12_euclid :::"|."::: ) (Set  "(" "seq"  ($#k8_nat_1 :::"."::: )  (Set (Var "n")) ")" ) ($#k12_euclid :::".|"::: ) ))); end; 






:: deftheorem    defines :::"|."::: TOPRNS_1:def 6 :  (Bool  "for" (Set (Var "N")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "of" (Set (Var "N"))  (Bool  "for" (Set (Var "b3")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set  ($#k5_toprns_1 :::"|."::: ) (Set (Var "seq")) ($#k5_toprns_1 :::".|"::: ) )) "iff" (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "b3"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set  ($#k12_euclid :::"|."::: ) (Set  "(" (Set (Var "seq"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n")) ")" ) ($#k12_euclid :::".|"::: ) )))  ")" )))); 
 
theorem :: TOPRNS_1:4 (Bool  "for" (Set (Var "N")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "of" (Set (Var "N")) "holds"  (Bool (Set (Set  "(" (Set (Var "seq1"))  ($#k1_toprns_1 :::"+"::: )  (Set (Var "seq2")) ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "seq1"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n")) ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "(" (Set (Var "seq2"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n")) ")" ))))) ; 
 
theorem :: TOPRNS_1:5 (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "N")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "of" (Set (Var "N")) "holds"  (Bool (Set (Set  "(" (Set (Var "r"))  ($#k2_toprns_1 :::"*"::: )  (Set (Var "seq")) ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "r"))  ($#k1_rlvect_1 :::"*"::: )  (Set  "(" (Set (Var "seq"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n")) ")" )))))) ; 
 
theorem :: TOPRNS_1:6 (Bool  "for" (Set (Var "N")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "of" (Set (Var "N")) "holds"  (Bool (Set (Set  "("  ($#k3_toprns_1 :::"-"::: )  (Set (Var "seq")) ")" )  ($#k8_nat_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_algstr_0 :::"-"::: )  (Set  "(" (Set (Var "seq"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n")) ")" ))))) ; 
 
theorem :: TOPRNS_1:7 (Bool  "for" (Set (Var "N")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "w")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "N")) ")" ) "holds"  (Bool (Set (Set  "("  ($#k18_complex1 :::"abs"::: )  (Set (Var "r")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  ($#k12_euclid :::"|."::: ) (Set (Var "w")) ($#k12_euclid :::".|"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k12_euclid :::"|."::: ) (Set  "(" (Set (Var "r"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "w")) ")" ) ($#k12_euclid :::".|"::: ) ))))) ; 
 
theorem :: TOPRNS_1:8 (Bool  "for" (Set (Var "N")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "of" (Set (Var "N")) "holds"  (Bool (Set  ($#k5_toprns_1 :::"|."::: ) (Set  "(" (Set (Var "r"))  ($#k2_toprns_1 :::"*"::: )  (Set (Var "seq")) ")" ) ($#k5_toprns_1 :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k18_complex1 :::"abs"::: )  (Set (Var "r")) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set  ($#k5_toprns_1 :::"|."::: ) (Set (Var "seq")) ($#k5_toprns_1 :::".|"::: ) )))))) ; 
 
theorem :: TOPRNS_1:9 (Bool  "for" (Set (Var "N")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "of" (Set (Var "N")) "holds"  (Bool (Set (Set (Var "seq1"))  ($#k1_toprns_1 :::"+"::: )  (Set (Var "seq2")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "seq2"))  ($#k1_toprns_1 :::"+"::: )  (Set (Var "seq1")))))) ; 
 
theorem :: TOPRNS_1:10 (Bool  "for" (Set (Var "N")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "," (Set (Var "seq3")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "of" (Set (Var "N")) "holds"  (Bool (Set (Set  "(" (Set (Var "seq1"))  ($#k1_toprns_1 :::"+"::: )  (Set (Var "seq2")) ")" )  ($#k1_toprns_1 :::"+"::: )  (Set (Var "seq3")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "seq1"))  ($#k1_toprns_1 :::"+"::: )  (Set  "(" (Set (Var "seq2"))  ($#k1_toprns_1 :::"+"::: )  (Set (Var "seq3")) ")" ))))) ; 
 
theorem :: TOPRNS_1:11 (Bool  "for" (Set (Var "N")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "of" (Set (Var "N")) "holds"  (Bool (Set   ($#k3_toprns_1 :::"-"::: )  (Set (Var "seq")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_real_1 :::"-"::: )  (Num 1) ")" )  ($#k2_toprns_1 :::"*"::: )  (Set (Var "seq")))))) ; 
 
theorem :: TOPRNS_1:12 (Bool  "for" (Set (Var "N")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "of" (Set (Var "N")) "holds"  (Bool (Set (Set (Var "r"))  ($#k2_toprns_1 :::"*"::: )  (Set  "(" (Set (Var "seq1"))  ($#k1_toprns_1 :::"+"::: )  (Set (Var "seq2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "r"))  ($#k2_toprns_1 :::"*"::: )  (Set (Var "seq1")) ")" )  ($#k1_toprns_1 :::"+"::: )  (Set  "(" (Set (Var "r"))  ($#k2_toprns_1 :::"*"::: )  (Set (Var "seq2")) ")" )))))) ; 
 
theorem :: TOPRNS_1:13 (Bool  "for" (Set (Var "N")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "r")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "of" (Set (Var "N")) "holds"  (Bool (Set (Set  "(" (Set (Var "r"))  ($#k8_real_1 :::"*"::: )  (Set (Var "q")) ")" )  ($#k2_toprns_1 :::"*"::: )  (Set (Var "seq")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "r"))  ($#k2_toprns_1 :::"*"::: )  (Set  "(" (Set (Var "q"))  ($#k2_toprns_1 :::"*"::: )  (Set (Var "seq")) ")" )))))) ; 
 
theorem :: TOPRNS_1:14 (Bool  "for" (Set (Var "N")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "of" (Set (Var "N")) "holds"  (Bool (Set (Set (Var "r"))  ($#k2_toprns_1 :::"*"::: )  (Set  "(" (Set (Var "seq1"))  ($#k4_toprns_1 :::"-"::: )  (Set (Var "seq2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "r"))  ($#k2_toprns_1 :::"*"::: )  (Set (Var "seq1")) ")" )  ($#k4_toprns_1 :::"-"::: )  (Set  "(" (Set (Var "r"))  ($#k2_toprns_1 :::"*"::: )  (Set (Var "seq2")) ")" )))))) ; 
 
theorem :: TOPRNS_1:15 (Bool  "for" (Set (Var "N")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "," (Set (Var "seq3")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "of" (Set (Var "N")) "holds"  (Bool (Set (Set (Var "seq1"))  ($#k4_toprns_1 :::"-"::: )  (Set  "(" (Set (Var "seq2"))  ($#k1_toprns_1 :::"+"::: )  (Set (Var "seq3")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "seq1"))  ($#k4_toprns_1 :::"-"::: )  (Set (Var "seq2")) ")" )  ($#k4_toprns_1 :::"-"::: )  (Set (Var "seq3")))))) ; 
 
theorem :: TOPRNS_1:16 (Bool  "for" (Set (Var "N")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "of" (Set (Var "N")) "holds"  (Bool (Set (Num 1)  ($#k2_toprns_1 :::"*"::: )  (Set (Var "seq")))  ($#r1_hidden :::"="::: )  (Set (Var "seq"))))) ; 
 
theorem :: TOPRNS_1:17 (Bool  "for" (Set (Var "N")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "of" (Set (Var "N")) "holds"  (Bool (Set   ($#k3_toprns_1 :::"-"::: )  (Set  "("  ($#k3_toprns_1 :::"-"::: )  (Set (Var "seq")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "seq"))))) ; 
 
theorem :: TOPRNS_1:18 (Bool  "for" (Set (Var "N")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "of" (Set (Var "N")) "holds"  (Bool (Set (Set (Var "seq1"))  ($#k4_toprns_1 :::"-"::: )  (Set  "("  ($#k3_toprns_1 :::"-"::: )  (Set (Var "seq2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "seq1"))  ($#k1_toprns_1 :::"+"::: )  (Set (Var "seq2")))))) ; 
 
theorem :: TOPRNS_1:19 (Bool  "for" (Set (Var "N")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "," (Set (Var "seq3")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "of" (Set (Var "N")) "holds"  (Bool (Set (Set (Var "seq1"))  ($#k4_toprns_1 :::"-"::: )  (Set  "(" (Set (Var "seq2"))  ($#k4_toprns_1 :::"-"::: )  (Set (Var "seq3")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "seq1"))  ($#k4_toprns_1 :::"-"::: )  (Set (Var "seq2")) ")" )  ($#k1_toprns_1 :::"+"::: )  (Set (Var "seq3")))))) ; 
 
theorem :: TOPRNS_1:20 (Bool  "for" (Set (Var "N")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "," (Set (Var "seq3")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "of" (Set (Var "N")) "holds"  (Bool (Set (Set (Var "seq1"))  ($#k1_toprns_1 :::"+"::: )  (Set  "(" (Set (Var "seq2"))  ($#k4_toprns_1 :::"-"::: )  (Set (Var "seq3")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "seq1"))  ($#k1_toprns_1 :::"+"::: )  (Set (Var "seq2")) ")" )  ($#k4_toprns_1 :::"-"::: )  (Set (Var "seq3")))))) ; 
 
theorem :: TOPRNS_1:21 (Bool  "for" (Set (Var "N")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "of" (Set (Var "N"))  "st" (Bool (Bool (Set (Var "r"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "seq")) "is"   ($#v1_toprns_1 :::"non-zero"::: )  )) "holds"  (Bool (Set (Set (Var "r"))  ($#k2_toprns_1 :::"*"::: )  (Set (Var "seq"))) "is"   ($#v1_toprns_1 :::"non-zero"::: )  )))) ; 
 
theorem :: TOPRNS_1:22 (Bool  "for" (Set (Var "N")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "of" (Set (Var "N"))  "st" (Bool (Bool (Set (Var "seq")) "is"   ($#v1_toprns_1 :::"non-zero"::: )  )) "holds"  (Bool (Set   ($#k3_toprns_1 :::"-"::: )  (Set (Var "seq"))) "is"   ($#v1_toprns_1 :::"non-zero"::: )  ))) ; 
 
theorem :: TOPRNS_1:23 (Bool  "for" (Set (Var "N")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set  ($#k12_euclid :::"|."::: ) (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "N")) ")" ) ")" ) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: TOPRNS_1:24 (Bool  "for" (Set (Var "N")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "w")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "N")) ")" )  "st" (Bool (Bool (Set  ($#k12_euclid :::"|."::: ) (Set (Var "w")) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Var "w"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "N")) ")" ))))) ; 
 
theorem :: TOPRNS_1:25 (Bool  "for" (Set (Var "N")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "w")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "N")) ")" ) "holds"  (Bool (Set  ($#k12_euclid :::"|."::: ) (Set (Var "w")) ($#k12_euclid :::".|"::: ) )  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )))) ; 
 
theorem :: TOPRNS_1:26 (Bool  "for" (Set (Var "N")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "w")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "N")) ")" ) "holds"  (Bool (Set  ($#k12_euclid :::"|."::: ) (Set  "("  ($#k4_algstr_0 :::"-"::: )  (Set (Var "w")) ")" ) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Set  ($#k12_euclid :::"|."::: ) (Set (Var "w")) ($#k12_euclid :::".|"::: ) )))) ; 
 
theorem :: TOPRNS_1:27 (Bool  "for" (Set (Var "N")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "w1")) "," (Set (Var "w2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "N")) ")" ) "holds"  (Bool (Set  ($#k12_euclid :::"|."::: ) (Set  "(" (Set (Var "w1"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "w2")) ")" ) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Set  ($#k12_euclid :::"|."::: ) (Set  "(" (Set (Var "w2"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "w1")) ")" ) ($#k12_euclid :::".|"::: ) )))) ; 
 
theorem :: TOPRNS_1:28 (Bool  "for" (Set (Var "N")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "w1")) "," (Set (Var "w2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "N")) ")" ) "holds"   (Bool  "("  (Bool (Set  ($#k12_euclid :::"|."::: ) (Set  "(" (Set (Var "w1"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "w2")) ")" ) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) "iff" (Bool (Set (Var "w1"))  ($#r1_hidden :::"="::: )  (Set (Var "w2")))  ")" ))) ; 
 
theorem :: TOPRNS_1:29 (Bool  "for" (Set (Var "N")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "w1")) "," (Set (Var "w2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "N")) ")" ) "holds"  (Bool (Set  ($#k12_euclid :::"|."::: ) (Set  "(" (Set (Var "w1"))  ($#k3_rlvect_1 :::"+"::: )  (Set (Var "w2")) ")" ) ($#k12_euclid :::".|"::: ) )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  ($#k12_euclid :::"|."::: ) (Set (Var "w1")) ($#k12_euclid :::".|"::: ) )  ($#k7_real_1 :::"+"::: )  (Set  ($#k12_euclid :::"|."::: ) (Set (Var "w2")) ($#k12_euclid :::".|"::: ) ))))) ; 
 
theorem :: TOPRNS_1:30 (Bool  "for" (Set (Var "N")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "w1")) "," (Set (Var "w2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "N")) ")" ) "holds"  (Bool (Set  ($#k12_euclid :::"|."::: ) (Set  "(" (Set (Var "w1"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "w2")) ")" ) ($#k12_euclid :::".|"::: ) )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  ($#k12_euclid :::"|."::: ) (Set (Var "w1")) ($#k12_euclid :::".|"::: ) )  ($#k7_real_1 :::"+"::: )  (Set  ($#k12_euclid :::"|."::: ) (Set (Var "w2")) ($#k12_euclid :::".|"::: ) ))))) ; 
 
theorem :: TOPRNS_1:31 (Bool  "for" (Set (Var "N")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "w1")) "," (Set (Var "w2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "N")) ")" ) "holds"  (Bool (Set (Set  ($#k12_euclid :::"|."::: ) (Set (Var "w1")) ($#k12_euclid :::".|"::: ) )  ($#k9_real_1 :::"-"::: )  (Set  ($#k12_euclid :::"|."::: ) (Set (Var "w2")) ($#k12_euclid :::".|"::: ) ))  ($#r1_xxreal_0 :::"<="::: )  (Set  ($#k12_euclid :::"|."::: ) (Set  "(" (Set (Var "w1"))  ($#k3_rlvect_1 :::"+"::: )  (Set (Var "w2")) ")" ) ($#k12_euclid :::".|"::: ) )))) ; 
 
theorem :: TOPRNS_1:32 (Bool  "for" (Set (Var "N")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "w1")) "," (Set (Var "w2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "N")) ")" ) "holds"  (Bool (Set (Set  ($#k12_euclid :::"|."::: ) (Set (Var "w1")) ($#k12_euclid :::".|"::: ) )  ($#k9_real_1 :::"-"::: )  (Set  ($#k12_euclid :::"|."::: ) (Set (Var "w2")) ($#k12_euclid :::".|"::: ) ))  ($#r1_xxreal_0 :::"<="::: )  (Set  ($#k12_euclid :::"|."::: ) (Set  "(" (Set (Var "w1"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "w2")) ")" ) ($#k12_euclid :::".|"::: ) )))) ; 
 
theorem :: TOPRNS_1:33 (Bool  "for" (Set (Var "N")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "w1")) "," (Set (Var "w2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "N")) ")" )  "st" (Bool (Bool (Set (Var "w1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "w2")))) "holds"  (Bool (Set  ($#k12_euclid :::"|."::: ) (Set  "(" (Set (Var "w1"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "w2")) ")" ) ($#k12_euclid :::".|"::: ) )  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )))) ; 
 
theorem :: TOPRNS_1:34 (Bool  "for" (Set (Var "N")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "w1")) "," (Set (Var "w2")) "," (Set (Var "w")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "N")) ")" ) "holds"  (Bool (Set  ($#k12_euclid :::"|."::: ) (Set  "(" (Set (Var "w1"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "w2")) ")" ) ($#k12_euclid :::".|"::: ) )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  ($#k12_euclid :::"|."::: ) (Set  "(" (Set (Var "w1"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "w")) ")" ) ($#k12_euclid :::".|"::: ) )  ($#k7_real_1 :::"+"::: )  (Set  ($#k12_euclid :::"|."::: ) (Set  "(" (Set (Var "w"))  ($#k5_algstr_0 :::"-"::: )  (Set (Var "w2")) ")" ) ($#k12_euclid :::".|"::: ) ))))) ; 
 definitionlet "N" be    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "IT" be   ($#m1_subset_1 :::"Real_Sequence":::) "of" (Set (Const "N")); attr "IT" is  :::"bounded":::  means :: TOPRNS_1:def 7 (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  ($#k12_euclid :::"|."::: ) (Set  "(" "IT"  ($#k8_nat_1 :::"."::: )  (Set (Var "n")) ")" ) ($#k12_euclid :::".|"::: ) )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r"))))); end; 





:: deftheorem    defines :::"bounded"::: TOPRNS_1:def 7 :  (Bool  "for" (Set (Var "N")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "IT")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "of" (Set (Var "N")) "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v2_toprns_1 :::"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  ($#k12_euclid :::"|."::: ) (Set  "(" (Set (Var "IT"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n")) ")" ) ($#k12_euclid :::".|"::: ) )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r")))))  ")" ))); 
 
theorem :: TOPRNS_1:35 (Bool  "for" (Set (Var "N")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "of" (Set (Var "N"))  (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  ($#k12_euclid :::"|."::: ) (Set  "(" (Set (Var "seq"))  ($#k8_nat_1 :::"."::: )  (Set (Var "m")) ")" ) ($#k12_euclid :::".|"::: ) )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r")))  ")" )  ")" ))))) ; 
 definitionlet "N" be    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "IT" be   ($#m1_subset_1 :::"Real_Sequence":::) "of" (Set (Const "N")); attr "IT" is  :::"convergent":::  means :: TOPRNS_1:def 8 (Bool  "ex" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  "N" ")" ) "st"  (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r")))) "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  ($#k12_euclid :::"|."::: ) (Set  "(" (Set  "(" "IT"  ($#k8_nat_1 :::"."::: )  (Set (Var "m")) ")" )  ($#k5_algstr_0 :::"-"::: )  (Set (Var "g")) ")" ) ($#k12_euclid :::".|"::: ) )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r"))))))); end; 





:: deftheorem    defines :::"convergent"::: TOPRNS_1:def 8 :  (Bool  "for" (Set (Var "N")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "IT")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "of" (Set (Var "N")) "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v3_toprns_1 :::"convergent"::: )  ) "iff" (Bool  "ex" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "N")) ")" ) "st"  (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r")))) "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  ($#k12_euclid :::"|."::: ) (Set  "(" (Set  "(" (Set (Var "IT"))  ($#k8_nat_1 :::"."::: )  (Set (Var "m")) ")" )  ($#k5_algstr_0 :::"-"::: )  (Set (Var "g")) ")" ) ($#k12_euclid :::".|"::: ) )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r")))))))  ")" ))); 
 definitionlet "N" be    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "seq" be   ($#m1_subset_1 :::"Real_Sequence":::) "of" (Set (Const "N")); assume 
(Bool (Set (Const "seq")) "is"   ($#v3_toprns_1 :::"convergent"::: )  )
 ; func  :::"lim"::: "seq" ->   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  "N" ")" ) means :: TOPRNS_1:def 9 (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r")))) "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  ($#k12_euclid :::"|."::: ) (Set  "(" (Set  "(" "seq"  ($#k8_nat_1 :::"."::: )  (Set (Var "m")) ")" )  ($#k5_algstr_0 :::"-"::: )  it ")" ) ($#k12_euclid :::".|"::: ) )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r")))))); end; 







:: deftheorem    defines :::"lim"::: TOPRNS_1:def 9 :  (Bool  "for" (Set (Var "N")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "of" (Set (Var "N"))  "st" (Bool (Bool (Set (Var "seq")) "is"   ($#v3_toprns_1 :::"convergent"::: )  )) "holds"  (Bool  "for" (Set (Var "b3")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "N")) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_toprns_1 :::"lim"::: )  (Set (Var "seq")))) "iff" (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r")))) "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  ($#k12_euclid :::"|."::: ) (Set  "(" (Set  "(" (Set (Var "seq"))  ($#k8_nat_1 :::"."::: )  (Set (Var "m")) ")" )  ($#k5_algstr_0 :::"-"::: )  (Set (Var "b3")) ")" ) ($#k12_euclid :::".|"::: ) )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "r"))))))  ")" )))); 
 
theorem :: TOPRNS_1:36 (Bool  "for" (Set (Var "N")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "seq")) "," (Set (Var "seq9")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "of" (Set (Var "N"))  "st" (Bool (Bool (Set (Var "seq")) "is"   ($#v3_toprns_1 :::"convergent"::: )  ) & (Bool (Set (Var "seq9")) "is"   ($#v3_toprns_1 :::"convergent"::: )  )) "holds"  (Bool (Set (Set (Var "seq"))  ($#k1_toprns_1 :::"+"::: )  (Set (Var "seq9"))) "is"   ($#v3_toprns_1 :::"convergent"::: )  ))) ; 
 
theorem :: TOPRNS_1:37 (Bool  "for" (Set (Var "N")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "seq")) "," (Set (Var "seq9")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "of" (Set (Var "N"))  "st" (Bool (Bool (Set (Var "seq")) "is"   ($#v3_toprns_1 :::"convergent"::: )  ) & (Bool (Set (Var "seq9")) "is"   ($#v3_toprns_1 :::"convergent"::: )  )) "holds"  (Bool (Set   ($#k6_toprns_1 :::"lim"::: )  (Set  "(" (Set (Var "seq"))  ($#k1_toprns_1 :::"+"::: )  (Set (Var "seq9")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k6_toprns_1 :::"lim"::: )  (Set (Var "seq")) ")" )  ($#k3_rlvect_1 :::"+"::: )  (Set  "("  ($#k6_toprns_1 :::"lim"::: )  (Set (Var "seq9")) ")" ))))) ; 
 
theorem :: TOPRNS_1:38 (Bool  "for" (Set (Var "N")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "of" (Set (Var "N"))  "st" (Bool (Bool (Set (Var "seq")) "is"   ($#v3_toprns_1 :::"convergent"::: )  )) "holds"  (Bool (Set (Set (Var "r"))  ($#k2_toprns_1 :::"*"::: )  (Set (Var "seq"))) "is"   ($#v3_toprns_1 :::"convergent"::: )  )))) ; 
 
theorem :: TOPRNS_1:39 (Bool  "for" (Set (Var "N")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "of" (Set (Var "N"))  "st" (Bool (Bool (Set (Var "seq")) "is"   ($#v3_toprns_1 :::"convergent"::: )  )) "holds"  (Bool (Set   ($#k6_toprns_1 :::"lim"::: )  (Set  "(" (Set (Var "r"))  ($#k2_toprns_1 :::"*"::: )  (Set (Var "seq")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "r"))  ($#k1_rlvect_1 :::"*"::: )  (Set  "("  ($#k6_toprns_1 :::"lim"::: )  (Set (Var "seq")) ")" )))))) ; 
 
theorem :: TOPRNS_1:40 (Bool  "for" (Set (Var "N")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "of" (Set (Var "N"))  "st" (Bool (Bool (Set (Var "seq")) "is"   ($#v3_toprns_1 :::"convergent"::: )  )) "holds"  (Bool (Set   ($#k3_toprns_1 :::"-"::: )  (Set (Var "seq"))) "is"   ($#v3_toprns_1 :::"convergent"::: )  ))) ; 
 
theorem :: TOPRNS_1:41 (Bool  "for" (Set (Var "N")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "of" (Set (Var "N"))  "st" (Bool (Bool (Set (Var "seq")) "is"   ($#v3_toprns_1 :::"convergent"::: )  )) "holds"  (Bool (Set   ($#k6_toprns_1 :::"lim"::: )  (Set  "("  ($#k3_toprns_1 :::"-"::: )  (Set (Var "seq")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_algstr_0 :::"-"::: )  (Set  "("  ($#k6_toprns_1 :::"lim"::: )  (Set (Var "seq")) ")" ))))) ; 
 
theorem :: TOPRNS_1:42 (Bool  "for" (Set (Var "N")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "seq")) "," (Set (Var "seq9")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "of" (Set (Var "N"))  "st" (Bool (Bool (Set (Var "seq")) "is"   ($#v3_toprns_1 :::"convergent"::: )  ) & (Bool (Set (Var "seq9")) "is"   ($#v3_toprns_1 :::"convergent"::: )  )) "holds"  (Bool (Set (Set (Var "seq"))  ($#k4_toprns_1 :::"-"::: )  (Set (Var "seq9"))) "is"   ($#v3_toprns_1 :::"convergent"::: )  ))) ; 
 
theorem :: TOPRNS_1:43 (Bool  "for" (Set (Var "N")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "seq")) "," (Set (Var "seq9")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "of" (Set (Var "N"))  "st" (Bool (Bool (Set (Var "seq")) "is"   ($#v3_toprns_1 :::"convergent"::: )  ) & (Bool (Set (Var "seq9")) "is"   ($#v3_toprns_1 :::"convergent"::: )  )) "holds"  (Bool (Set   ($#k6_toprns_1 :::"lim"::: )  (Set  "(" (Set (Var "seq"))  ($#k4_toprns_1 :::"-"::: )  (Set (Var "seq9")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k6_toprns_1 :::"lim"::: )  (Set (Var "seq")) ")" )  ($#k5_algstr_0 :::"-"::: )  (Set  "("  ($#k6_toprns_1 :::"lim"::: )  (Set (Var "seq9")) ")" ))))) ; 
 
theorem :: TOPRNS_1:44 (Bool  "for" (Set (Var "N")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "of" (Set (Var "N"))  "st" (Bool (Bool (Set (Var "seq")) "is"   ($#v3_toprns_1 :::"convergent"::: )  )) "holds"  (Bool (Set (Var "seq")) "is"   ($#v2_toprns_1 :::"bounded"::: )  ))) ; 
 
theorem :: TOPRNS_1:45 (Bool  "for" (Set (Var "N")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "of" (Set (Var "N"))  "st" (Bool (Bool (Set (Var "seq")) "is"   ($#v3_toprns_1 :::"convergent"::: )  ) & (Bool (Set   ($#k6_toprns_1 :::"lim"::: )  (Set (Var "seq")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "N")) ")" )))) "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  ($#k12_euclid :::"|."::: ) (Set  "("  ($#k6_toprns_1 :::"lim"::: )  (Set (Var "seq")) ")" ) ($#k12_euclid :::".|"::: ) )  ($#k10_real_1 :::"/"::: )  (Num 2))  ($#r1_xxreal_0 :::"<"::: )  (Set  ($#k12_euclid :::"|."::: ) (Set  "(" (Set (Var "seq"))  ($#k8_nat_1 :::"."::: )  (Set (Var "m")) ")" ) ($#k12_euclid :::".|"::: ) )))))) ;