:: SEQ_1  semantic presentation begin  
















definitionmode Real_Sequence is   ($#m1_subset_1 :::"sequence":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ); end; 








theorem :: SEQ_1:1 (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::) "holds"   (Bool  "("  (Bool (Set (Var "f")) "is"   ($#m1_subset_1 :::"Real_Sequence":::)) "iff" (Bool  "("  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set   ($#k5_numbers :::"NAT"::: )  )) & (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 "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x"))) "is"   ($#v1_xreal_0 :::"real"::: )  )  ")" )  ")" )  ")" )) ; 
 
theorem :: SEQ_1:2 (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::) "holds"   (Bool  "("  (Bool (Set (Var "f")) "is"   ($#m1_subset_1 :::"Real_Sequence":::)) "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"   ($#v1_xreal_0 :::"real"::: )  )  ")" )  ")" )  ")" )) ; 
 definitionlet "f" be   ($#v3_valued_0 :::"real-valued"::: )    ($#m1_hidden :::"Function":::); let "x" be    ($#m1_hidden :::"set"::: )  ; :: original: :::"."::: redefine func "f" :::"."::: "x" ->   ($#m1_subset_1 :::"Real":::); end; registration
cluster   ($#v1_relat_1 :::"Relation-like"::: )     ($#v2_relat_1 :::"non-zero"::: )   (Set   ($#k5_numbers :::"NAT"::: )  )  ($#v4_relat_1 :::"-defined"::: )   (Set   ($#k1_numbers :::"REAL"::: )  )  ($#v5_relat_1 :::"-valued"::: )     ($#v1_funct_1 :::"Function-like"::: )     ($#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_1:3 (Bool  "for" (Set (Var "f")) "being"   ($#v2_relat_1 :::"non-zero"::: )    ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"  (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "f")))  ($#r1_tarski :::"c="::: )  (Set (Set  ($#k1_numbers :::"REAL"::: ) )  ($#k6_subset_1 :::"\"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) )))) ; 
 
theorem :: SEQ_1:4 (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "holds"   (Bool  "("  (Bool (Set (Var "seq")) "is"   ($#v2_relat_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_seq_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )))  ")" )) ; 
 
theorem :: SEQ_1:5 (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "holds"   (Bool  "("  (Bool (Set (Var "seq")) "is"   ($#v2_relat_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"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )))  ")" )) ; 
 
theorem :: SEQ_1:6 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   (Bool  "ex" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "seq")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "r")) ($#k1_tarski :::"}"::: ) )))) ; 
 scheme  :: SEQ_1:sch 1 ExRealSeq{ F1(   ($#m1_hidden :::"set"::: )  ) ->   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   } : 
(Bool  "ex" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "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_hidden :::"="::: )  (Set F1 "(" (Set (Var "n")) ")" ))))
 proof 


end; scheme  :: SEQ_1:sch 2 PartFuncExD9{ F1() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , F2() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , P1[   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set F1 "("  ")" ) "," (Set F2 "("  ")" ) "st"  (Bool  "("  (Bool  "("   "for" (Set (Var "d")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" ) "holds"   (Bool  "("  (Bool (Set (Var "d"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))) "iff" (Bool  "ex" (Set (Var "c")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F2 "("  ")" ) "st" (Bool P1[(Set (Var "d")) "," (Set (Var "c"))]))  ")" )  ")" ) & (Bool  "("   "for" (Set (Var "d")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" )  "st" (Bool (Bool (Set (Var "d"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f"))))) "holds"  (Bool P1[(Set (Var "d")) "," (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "d")))])  ")" )  ")" ))
 proof 


end; scheme  :: SEQ_1:sch 3 LambdaPFD9{ F1() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , F2() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , F3(   ($#m1_hidden :::"set"::: )  ) ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set F2 "("  ")" ), P1[   ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set F1 "("  ")" ) "," (Set F2 "("  ")" ) "st"  (Bool  "("  (Bool  "("   "for" (Set (Var "d")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" ) "holds"   (Bool  "("  (Bool (Set (Var "d"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))) "iff" (Bool P1[(Set (Var "d"))])  ")" )  ")" ) & (Bool  "("   "for" (Set (Var "d")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" )  "st" (Bool (Bool (Set (Var "d"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f"))))) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "d")))  ($#r1_hidden :::"="::: )  (Set F3 "(" (Set (Var "d")) ")" ))  ")" )  ")" ))
 proof 


end; scheme  :: SEQ_1:sch 4 UnPartFuncD9{ F1() ->    ($#m1_hidden :::"set"::: )  , F2() ->    ($#m1_hidden :::"set"::: )  , F3() ->    ($#m1_hidden :::"set"::: )  , F4(   ($#m1_hidden :::"set"::: )  ) ->    ($#m1_hidden :::"set"::: )   } : 
(Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set F1 "("  ")" ) "," (Set F2 "("  ")" )  "st" (Bool (Bool (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set F3 "("  ")" )) & (Bool  "("   "for" (Set (Var "c")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" )  "st" (Bool (Bool (Set (Var "c"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f"))))) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set F4 "(" (Set (Var "c")) ")" ))  ")" ) & (Bool (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "g")))  ($#r1_hidden :::"="::: )  (Set F3 "("  ")" )) & (Bool  "("   "for" (Set (Var "c")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" )  "st" (Bool (Bool (Set (Var "c"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "g"))))) "holds"  (Bool (Set (Set (Var "g"))  ($#k1_funct_1 :::"."::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set F4 "(" (Set (Var "c")) ")" ))  ")" )) "holds"  (Bool (Set (Var "f"))  ($#r2_relset_1 :::"="::: )  (Set (Var "g"))))
 proof 


end; 
theorem :: SEQ_1:7 (Bool  "for" (Set (Var "seq")) "," (Set (Var "seq1")) "," (Set (Var "seq2")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "holds"   (Bool  "("  (Bool (Set (Var "seq"))  ($#r2_funct_2 :::"="::: )  (Set (Set (Var "seq1"))  ($#k3_valued_1 :::"+"::: )  (Set (Var "seq2")))) "iff" (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_hidden :::"="::: )  (Set (Set  "(" (Set (Var "seq1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set (Var "seq2"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" ))))  ")" )) ; 
 
theorem :: SEQ_1:8 (Bool  "for" (Set (Var "seq")) "," (Set (Var "seq1")) "," (Set (Var "seq2")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "holds"   (Bool  "("  (Bool (Set (Var "seq"))  ($#r2_funct_2 :::"="::: )  (Set (Set (Var "seq1"))  ($#k20_valued_1 :::"(#)"::: )  (Set (Var "seq2")))) "iff" (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_hidden :::"="::: )  (Set (Set  "(" (Set (Var "seq1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "seq2"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" ))))  ")" )) ; 
 
theorem :: SEQ_1:9 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "holds"   (Bool  "("  (Bool (Set (Var "seq1"))  ($#r2_funct_2 :::"="::: )  (Set (Set (Var "r"))  ($#k26_valued_1 :::"(#)"::: )  (Set (Var "seq2")))) "iff" (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "seq1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "r"))  ($#k4_real_1 :::"*"::: )  (Set  "(" (Set (Var "seq2"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" ))))  ")" ))) ; 
 
theorem :: SEQ_1:10 (Bool  "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "holds"   (Bool  "("  (Bool (Set (Var "seq1"))  ($#r2_funct_2 :::"="::: )  (Set   ($#k32_valued_1 :::"-"::: )  (Set (Var "seq2")))) "iff" (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "seq1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Set  "(" (Set (Var "seq2"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" ))))  ")" )) ; 
 
theorem :: SEQ_1:11 (Bool  "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "holds"  (Bool (Set (Set (Var "seq1"))  ($#k47_valued_1 :::"-"::: )  (Set (Var "seq2")))  ($#r2_funct_2 :::"="::: )  (Set (Set (Var "seq1"))  ($#k3_valued_1 :::"+"::: )  (Set  "("  ($#k32_valued_1 :::"-"::: )  (Set (Var "seq2")) ")" )))) ; 
 
theorem :: SEQ_1:12 (Bool  "for" (Set (Var "seq1")) "," (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "holds"   (Bool  "("  (Bool (Set (Var "seq1"))  ($#r2_funct_2 :::"="::: )  (Set   ($#k56_valued_1 :::"abs"::: )  (Set (Var "seq")))) "iff" (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "seq1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set   ($#k18_complex1 :::"abs"::: )  (Set  "(" (Set (Var "seq"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n")) ")" ))))  ")" )) ; 
 
theorem :: SEQ_1:13 (Bool  "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "," (Set (Var "seq3")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "holds"  (Bool (Set (Set  "(" (Set (Var "seq1"))  ($#k3_valued_1 :::"+"::: )  (Set (Var "seq2")) ")" )  ($#k3_valued_1 :::"+"::: )  (Set (Var "seq3")))  ($#r2_funct_2 :::"="::: )  (Set (Set (Var "seq1"))  ($#k3_valued_1 :::"+"::: )  (Set  "(" (Set (Var "seq2"))  ($#k3_valued_1 :::"+"::: )  (Set (Var "seq3")) ")" )))) ; 
 
theorem :: SEQ_1:14 (Bool  "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "," (Set (Var "seq3")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "holds"  (Bool (Set (Set  "(" (Set (Var "seq1"))  ($#k20_valued_1 :::"(#)"::: )  (Set (Var "seq2")) ")" )  ($#k20_valued_1 :::"(#)"::: )  (Set (Var "seq3")))  ($#r2_funct_2 :::"="::: )  (Set (Set (Var "seq1"))  ($#k20_valued_1 :::"(#)"::: )  (Set  "(" (Set (Var "seq2"))  ($#k20_valued_1 :::"(#)"::: )  (Set (Var "seq3")) ")" )))) ; 
 
theorem :: SEQ_1:15 (Bool  "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "," (Set (Var "seq3")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "holds"  (Bool (Set (Set  "(" (Set (Var "seq1"))  ($#k3_valued_1 :::"+"::: )  (Set (Var "seq2")) ")" )  ($#k20_valued_1 :::"(#)"::: )  (Set (Var "seq3")))  ($#r2_funct_2 :::"="::: )  (Set (Set  "(" (Set (Var "seq1"))  ($#k20_valued_1 :::"(#)"::: )  (Set (Var "seq3")) ")" )  ($#k3_valued_1 :::"+"::: )  (Set  "(" (Set (Var "seq2"))  ($#k20_valued_1 :::"(#)"::: )  (Set (Var "seq3")) ")" )))) ; 
 
theorem :: SEQ_1:16 (Bool  "for" (Set (Var "seq3")) "," (Set (Var "seq1")) "," (Set (Var "seq2")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "holds"  (Bool (Set (Set (Var "seq3"))  ($#k20_valued_1 :::"(#)"::: )  (Set  "(" (Set (Var "seq1"))  ($#k3_valued_1 :::"+"::: )  (Set (Var "seq2")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set (Set  "(" (Set (Var "seq3"))  ($#k20_valued_1 :::"(#)"::: )  (Set (Var "seq1")) ")" )  ($#k3_valued_1 :::"+"::: )  (Set  "(" (Set (Var "seq3"))  ($#k20_valued_1 :::"(#)"::: )  (Set (Var "seq2")) ")" )))) ; 
 
theorem :: SEQ_1:17 (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "holds"  (Bool (Set   ($#k32_valued_1 :::"-"::: )  (Set (Var "seq")))  ($#r2_funct_2 :::"="::: )  (Set (Set  "("  ($#k1_real_1 :::"-"::: )  (Num 1) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set (Var "seq"))))) ; 
 
theorem :: SEQ_1:18 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "holds"  (Bool (Set (Set (Var "r"))  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set (Var "seq1"))  ($#k20_valued_1 :::"(#)"::: )  (Set (Var "seq2")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set (Set  "(" (Set (Var "r"))  ($#k26_valued_1 :::"(#)"::: )  (Set (Var "seq1")) ")" )  ($#k20_valued_1 :::"(#)"::: )  (Set (Var "seq2")))))) ; 
 
theorem :: SEQ_1:19 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "holds"  (Bool (Set (Set (Var "r"))  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set (Var "seq1"))  ($#k20_valued_1 :::"(#)"::: )  (Set (Var "seq2")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set (Set (Var "seq1"))  ($#k20_valued_1 :::"(#)"::: )  (Set  "(" (Set (Var "r"))  ($#k26_valued_1 :::"(#)"::: )  (Set (Var "seq2")) ")" ))))) ; 
 
theorem :: SEQ_1:20 (Bool  "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "," (Set (Var "seq3")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "holds"  (Bool (Set (Set  "(" (Set (Var "seq1"))  ($#k47_valued_1 :::"-"::: )  (Set (Var "seq2")) ")" )  ($#k20_valued_1 :::"(#)"::: )  (Set (Var "seq3")))  ($#r2_funct_2 :::"="::: )  (Set (Set  "(" (Set (Var "seq1"))  ($#k20_valued_1 :::"(#)"::: )  (Set (Var "seq3")) ")" )  ($#k47_valued_1 :::"-"::: )  (Set  "(" (Set (Var "seq2"))  ($#k20_valued_1 :::"(#)"::: )  (Set (Var "seq3")) ")" )))) ; 
 
theorem :: SEQ_1:21 (Bool  "for" (Set (Var "seq3")) "," (Set (Var "seq1")) "," (Set (Var "seq2")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "holds"  (Bool (Set (Set  "(" (Set (Var "seq3"))  ($#k20_valued_1 :::"(#)"::: )  (Set (Var "seq1")) ")" )  ($#k47_valued_1 :::"-"::: )  (Set  "(" (Set (Var "seq3"))  ($#k20_valued_1 :::"(#)"::: )  (Set (Var "seq2")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set (Set (Var "seq3"))  ($#k20_valued_1 :::"(#)"::: )  (Set  "(" (Set (Var "seq1"))  ($#k47_valued_1 :::"-"::: )  (Set (Var "seq2")) ")" )))) ; 
 
theorem :: SEQ_1:22 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "holds"  (Bool (Set (Set (Var "r"))  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set (Var "seq1"))  ($#k3_valued_1 :::"+"::: )  (Set (Var "seq2")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set (Set  "(" (Set (Var "r"))  ($#k26_valued_1 :::"(#)"::: )  (Set (Var "seq1")) ")" )  ($#k3_valued_1 :::"+"::: )  (Set  "(" (Set (Var "r"))  ($#k26_valued_1 :::"(#)"::: )  (Set (Var "seq2")) ")" ))))) ; 
 
theorem :: SEQ_1:23 (Bool  "for" (Set (Var "r")) "," (Set (Var "p")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "holds"  (Bool (Set (Set  "(" (Set (Var "r"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "p")) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set (Var "seq")))  ($#r2_funct_2 :::"="::: )  (Set (Set (Var "r"))  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set (Var "p"))  ($#k26_valued_1 :::"(#)"::: )  (Set (Var "seq")) ")" ))))) ; 
 
theorem :: SEQ_1:24 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "holds"  (Bool (Set (Set (Var "r"))  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set (Var "seq1"))  ($#k47_valued_1 :::"-"::: )  (Set (Var "seq2")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set (Set  "(" (Set (Var "r"))  ($#k26_valued_1 :::"(#)"::: )  (Set (Var "seq1")) ")" )  ($#k47_valued_1 :::"-"::: )  (Set  "(" (Set (Var "r"))  ($#k26_valued_1 :::"(#)"::: )  (Set (Var "seq2")) ")" ))))) ; 
 
theorem :: SEQ_1:25 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "seq1")) "," (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "holds"  (Bool (Set (Set (Var "r"))  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set (Var "seq1"))  ($#k52_valued_1 :::"/""::: )  (Set (Var "seq")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set (Set  "(" (Set (Var "r"))  ($#k26_valued_1 :::"(#)"::: )  (Set (Var "seq1")) ")" )  ($#k52_valued_1 :::"/""::: )  (Set (Var "seq")))))) ; 
 
theorem :: SEQ_1:26 (Bool  "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "," (Set (Var "seq3")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "holds"  (Bool (Set (Set (Var "seq1"))  ($#k47_valued_1 :::"-"::: )  (Set  "(" (Set (Var "seq2"))  ($#k3_valued_1 :::"+"::: )  (Set (Var "seq3")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set (Set  "(" (Set (Var "seq1"))  ($#k47_valued_1 :::"-"::: )  (Set (Var "seq2")) ")" )  ($#k47_valued_1 :::"-"::: )  (Set (Var "seq3"))))) ; 
 
theorem :: SEQ_1:27 (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "holds"  (Bool (Set (Num 1)  ($#k26_valued_1 :::"(#)"::: )  (Set (Var "seq")))  ($#r2_funct_2 :::"="::: )  (Set (Var "seq")))) ; 
 
theorem :: SEQ_1:28 canceled; 
 
theorem :: SEQ_1:29 (Bool  "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "holds"  (Bool (Set (Set (Var "seq1"))  ($#k47_valued_1 :::"-"::: )  (Set  "("  ($#k32_valued_1 :::"-"::: )  (Set (Var "seq2")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set (Set (Var "seq1"))  ($#k3_valued_1 :::"+"::: )  (Set (Var "seq2"))))) ; 
 
theorem :: SEQ_1:30 (Bool  "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "," (Set (Var "seq3")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "holds"  (Bool (Set (Set (Var "seq1"))  ($#k47_valued_1 :::"-"::: )  (Set  "(" (Set (Var "seq2"))  ($#k47_valued_1 :::"-"::: )  (Set (Var "seq3")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set (Set  "(" (Set (Var "seq1"))  ($#k47_valued_1 :::"-"::: )  (Set (Var "seq2")) ")" )  ($#k3_valued_1 :::"+"::: )  (Set (Var "seq3"))))) ; 
 
theorem :: SEQ_1:31 (Bool  "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "," (Set (Var "seq3")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "holds"  (Bool (Set (Set (Var "seq1"))  ($#k3_valued_1 :::"+"::: )  (Set  "(" (Set (Var "seq2"))  ($#k47_valued_1 :::"-"::: )  (Set (Var "seq3")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set (Set  "(" (Set (Var "seq1"))  ($#k3_valued_1 :::"+"::: )  (Set (Var "seq2")) ")" )  ($#k47_valued_1 :::"-"::: )  (Set (Var "seq3"))))) ; 
 
theorem :: SEQ_1:32 (Bool  "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "holds"   (Bool  "("  (Bool (Set (Set  "("  ($#k32_valued_1 :::"-"::: )  (Set (Var "seq1")) ")" )  ($#k20_valued_1 :::"(#)"::: )  (Set (Var "seq2")))  ($#r2_funct_2 :::"="::: )  (Set   ($#k32_valued_1 :::"-"::: )  (Set  "(" (Set (Var "seq1"))  ($#k20_valued_1 :::"(#)"::: )  (Set (Var "seq2")) ")" ))) & (Bool (Set (Set (Var "seq1"))  ($#k20_valued_1 :::"(#)"::: )  (Set  "("  ($#k32_valued_1 :::"-"::: )  (Set (Var "seq2")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set   ($#k32_valued_1 :::"-"::: )  (Set  "(" (Set (Var "seq1"))  ($#k20_valued_1 :::"(#)"::: )  (Set (Var "seq2")) ")" )))  ")" )) ; 
 
theorem :: SEQ_1:33 (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  "st" (Bool (Bool (Set (Var "seq")) "is"   ($#v2_relat_1 :::"non-zero"::: )  )) "holds"  (Bool (Set (Set (Var "seq"))  ($#k37_valued_1 :::"""::: )  ) "is"   ($#v2_relat_1 :::"non-zero"::: )  )) ; 
 
theorem :: SEQ_1:34 canceled; 
 
theorem :: SEQ_1:35 (Bool  "for" (Set (Var "seq")) "," (Set (Var "seq1")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "holds"   (Bool  "("  (Bool  "("  (Bool (Set (Var "seq")) "is"   ($#v2_relat_1 :::"non-zero"::: )  ) & (Bool (Set (Var "seq1")) "is"   ($#v2_relat_1 :::"non-zero"::: )  )  ")" ) "iff" (Bool (Set (Set (Var "seq"))  ($#k20_valued_1 :::"(#)"::: )  (Set (Var "seq1"))) "is"   ($#v2_relat_1 :::"non-zero"::: )  )  ")" )) ; 
 
theorem :: SEQ_1:36 (Bool  "for" (Set (Var "seq")) "," (Set (Var "seq1")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "holds"  (Bool (Set (Set  "(" (Set (Var "seq"))  ($#k37_valued_1 :::"""::: )  ")" )  ($#k20_valued_1 :::"(#)"::: )  (Set  "(" (Set (Var "seq1"))  ($#k37_valued_1 :::"""::: )  ")" ))  ($#r2_funct_2 :::"="::: )  (Set (Set  "(" (Set (Var "seq"))  ($#k20_valued_1 :::"(#)"::: )  (Set (Var "seq1")) ")" )  ($#k37_valued_1 :::"""::: )  ))) ; 
 
theorem :: SEQ_1:37 (Bool  "for" (Set (Var "seq")) "," (Set (Var "seq1")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  "st" (Bool (Bool (Set (Var "seq")) "is"   ($#v2_relat_1 :::"non-zero"::: )  )) "holds"  (Bool (Set (Set  "(" (Set (Var "seq1"))  ($#k52_valued_1 :::"/""::: )  (Set (Var "seq")) ")" )  ($#k20_valued_1 :::"(#)"::: )  (Set (Var "seq")))  ($#r2_funct_2 :::"="::: )  (Set (Var "seq1")))) ; 
 
theorem :: SEQ_1:38 (Bool  "for" (Set (Var "seq9")) "," (Set (Var "seq")) "," (Set (Var "seq19")) "," (Set (Var "seq1")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "holds"  (Bool (Set (Set  "(" (Set (Var "seq9"))  ($#k52_valued_1 :::"/""::: )  (Set (Var "seq")) ")" )  ($#k20_valued_1 :::"(#)"::: )  (Set  "(" (Set (Var "seq19"))  ($#k52_valued_1 :::"/""::: )  (Set (Var "seq1")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set (Set  "(" (Set (Var "seq9"))  ($#k20_valued_1 :::"(#)"::: )  (Set (Var "seq19")) ")" )  ($#k52_valued_1 :::"/""::: )  (Set  "(" (Set (Var "seq"))  ($#k20_valued_1 :::"(#)"::: )  (Set (Var "seq1")) ")" )))) ; 
 
theorem :: SEQ_1:39 (Bool  "for" (Set (Var "seq")) "," (Set (Var "seq1")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  "st" (Bool (Bool (Set (Var "seq")) "is"   ($#v2_relat_1 :::"non-zero"::: )  ) & (Bool (Set (Var "seq1")) "is"   ($#v2_relat_1 :::"non-zero"::: )  )) "holds"  (Bool (Set (Set (Var "seq"))  ($#k52_valued_1 :::"/""::: )  (Set (Var "seq1"))) "is"   ($#v2_relat_1 :::"non-zero"::: )  )) ; 
 
theorem :: SEQ_1:40 (Bool  "for" (Set (Var "seq")) "," (Set (Var "seq1")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "holds"  (Bool (Set (Set  "(" (Set (Var "seq"))  ($#k52_valued_1 :::"/""::: )  (Set (Var "seq1")) ")" )  ($#k37_valued_1 :::"""::: )  )  ($#r2_funct_2 :::"="::: )  (Set (Set (Var "seq1"))  ($#k52_valued_1 :::"/""::: )  (Set (Var "seq"))))) ; 
 
theorem :: SEQ_1:41 (Bool  "for" (Set (Var "seq2")) "," (Set (Var "seq1")) "," (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "holds"  (Bool (Set (Set (Var "seq2"))  ($#k20_valued_1 :::"(#)"::: )  (Set  "(" (Set (Var "seq1"))  ($#k52_valued_1 :::"/""::: )  (Set (Var "seq")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set (Set  "(" (Set (Var "seq2"))  ($#k20_valued_1 :::"(#)"::: )  (Set (Var "seq1")) ")" )  ($#k52_valued_1 :::"/""::: )  (Set (Var "seq"))))) ; 
 
theorem :: SEQ_1:42 (Bool  "for" (Set (Var "seq2")) "," (Set (Var "seq")) "," (Set (Var "seq1")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "holds"  (Bool (Set (Set (Var "seq2"))  ($#k52_valued_1 :::"/""::: )  (Set  "(" (Set (Var "seq"))  ($#k52_valued_1 :::"/""::: )  (Set (Var "seq1")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set (Set  "(" (Set (Var "seq2"))  ($#k20_valued_1 :::"(#)"::: )  (Set (Var "seq1")) ")" )  ($#k52_valued_1 :::"/""::: )  (Set (Var "seq"))))) ; 
 
theorem :: SEQ_1:43 (Bool  "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "," (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  "st" (Bool (Bool (Set (Var "seq1")) "is"   ($#v2_relat_1 :::"non-zero"::: )  )) "holds"  (Bool (Set (Set (Var "seq2"))  ($#k52_valued_1 :::"/""::: )  (Set (Var "seq")))  ($#r2_funct_2 :::"="::: )  (Set (Set  "(" (Set (Var "seq2"))  ($#k20_valued_1 :::"(#)"::: )  (Set (Var "seq1")) ")" )  ($#k52_valued_1 :::"/""::: )  (Set  "(" (Set (Var "seq"))  ($#k20_valued_1 :::"(#)"::: )  (Set (Var "seq1")) ")" )))) ; 
 
theorem :: SEQ_1:44 (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 "r"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "seq")) "is"   ($#v2_relat_1 :::"non-zero"::: )  )) "holds"  (Bool (Set (Set (Var "r"))  ($#k26_valued_1 :::"(#)"::: )  (Set (Var "seq"))) "is"   ($#v2_relat_1 :::"non-zero"::: )  ))) ; 
 
theorem :: SEQ_1:45 (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  "st" (Bool (Bool (Set (Var "seq")) "is"   ($#v2_relat_1 :::"non-zero"::: )  )) "holds"  (Bool (Set   ($#k32_valued_1 :::"-"::: )  (Set (Var "seq"))) "is"   ($#v2_relat_1 :::"non-zero"::: )  )) ; 
 
theorem :: SEQ_1:46 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "holds"  (Bool (Set (Set  "(" (Set (Var "r"))  ($#k26_valued_1 :::"(#)"::: )  (Set (Var "seq")) ")" )  ($#k37_valued_1 :::"""::: )  )  ($#r2_funct_2 :::"="::: )  (Set (Set  "(" (Set (Var "r"))  ($#k5_xcmplx_0 :::"""::: )  ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set (Var "seq"))  ($#k37_valued_1 :::"""::: )  ")" ))))) ; 
 
theorem :: SEQ_1:47 (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "holds"  (Bool (Set (Set  "("  ($#k32_valued_1 :::"-"::: )  (Set (Var "seq")) ")" )  ($#k37_valued_1 :::"""::: )  )  ($#r2_funct_2 :::"="::: )  (Set (Set  "("  ($#k1_real_1 :::"-"::: )  (Num 1) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set  "(" (Set (Var "seq"))  ($#k37_valued_1 :::"""::: )  ")" )))) ; 
 
theorem :: SEQ_1:48 (Bool  "for" (Set (Var "seq1")) "," (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "holds"   (Bool  "("  (Bool (Set   ($#k32_valued_1 :::"-"::: )  (Set  "(" (Set (Var "seq1"))  ($#k52_valued_1 :::"/""::: )  (Set (Var "seq")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set (Set  "("  ($#k32_valued_1 :::"-"::: )  (Set (Var "seq1")) ")" )  ($#k52_valued_1 :::"/""::: )  (Set (Var "seq")))) & (Bool (Set (Set (Var "seq1"))  ($#k52_valued_1 :::"/""::: )  (Set  "("  ($#k32_valued_1 :::"-"::: )  (Set (Var "seq")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set   ($#k32_valued_1 :::"-"::: )  (Set  "(" (Set (Var "seq1"))  ($#k52_valued_1 :::"/""::: )  (Set (Var "seq")) ")" )))  ")" )) ; 
 
theorem :: SEQ_1:49 (Bool  "for" (Set (Var "seq1")) "," (Set (Var "seq")) "," (Set (Var "seq19")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "holds"   (Bool  "("  (Bool (Set (Set  "(" (Set (Var "seq1"))  ($#k52_valued_1 :::"/""::: )  (Set (Var "seq")) ")" )  ($#k3_valued_1 :::"+"::: )  (Set  "(" (Set (Var "seq19"))  ($#k52_valued_1 :::"/""::: )  (Set (Var "seq")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set (Set  "(" (Set (Var "seq1"))  ($#k3_valued_1 :::"+"::: )  (Set (Var "seq19")) ")" )  ($#k52_valued_1 :::"/""::: )  (Set (Var "seq")))) & (Bool (Set (Set  "(" (Set (Var "seq1"))  ($#k52_valued_1 :::"/""::: )  (Set (Var "seq")) ")" )  ($#k47_valued_1 :::"-"::: )  (Set  "(" (Set (Var "seq19"))  ($#k52_valued_1 :::"/""::: )  (Set (Var "seq")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set (Set  "(" (Set (Var "seq1"))  ($#k47_valued_1 :::"-"::: )  (Set (Var "seq19")) ")" )  ($#k52_valued_1 :::"/""::: )  (Set (Var "seq"))))  ")" )) ; 
 
theorem :: SEQ_1:50 (Bool  "for" (Set (Var "seq")) "," (Set (Var "seq9")) "," (Set (Var "seq1")) "," (Set (Var "seq19")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  "st" (Bool (Bool (Set (Var "seq")) "is"   ($#v2_relat_1 :::"non-zero"::: )  ) & (Bool (Set (Var "seq9")) "is"   ($#v2_relat_1 :::"non-zero"::: )  )) "holds"  (Bool  "("  (Bool (Set (Set  "(" (Set (Var "seq1"))  ($#k52_valued_1 :::"/""::: )  (Set (Var "seq")) ")" )  ($#k3_valued_1 :::"+"::: )  (Set  "(" (Set (Var "seq19"))  ($#k52_valued_1 :::"/""::: )  (Set (Var "seq9")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "seq1"))  ($#k20_valued_1 :::"(#)"::: )  (Set (Var "seq9")) ")" )  ($#k3_valued_1 :::"+"::: )  (Set  "(" (Set (Var "seq19"))  ($#k20_valued_1 :::"(#)"::: )  (Set (Var "seq")) ")" ) ")" )  ($#k52_valued_1 :::"/""::: )  (Set  "(" (Set (Var "seq"))  ($#k20_valued_1 :::"(#)"::: )  (Set (Var "seq9")) ")" ))) & (Bool (Set (Set  "(" (Set (Var "seq1"))  ($#k52_valued_1 :::"/""::: )  (Set (Var "seq")) ")" )  ($#k47_valued_1 :::"-"::: )  (Set  "(" (Set (Var "seq19"))  ($#k52_valued_1 :::"/""::: )  (Set (Var "seq9")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "seq1"))  ($#k20_valued_1 :::"(#)"::: )  (Set (Var "seq9")) ")" )  ($#k47_valued_1 :::"-"::: )  (Set  "(" (Set (Var "seq19"))  ($#k20_valued_1 :::"(#)"::: )  (Set (Var "seq")) ")" ) ")" )  ($#k52_valued_1 :::"/""::: )  (Set  "(" (Set (Var "seq"))  ($#k20_valued_1 :::"(#)"::: )  (Set (Var "seq9")) ")" )))  ")" )) ; 
 
theorem :: SEQ_1:51 (Bool  "for" (Set (Var "seq19")) "," (Set (Var "seq")) "," (Set (Var "seq9")) "," (Set (Var "seq1")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "holds"  (Bool (Set (Set  "(" (Set (Var "seq19"))  ($#k52_valued_1 :::"/""::: )  (Set (Var "seq")) ")" )  ($#k52_valued_1 :::"/""::: )  (Set  "(" (Set (Var "seq9"))  ($#k52_valued_1 :::"/""::: )  (Set (Var "seq1")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set (Set  "(" (Set (Var "seq19"))  ($#k20_valued_1 :::"(#)"::: )  (Set (Var "seq1")) ")" )  ($#k52_valued_1 :::"/""::: )  (Set  "(" (Set (Var "seq"))  ($#k20_valued_1 :::"(#)"::: )  (Set (Var "seq9")) ")" )))) ; 
 
theorem :: SEQ_1:52 (Bool  "for" (Set (Var "seq")) "," (Set (Var "seq9")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "holds"  (Bool (Set   ($#k56_valued_1 :::"abs"::: )  (Set  "(" (Set (Var "seq"))  ($#k20_valued_1 :::"(#)"::: )  (Set (Var "seq9")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set (Set  "("  ($#k56_valued_1 :::"abs"::: )  (Set (Var "seq")) ")" )  ($#k20_valued_1 :::"(#)"::: )  (Set  "("  ($#k56_valued_1 :::"abs"::: )  (Set (Var "seq9")) ")" )))) ; 
 
theorem :: SEQ_1:53 (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  "st" (Bool (Bool (Set (Var "seq")) "is"   ($#v2_relat_1 :::"non-zero"::: )  )) "holds"  (Bool (Set   ($#k56_valued_1 :::"abs"::: )  (Set (Var "seq"))) "is"   ($#v2_relat_1 :::"non-zero"::: )  )) ; 
 
theorem :: SEQ_1:54 (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "holds"  (Bool (Set (Set  "("  ($#k56_valued_1 :::"abs"::: )  (Set (Var "seq")) ")" )  ($#k37_valued_1 :::"""::: )  )  ($#r2_funct_2 :::"="::: )  (Set   ($#k56_valued_1 :::"abs"::: )  (Set  "(" (Set (Var "seq"))  ($#k37_valued_1 :::"""::: )  ")" )))) ; 
 
theorem :: SEQ_1:55 (Bool  "for" (Set (Var "seq9")) "," (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "holds"  (Bool (Set   ($#k56_valued_1 :::"abs"::: )  (Set  "(" (Set (Var "seq9"))  ($#k52_valued_1 :::"/""::: )  (Set (Var "seq")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set (Set  "("  ($#k56_valued_1 :::"abs"::: )  (Set (Var "seq9")) ")" )  ($#k52_valued_1 :::"/""::: )  (Set  "("  ($#k56_valued_1 :::"abs"::: )  (Set (Var "seq")) ")" )))) ; 
 
theorem :: SEQ_1:56 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "seq")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "holds"  (Bool (Set   ($#k56_valued_1 :::"abs"::: )  (Set  "(" (Set (Var "r"))  ($#k26_valued_1 :::"(#)"::: )  (Set (Var "seq")) ")" ))  ($#r2_funct_2 :::"="::: )  (Set (Set  "("  ($#k18_complex1 :::"abs"::: )  (Set (Var "r")) ")" )  ($#k26_valued_1 :::"(#)"::: )  (Set  "("  ($#k56_valued_1 :::"abs"::: )  (Set (Var "seq")) ")" ))))) ;