:: LIMFUNC1 semantic presentation begin notationlet "r" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; synonym :::"left_open_halfline"::: "r" for :::"halfline"::: "r"; end; definitionlet "r" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; func :::"left_closed_halfline"::: "r" -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) equals :: LIMFUNC1:def 1 (Set ($#k3_xxreal_1 :::"]."::: ) (Set ($#k2_xxreal_0 :::"-infty"::: ) ) "," "r" ($#k3_xxreal_1 :::".]"::: ) ); func :::"right_closed_halfline"::: "r" -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) equals :: LIMFUNC1:def 2 (Set ($#k2_xxreal_1 :::"[."::: ) "r" "," (Set ($#k1_xxreal_0 :::"+infty"::: ) ) ($#k2_xxreal_1 :::".["::: ) ); func :::"right_open_halfline"::: "r" -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) equals :: LIMFUNC1:def 3 (Set ($#k4_xxreal_1 :::"]."::: ) "r" "," (Set ($#k1_xxreal_0 :::"+infty"::: ) ) ($#k4_xxreal_1 :::".["::: ) ); end; :: deftheorem defines :::"left_closed_halfline"::: LIMFUNC1:def 1 : (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k1_limfunc1 :::"left_closed_halfline"::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set ($#k3_xxreal_1 :::"]."::: ) (Set ($#k2_xxreal_0 :::"-infty"::: ) ) "," (Set (Var "r")) ($#k3_xxreal_1 :::".]"::: ) ))); :: deftheorem defines :::"right_closed_halfline"::: LIMFUNC1:def 2 : (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k2_limfunc1 :::"right_closed_halfline"::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set ($#k2_xxreal_1 :::"[."::: ) (Set (Var "r")) "," (Set ($#k1_xxreal_0 :::"+infty"::: ) ) ($#k2_xxreal_1 :::".["::: ) ))); :: deftheorem defines :::"right_open_halfline"::: LIMFUNC1:def 3 : (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k3_limfunc1 :::"right_open_halfline"::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set ($#k4_xxreal_1 :::"]."::: ) (Set (Var "r")) "," (Set ($#k1_xxreal_0 :::"+infty"::: ) ) ($#k4_xxreal_1 :::".["::: ) ))); theorem :: LIMFUNC1:1 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "seq")) "is" ($#v7_valued_0 :::"non-decreasing"::: ) )) "implies" (Bool (Set (Var "seq")) "is" ($#v2_seq_2 :::"bounded_below"::: ) ) ")" & "(" (Bool (Bool (Set (Var "seq")) "is" ($#v8_valued_0 :::"non-increasing"::: ) )) "implies" (Bool (Set (Var "seq")) "is" ($#v1_seq_2 :::"bounded_above"::: ) ) ")" ")" )) ; theorem :: LIMFUNC1:2 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v2_relat_1 :::"non-zero"::: ) ) & (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" ($#v7_valued_0 :::"non-decreasing"::: ) )) "holds" (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 ($#k6_numbers :::"0"::: ) )))) ; theorem :: LIMFUNC1:3 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v2_relat_1 :::"non-zero"::: ) ) & (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" ($#v8_valued_0 :::"non-increasing"::: ) )) "holds" (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")))))) ; theorem :: LIMFUNC1:4 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k2_seq_2 :::"lim"::: ) (Set (Var "seq"))))) "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 ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "seq")) ($#k1_seq_1 :::"."::: ) (Set (Var "m"))))))) ; theorem :: LIMFUNC1:5 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k2_seq_2 :::"lim"::: ) (Set (Var "seq"))))) "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 "(" ($#k2_seq_2 :::"lim"::: ) (Set (Var "seq")) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2)) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "seq")) ($#k1_seq_1 :::"."::: ) (Set (Var "m"))))))) ; definitionlet "seq" be ($#m1_subset_1 :::"Real_Sequence":::); attr "seq" is :::"divergent_to+infty"::: means :: LIMFUNC1:def 4 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (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 (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set "seq" ($#k1_seq_1 :::"."::: ) (Set (Var "m"))))))); attr "seq" is :::"divergent_to-infty"::: means :: LIMFUNC1:def 5 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (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 "seq" ($#k1_seq_1 :::"."::: ) (Set (Var "m"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r")))))); end; :: deftheorem defines :::"divergent_to+infty"::: LIMFUNC1:def 4 : (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "holds" (Bool "(" (Bool (Set (Var "seq")) "is" ($#v1_limfunc1 :::"divergent_to+infty"::: ) ) "iff" (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (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 (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "seq")) ($#k1_seq_1 :::"."::: ) (Set (Var "m"))))))) ")" )); :: deftheorem defines :::"divergent_to-infty"::: LIMFUNC1:def 5 : (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "holds" (Bool "(" (Bool (Set (Var "seq")) "is" ($#v2_limfunc1 :::"divergent_to-infty"::: ) ) "iff" (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (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 (Var "seq")) ($#k1_seq_1 :::"."::: ) (Set (Var "m"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r")))))) ")" )); theorem :: LIMFUNC1:6 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool "(" (Bool (Set (Var "seq")) "is" ($#v1_limfunc1 :::"divergent_to+infty"::: ) ) "or" (Bool (Set (Var "seq")) "is" ($#v2_limfunc1 :::"divergent_to-infty"::: ) ) ")" )) "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 (Var "seq")) ($#k1_valued_0 :::"^\"::: ) (Set (Var "m"))) "is" ($#v2_relat_1 :::"non-zero"::: ) )))) ; theorem :: LIMFUNC1:7 (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "holds" (Bool "(" "(" (Bool (Bool (Set (Set (Var "seq")) ($#k1_valued_0 :::"^\"::: ) (Set (Var "k"))) "is" ($#v1_limfunc1 :::"divergent_to+infty"::: ) )) "implies" (Bool (Set (Var "seq")) "is" ($#v1_limfunc1 :::"divergent_to+infty"::: ) ) ")" & "(" (Bool (Bool (Set (Set (Var "seq")) ($#k1_valued_0 :::"^\"::: ) (Set (Var "k"))) "is" ($#v2_limfunc1 :::"divergent_to-infty"::: ) )) "implies" (Bool (Set (Var "seq")) "is" ($#v2_limfunc1 :::"divergent_to-infty"::: ) ) ")" ")" ))) ; theorem :: LIMFUNC1:8 (Bool "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "seq1")) "is" ($#v1_limfunc1 :::"divergent_to+infty"::: ) ) & (Bool (Set (Var "seq2")) "is" ($#v1_limfunc1 :::"divergent_to+infty"::: ) )) "holds" (Bool (Set (Set (Var "seq1")) ($#k3_valued_1 :::"+"::: ) (Set (Var "seq2"))) "is" ($#v1_limfunc1 :::"divergent_to+infty"::: ) )) ; theorem :: LIMFUNC1:9 (Bool "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "seq1")) "is" ($#v1_limfunc1 :::"divergent_to+infty"::: ) ) & (Bool (Set (Var "seq2")) "is" ($#v2_seq_2 :::"bounded_below"::: ) )) "holds" (Bool (Set (Set (Var "seq1")) ($#k3_valued_1 :::"+"::: ) (Set (Var "seq2"))) "is" ($#v1_limfunc1 :::"divergent_to+infty"::: ) )) ; theorem :: LIMFUNC1:10 (Bool "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "seq1")) "is" ($#v1_limfunc1 :::"divergent_to+infty"::: ) ) & (Bool (Set (Var "seq2")) "is" ($#v1_limfunc1 :::"divergent_to+infty"::: ) )) "holds" (Bool (Set (Set (Var "seq1")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "seq2"))) "is" ($#v1_limfunc1 :::"divergent_to+infty"::: ) )) ; theorem :: LIMFUNC1:11 (Bool "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "seq1")) "is" ($#v2_limfunc1 :::"divergent_to-infty"::: ) ) & (Bool (Set (Var "seq2")) "is" ($#v2_limfunc1 :::"divergent_to-infty"::: ) )) "holds" (Bool (Set (Set (Var "seq1")) ($#k3_valued_1 :::"+"::: ) (Set (Var "seq2"))) "is" ($#v2_limfunc1 :::"divergent_to-infty"::: ) )) ; theorem :: LIMFUNC1:12 (Bool "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "seq1")) "is" ($#v2_limfunc1 :::"divergent_to-infty"::: ) ) & (Bool (Set (Var "seq2")) "is" ($#v1_seq_2 :::"bounded_above"::: ) )) "holds" (Bool (Set (Set (Var "seq1")) ($#k3_valued_1 :::"+"::: ) (Set (Var "seq2"))) "is" ($#v2_limfunc1 :::"divergent_to-infty"::: ) )) ; theorem :: LIMFUNC1:13 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "seq")) "is" ($#v1_limfunc1 :::"divergent_to+infty"::: ) ) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "seq"))) "is" ($#v1_limfunc1 :::"divergent_to+infty"::: ) ) ")" & "(" (Bool (Bool (Set (Var "seq")) "is" ($#v1_limfunc1 :::"divergent_to+infty"::: ) ) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "seq"))) "is" ($#v2_limfunc1 :::"divergent_to-infty"::: ) ) ")" & "(" (Bool (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool "(" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "seq")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) )) & (Bool (Set (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "seq"))) "is" ($#v3_funct_1 :::"constant"::: ) ) ")" ) ")" ")" ))) ; theorem :: LIMFUNC1:14 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "seq")) "is" ($#v2_limfunc1 :::"divergent_to-infty"::: ) ) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "seq"))) "is" ($#v2_limfunc1 :::"divergent_to-infty"::: ) ) ")" & "(" (Bool (Bool (Set (Var "seq")) "is" ($#v2_limfunc1 :::"divergent_to-infty"::: ) ) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "seq"))) "is" ($#v1_limfunc1 :::"divergent_to+infty"::: ) ) ")" & "(" (Bool (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool "(" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "seq")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) )) & (Bool (Set (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "seq"))) "is" ($#v3_funct_1 :::"constant"::: ) ) ")" ) ")" ")" ))) ; theorem :: LIMFUNC1:15 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "seq")) "is" ($#v1_limfunc1 :::"divergent_to+infty"::: ) )) "implies" (Bool (Set ($#k32_valued_1 :::"-"::: ) (Set (Var "seq"))) "is" ($#v2_limfunc1 :::"divergent_to-infty"::: ) ) ")" & "(" (Bool (Bool (Set (Var "seq")) "is" ($#v2_limfunc1 :::"divergent_to-infty"::: ) )) "implies" (Bool (Set ($#k32_valued_1 :::"-"::: ) (Set (Var "seq"))) "is" ($#v1_limfunc1 :::"divergent_to+infty"::: ) ) ")" ")" )) ; theorem :: LIMFUNC1:16 (Bool "for" (Set (Var "seq")) "," (Set (Var "seq1")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v2_seq_2 :::"bounded_below"::: ) ) & (Bool (Set (Var "seq1")) "is" ($#v2_limfunc1 :::"divergent_to-infty"::: ) )) "holds" (Bool (Set (Set (Var "seq")) ($#k47_valued_1 :::"-"::: ) (Set (Var "seq1"))) "is" ($#v1_limfunc1 :::"divergent_to+infty"::: ) )) ; theorem :: LIMFUNC1:17 (Bool "for" (Set (Var "seq")) "," (Set (Var "seq1")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v1_seq_2 :::"bounded_above"::: ) ) & (Bool (Set (Var "seq1")) "is" ($#v1_limfunc1 :::"divergent_to+infty"::: ) )) "holds" (Bool (Set (Set (Var "seq")) ($#k47_valued_1 :::"-"::: ) (Set (Var "seq1"))) "is" ($#v2_limfunc1 :::"divergent_to-infty"::: ) )) ; theorem :: LIMFUNC1:18 (Bool "for" (Set (Var "seq")) "," (Set (Var "seq1")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v1_limfunc1 :::"divergent_to+infty"::: ) ) & (Bool (Set (Var "seq1")) "is" ($#v2_comseq_2 :::"convergent"::: ) )) "holds" (Bool (Set (Set (Var "seq")) ($#k3_valued_1 :::"+"::: ) (Set (Var "seq1"))) "is" ($#v1_limfunc1 :::"divergent_to+infty"::: ) )) ; theorem :: LIMFUNC1:19 (Bool "for" (Set (Var "seq")) "," (Set (Var "seq1")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v2_limfunc1 :::"divergent_to-infty"::: ) ) & (Bool (Set (Var "seq1")) "is" ($#v2_comseq_2 :::"convergent"::: ) )) "holds" (Bool (Set (Set (Var "seq")) ($#k3_valued_1 :::"+"::: ) (Set (Var "seq1"))) "is" ($#v2_limfunc1 :::"divergent_to-infty"::: ) )) ; theorem :: LIMFUNC1:20 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "seq")) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Var "n"))) ")" )) "holds" (Bool (Set (Var "seq")) "is" ($#v1_limfunc1 :::"divergent_to+infty"::: ) )) ; theorem :: LIMFUNC1:21 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "seq")) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set (Var "n")))) ")" )) "holds" (Bool (Set (Var "seq")) "is" ($#v2_limfunc1 :::"divergent_to-infty"::: ) )) ; theorem :: LIMFUNC1:22 (Bool "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "seq1")) "is" ($#v1_limfunc1 :::"divergent_to+infty"::: ) ) & (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "seq2")) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::">="::: ) (Set (Var "r"))) ")" ) ")" ))) "holds" (Bool (Set (Set (Var "seq1")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "seq2"))) "is" ($#v1_limfunc1 :::"divergent_to+infty"::: ) )) ; theorem :: LIMFUNC1:23 (Bool "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "seq1")) "is" ($#v2_limfunc1 :::"divergent_to-infty"::: ) ) & (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "seq2")) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::">="::: ) (Set (Var "r"))) ")" ) ")" ))) "holds" (Bool (Set (Set (Var "seq1")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "seq2"))) "is" ($#v2_limfunc1 :::"divergent_to-infty"::: ) )) ; theorem :: LIMFUNC1:24 (Bool "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "seq1")) "is" ($#v2_limfunc1 :::"divergent_to-infty"::: ) ) & (Bool (Set (Var "seq2")) "is" ($#v2_limfunc1 :::"divergent_to-infty"::: ) )) "holds" (Bool (Set (Set (Var "seq1")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "seq2"))) "is" ($#v1_limfunc1 :::"divergent_to+infty"::: ) )) ; theorem :: LIMFUNC1:25 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool "(" (Bool (Set (Var "seq")) "is" ($#v1_limfunc1 :::"divergent_to+infty"::: ) ) "or" (Bool (Set (Var "seq")) "is" ($#v2_limfunc1 :::"divergent_to-infty"::: ) ) ")" )) "holds" (Bool (Set ($#k56_valued_1 :::"abs"::: ) (Set (Var "seq"))) "is" ($#v1_limfunc1 :::"divergent_to+infty"::: ) )) ; theorem :: LIMFUNC1:26 (Bool "for" (Set (Var "seq")) "," (Set (Var "seq1")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v1_limfunc1 :::"divergent_to+infty"::: ) ) & (Bool (Set (Var "seq1")) "is" ($#m2_valued_0 :::"subsequence"::: ) "of" (Set (Var "seq")))) "holds" (Bool (Set (Var "seq1")) "is" ($#v1_limfunc1 :::"divergent_to+infty"::: ) )) ; theorem :: LIMFUNC1:27 (Bool "for" (Set (Var "seq")) "," (Set (Var "seq1")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v2_limfunc1 :::"divergent_to-infty"::: ) ) & (Bool (Set (Var "seq1")) "is" ($#m2_valued_0 :::"subsequence"::: ) "of" (Set (Var "seq")))) "holds" (Bool (Set (Var "seq1")) "is" ($#v2_limfunc1 :::"divergent_to-infty"::: ) )) ; theorem :: LIMFUNC1:28 (Bool "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "seq1")) "is" ($#v1_limfunc1 :::"divergent_to+infty"::: ) ) & (Bool (Set (Var "seq2")) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k2_seq_2 :::"lim"::: ) (Set (Var "seq2"))))) "holds" (Bool (Set (Set (Var "seq1")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "seq2"))) "is" ($#v1_limfunc1 :::"divergent_to+infty"::: ) )) ; theorem :: LIMFUNC1:29 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v7_valued_0 :::"non-decreasing"::: ) ) & (Bool (Bool "not" (Set (Var "seq")) "is" ($#v1_seq_2 :::"bounded_above"::: ) ))) "holds" (Bool (Set (Var "seq")) "is" ($#v1_limfunc1 :::"divergent_to+infty"::: ) )) ; theorem :: LIMFUNC1:30 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v8_valued_0 :::"non-increasing"::: ) ) & (Bool (Bool "not" (Set (Var "seq")) "is" ($#v2_seq_2 :::"bounded_below"::: ) ))) "holds" (Bool (Set (Var "seq")) "is" ($#v2_limfunc1 :::"divergent_to-infty"::: ) )) ; theorem :: LIMFUNC1:31 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v5_valued_0 :::"increasing"::: ) ) & (Bool (Bool "not" (Set (Var "seq")) "is" ($#v1_seq_2 :::"bounded_above"::: ) ))) "holds" (Bool (Set (Var "seq")) "is" ($#v1_limfunc1 :::"divergent_to+infty"::: ) )) ; theorem :: LIMFUNC1:32 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v6_valued_0 :::"decreasing"::: ) ) & (Bool (Bool "not" (Set (Var "seq")) "is" ($#v2_seq_2 :::"bounded_below"::: ) ))) "holds" (Bool (Set (Var "seq")) "is" ($#v2_limfunc1 :::"divergent_to-infty"::: ) )) ; theorem :: LIMFUNC1:33 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "holds" (Bool "(" "not" (Bool (Set (Var "seq")) "is" ($#v1_seqm_3 :::"monotone"::: ) ) "or" (Bool (Set (Var "seq")) "is" ($#v2_comseq_2 :::"convergent"::: ) ) "or" (Bool (Set (Var "seq")) "is" ($#v1_limfunc1 :::"divergent_to+infty"::: ) ) "or" (Bool (Set (Var "seq")) "is" ($#v2_limfunc1 :::"divergent_to-infty"::: ) ) ")" )) ; theorem :: LIMFUNC1:34 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool "(" (Bool (Set (Var "seq")) "is" ($#v1_limfunc1 :::"divergent_to+infty"::: ) ) "or" (Bool (Set (Var "seq")) "is" ($#v2_limfunc1 :::"divergent_to-infty"::: ) ) ")" )) "holds" (Bool "(" (Bool (Set (Set (Var "seq")) ($#k37_valued_1 :::"""::: ) ) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set "(" (Set (Var "seq")) ($#k37_valued_1 :::"""::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) ; theorem :: LIMFUNC1:35 (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 "ex" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "seq")) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))))))) "holds" (Bool (Set (Set (Var "seq")) ($#k37_valued_1 :::"""::: ) ) "is" ($#v1_limfunc1 :::"divergent_to+infty"::: ) )) ; theorem :: LIMFUNC1:36 (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 "ex" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool (Set (Set (Var "seq")) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) ))))) "holds" (Bool (Set (Set (Var "seq")) ($#k37_valued_1 :::"""::: ) ) "is" ($#v2_limfunc1 :::"divergent_to-infty"::: ) )) ; theorem :: LIMFUNC1:37 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v2_relat_1 :::"non-zero"::: ) ) & (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" ($#v7_valued_0 :::"non-decreasing"::: ) )) "holds" (Bool (Set (Set (Var "seq")) ($#k37_valued_1 :::"""::: ) ) "is" ($#v2_limfunc1 :::"divergent_to-infty"::: ) )) ; theorem :: LIMFUNC1:38 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v2_relat_1 :::"non-zero"::: ) ) & (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" ($#v8_valued_0 :::"non-increasing"::: ) )) "holds" (Bool (Set (Set (Var "seq")) ($#k37_valued_1 :::"""::: ) ) "is" ($#v1_limfunc1 :::"divergent_to+infty"::: ) )) ; theorem :: LIMFUNC1:39 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v2_relat_1 :::"non-zero"::: ) ) & (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" ($#v5_valued_0 :::"increasing"::: ) )) "holds" (Bool (Set (Set (Var "seq")) ($#k37_valued_1 :::"""::: ) ) "is" ($#v2_limfunc1 :::"divergent_to-infty"::: ) )) ; theorem :: LIMFUNC1:40 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v2_relat_1 :::"non-zero"::: ) ) & (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" ($#v6_valued_0 :::"decreasing"::: ) )) "holds" (Bool (Set (Set (Var "seq")) ($#k37_valued_1 :::"""::: ) ) "is" ($#v1_limfunc1 :::"divergent_to+infty"::: ) )) ; theorem :: LIMFUNC1:41 (Bool "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "seq1")) "is" ($#v1_comseq_2 :::"bounded"::: ) ) & (Bool "(" (Bool (Set (Var "seq2")) "is" ($#v1_limfunc1 :::"divergent_to+infty"::: ) ) "or" (Bool (Set (Var "seq2")) "is" ($#v2_limfunc1 :::"divergent_to-infty"::: ) ) ")" )) "holds" (Bool "(" (Bool (Set (Set (Var "seq1")) ($#k52_valued_1 :::"/""::: ) (Set (Var "seq2"))) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set "(" (Set (Var "seq1")) ($#k52_valued_1 :::"/""::: ) (Set (Var "seq2")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) ; theorem :: LIMFUNC1:42 (Bool "for" (Set (Var "seq")) "," (Set (Var "seq1")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v1_limfunc1 :::"divergent_to+infty"::: ) ) & (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 "seq1")) ($#k1_seq_1 :::"."::: ) (Set (Var "n")))) ")" )) "holds" (Bool (Set (Var "seq1")) "is" ($#v1_limfunc1 :::"divergent_to+infty"::: ) )) ; theorem :: LIMFUNC1:43 (Bool "for" (Set (Var "seq")) "," (Set (Var "seq1")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v2_limfunc1 :::"divergent_to-infty"::: ) ) & (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_xxreal_0 :::"<="::: ) (Set (Set (Var "seq")) ($#k1_seq_1 :::"."::: ) (Set (Var "n")))) ")" )) "holds" (Bool (Set (Var "seq1")) "is" ($#v2_limfunc1 :::"divergent_to-infty"::: ) )) ; definitionlet "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ); attr "f" is :::"convergent_in+infty"::: means :: LIMFUNC1:def 6 (Bool "(" (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "g"))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) "f")) ")" )) ")" ) & (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v1_limfunc1 :::"divergent_to+infty"::: ) ) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "seq"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) "f"))) "holds" (Bool "(" (Bool (Set "f" ($#k8_funct_2 :::"/*"::: ) (Set (Var "seq"))) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set "(" "f" ($#k8_funct_2 :::"/*"::: ) (Set (Var "seq")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "g"))) ")" ))) ")" ); attr "f" is :::"divergent_in+infty_to+infty"::: means :: LIMFUNC1:def 7 (Bool "(" (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "g"))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) "f")) ")" )) ")" ) & (Bool "(" "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v1_limfunc1 :::"divergent_to+infty"::: ) ) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "seq"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) "f"))) "holds" (Bool (Set "f" ($#k8_funct_2 :::"/*"::: ) (Set (Var "seq"))) "is" ($#v1_limfunc1 :::"divergent_to+infty"::: ) ) ")" ) ")" ); attr "f" is :::"divergent_in+infty_to-infty"::: means :: LIMFUNC1:def 8 (Bool "(" (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "g"))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) "f")) ")" )) ")" ) & (Bool "(" "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v1_limfunc1 :::"divergent_to+infty"::: ) ) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "seq"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) "f"))) "holds" (Bool (Set "f" ($#k8_funct_2 :::"/*"::: ) (Set (Var "seq"))) "is" ($#v2_limfunc1 :::"divergent_to-infty"::: ) ) ")" ) ")" ); attr "f" is :::"convergent_in-infty"::: means :: LIMFUNC1:def 9 (Bool "(" (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "g")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) "f")) ")" )) ")" ) & (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v2_limfunc1 :::"divergent_to-infty"::: ) ) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "seq"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) "f"))) "holds" (Bool "(" (Bool (Set "f" ($#k8_funct_2 :::"/*"::: ) (Set (Var "seq"))) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set "(" "f" ($#k8_funct_2 :::"/*"::: ) (Set (Var "seq")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "g"))) ")" ))) ")" ); attr "f" is :::"divergent_in-infty_to+infty"::: means :: LIMFUNC1:def 10 (Bool "(" (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "g")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) "f")) ")" )) ")" ) & (Bool "(" "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v2_limfunc1 :::"divergent_to-infty"::: ) ) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "seq"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) "f"))) "holds" (Bool (Set "f" ($#k8_funct_2 :::"/*"::: ) (Set (Var "seq"))) "is" ($#v1_limfunc1 :::"divergent_to+infty"::: ) ) ")" ) ")" ); attr "f" is :::"divergent_in-infty_to-infty"::: means :: LIMFUNC1:def 11 (Bool "(" (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "g")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) "f")) ")" )) ")" ) & (Bool "(" "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v2_limfunc1 :::"divergent_to-infty"::: ) ) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "seq"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) "f"))) "holds" (Bool (Set "f" ($#k8_funct_2 :::"/*"::: ) (Set (Var "seq"))) "is" ($#v2_limfunc1 :::"divergent_to-infty"::: ) ) ")" ) ")" ); end; :: deftheorem defines :::"convergent_in+infty"::: LIMFUNC1:def 6 : (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v3_limfunc1 :::"convergent_in+infty"::: ) ) "iff" (Bool "(" (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "g"))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) ")" )) ")" ) & (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v1_limfunc1 :::"divergent_to+infty"::: ) ) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "seq"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k8_funct_2 :::"/*"::: ) (Set (Var "seq"))) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set "(" (Set (Var "f")) ($#k8_funct_2 :::"/*"::: ) (Set (Var "seq")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "g"))) ")" ))) ")" ) ")" )); :: deftheorem defines :::"divergent_in+infty_to+infty"::: LIMFUNC1:def 7 : (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v4_limfunc1 :::"divergent_in+infty_to+infty"::: ) ) "iff" (Bool "(" (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "g"))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) ")" )) ")" ) & (Bool "(" "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v1_limfunc1 :::"divergent_to+infty"::: ) ) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "seq"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k8_funct_2 :::"/*"::: ) (Set (Var "seq"))) "is" ($#v1_limfunc1 :::"divergent_to+infty"::: ) ) ")" ) ")" ) ")" )); :: deftheorem defines :::"divergent_in+infty_to-infty"::: LIMFUNC1:def 8 : (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v5_limfunc1 :::"divergent_in+infty_to-infty"::: ) ) "iff" (Bool "(" (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "g"))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) ")" )) ")" ) & (Bool "(" "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v1_limfunc1 :::"divergent_to+infty"::: ) ) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "seq"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k8_funct_2 :::"/*"::: ) (Set (Var "seq"))) "is" ($#v2_limfunc1 :::"divergent_to-infty"::: ) ) ")" ) ")" ) ")" )); :: deftheorem defines :::"convergent_in-infty"::: LIMFUNC1:def 9 : (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v6_limfunc1 :::"convergent_in-infty"::: ) ) "iff" (Bool "(" (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "g")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) ")" )) ")" ) & (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v2_limfunc1 :::"divergent_to-infty"::: ) ) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "seq"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k8_funct_2 :::"/*"::: ) (Set (Var "seq"))) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set "(" (Set (Var "f")) ($#k8_funct_2 :::"/*"::: ) (Set (Var "seq")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "g"))) ")" ))) ")" ) ")" )); :: deftheorem defines :::"divergent_in-infty_to+infty"::: LIMFUNC1:def 10 : (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v7_limfunc1 :::"divergent_in-infty_to+infty"::: ) ) "iff" (Bool "(" (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "g")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) ")" )) ")" ) & (Bool "(" "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v2_limfunc1 :::"divergent_to-infty"::: ) ) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "seq"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k8_funct_2 :::"/*"::: ) (Set (Var "seq"))) "is" ($#v1_limfunc1 :::"divergent_to+infty"::: ) ) ")" ) ")" ) ")" )); :: deftheorem defines :::"divergent_in-infty_to-infty"::: LIMFUNC1:def 11 : (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v8_limfunc1 :::"divergent_in-infty_to-infty"::: ) ) "iff" (Bool "(" (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "g")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) ")" )) ")" ) & (Bool "(" "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v2_limfunc1 :::"divergent_to-infty"::: ) ) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "seq"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k8_funct_2 :::"/*"::: ) (Set (Var "seq"))) "is" ($#v2_limfunc1 :::"divergent_to-infty"::: ) ) ")" ) ")" ) ")" )); theorem :: LIMFUNC1:44 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v3_limfunc1 :::"convergent_in+infty"::: ) ) "iff" (Bool "(" (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "g"))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) ")" )) ")" ) & (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "for" (Set (Var "g1")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "g1")))) "holds" (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "for" (Set (Var "r1")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r1"))) & (Bool (Set (Var "r1")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set "(" (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "r1")) ")" ) ($#k9_real_1 :::"-"::: ) (Set (Var "g")) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "g1"))))))) ")" ) ")" )) ; theorem :: LIMFUNC1:45 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v6_limfunc1 :::"convergent_in-infty"::: ) ) "iff" (Bool "(" (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "g")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) ")" )) ")" ) & (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "for" (Set (Var "g1")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "g1")))) "holds" (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "for" (Set (Var "r1")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "r1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set (Var "r1")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set "(" (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "r1")) ")" ) ($#k9_real_1 :::"-"::: ) (Set (Var "g")) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "g1"))))))) ")" ) ")" )) ; theorem :: LIMFUNC1:46 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v4_limfunc1 :::"divergent_in+infty_to+infty"::: ) ) "iff" (Bool "(" (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "g"))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) ")" )) ")" ) & (Bool "(" "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "for" (Set (Var "r1")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r1"))) & (Bool (Set (Var "r1")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Var "g")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "r1")))))) ")" ) ")" ) ")" )) ; theorem :: LIMFUNC1:47 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v5_limfunc1 :::"divergent_in+infty_to-infty"::: ) ) "iff" (Bool "(" (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "g"))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) ")" )) ")" ) & (Bool "(" "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "for" (Set (Var "r1")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r1"))) & (Bool (Set (Var "r1")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "r1"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "g"))))) ")" ) ")" ) ")" )) ; theorem :: LIMFUNC1:48 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v7_limfunc1 :::"divergent_in-infty_to+infty"::: ) ) "iff" (Bool "(" (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "g")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) ")" )) ")" ) & (Bool "(" "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "for" (Set (Var "r1")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "r1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set (Var "r1")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Var "g")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "r1")))))) ")" ) ")" ) ")" )) ; theorem :: LIMFUNC1:49 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v8_limfunc1 :::"divergent_in-infty_to-infty"::: ) ) "iff" (Bool "(" (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "g")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) ")" )) ")" ) & (Bool "(" "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "for" (Set (Var "r1")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "r1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set (Var "r1")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "r1"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "g"))))) ")" ) ")" ) ")" )) ; theorem :: LIMFUNC1:50 (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f1")) "is" ($#v4_limfunc1 :::"divergent_in+infty_to+infty"::: ) ) & (Bool (Set (Var "f2")) "is" ($#v4_limfunc1 :::"divergent_in+infty_to+infty"::: ) ) & (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "g"))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f1")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f2")) ")" ))) ")" )) ")" )) "holds" (Bool "(" (Bool (Set (Set (Var "f1")) ($#k3_valued_1 :::"+"::: ) (Set (Var "f2"))) "is" ($#v4_limfunc1 :::"divergent_in+infty_to+infty"::: ) ) & (Bool (Set (Set (Var "f1")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "f2"))) "is" ($#v4_limfunc1 :::"divergent_in+infty_to+infty"::: ) ) ")" )) ; theorem :: LIMFUNC1:51 (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f1")) "is" ($#v5_limfunc1 :::"divergent_in+infty_to-infty"::: ) ) & (Bool (Set (Var "f2")) "is" ($#v5_limfunc1 :::"divergent_in+infty_to-infty"::: ) ) & (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "g"))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f1")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f2")) ")" ))) ")" )) ")" )) "holds" (Bool "(" (Bool (Set (Set (Var "f1")) ($#k3_valued_1 :::"+"::: ) (Set (Var "f2"))) "is" ($#v5_limfunc1 :::"divergent_in+infty_to-infty"::: ) ) & (Bool (Set (Set (Var "f1")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "f2"))) "is" ($#v4_limfunc1 :::"divergent_in+infty_to+infty"::: ) ) ")" )) ; theorem :: LIMFUNC1:52 (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f1")) "is" ($#v7_limfunc1 :::"divergent_in-infty_to+infty"::: ) ) & (Bool (Set (Var "f2")) "is" ($#v7_limfunc1 :::"divergent_in-infty_to+infty"::: ) ) & (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "g")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f1")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f2")) ")" ))) ")" )) ")" )) "holds" (Bool "(" (Bool (Set (Set (Var "f1")) ($#k3_valued_1 :::"+"::: ) (Set (Var "f2"))) "is" ($#v7_limfunc1 :::"divergent_in-infty_to+infty"::: ) ) & (Bool (Set (Set (Var "f1")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "f2"))) "is" ($#v7_limfunc1 :::"divergent_in-infty_to+infty"::: ) ) ")" )) ; theorem :: LIMFUNC1:53 (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f1")) "is" ($#v8_limfunc1 :::"divergent_in-infty_to-infty"::: ) ) & (Bool (Set (Var "f2")) "is" ($#v8_limfunc1 :::"divergent_in-infty_to-infty"::: ) ) & (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "g")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f1")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f2")) ")" ))) ")" )) ")" )) "holds" (Bool "(" (Bool (Set (Set (Var "f1")) ($#k3_valued_1 :::"+"::: ) (Set (Var "f2"))) "is" ($#v8_limfunc1 :::"divergent_in-infty_to-infty"::: ) ) & (Bool (Set (Set (Var "f1")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "f2"))) "is" ($#v7_limfunc1 :::"divergent_in-infty_to+infty"::: ) ) ")" )) ; theorem :: LIMFUNC1:54 (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f1")) "is" ($#v4_limfunc1 :::"divergent_in+infty_to+infty"::: ) ) & (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "g"))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f1")) ($#k3_valued_1 :::"+"::: ) (Set (Var "f2")) ")" ))) ")" )) ")" ) & (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Set (Set (Var "f2")) ($#k2_partfun1 :::"|"::: ) (Set "(" ($#k3_limfunc1 :::"right_open_halfline"::: ) (Set (Var "r")) ")" )) "is" ($#v2_seq_2 :::"bounded_below"::: ) ))) "holds" (Bool (Set (Set (Var "f1")) ($#k3_valued_1 :::"+"::: ) (Set (Var "f2"))) "is" ($#v4_limfunc1 :::"divergent_in+infty_to+infty"::: ) )) ; theorem :: LIMFUNC1:55 (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f1")) "is" ($#v4_limfunc1 :::"divergent_in+infty_to+infty"::: ) ) & (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "g"))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f1")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "f2")) ")" ))) ")" )) ")" ) & (Bool "ex" (Set (Var "r")) "," (Set (Var "r1")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool "(" "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f2")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k3_limfunc1 :::"right_open_halfline"::: ) (Set (Var "r1")) ")" )))) "holds" (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "f2")) ($#k1_seq_1 :::"."::: ) (Set (Var "g")))) ")" ) ")" ))) "holds" (Bool (Set (Set (Var "f1")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "f2"))) "is" ($#v4_limfunc1 :::"divergent_in+infty_to+infty"::: ) )) ; theorem :: LIMFUNC1:56 (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f1")) "is" ($#v7_limfunc1 :::"divergent_in-infty_to+infty"::: ) ) & (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "g")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f1")) ($#k3_valued_1 :::"+"::: ) (Set (Var "f2")) ")" ))) ")" )) ")" ) & (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Set (Set (Var "f2")) ($#k2_partfun1 :::"|"::: ) (Set "(" ($#k10_prob_1 :::"left_open_halfline"::: ) (Set (Var "r")) ")" )) "is" ($#v2_seq_2 :::"bounded_below"::: ) ))) "holds" (Bool (Set (Set (Var "f1")) ($#k3_valued_1 :::"+"::: ) (Set (Var "f2"))) "is" ($#v7_limfunc1 :::"divergent_in-infty_to+infty"::: ) )) ; theorem :: LIMFUNC1:57 (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f1")) "is" ($#v7_limfunc1 :::"divergent_in-infty_to+infty"::: ) ) & (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "g")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f1")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "f2")) ")" ))) ")" )) ")" ) & (Bool "ex" (Set (Var "r")) "," (Set (Var "r1")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool "(" "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f2")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k10_prob_1 :::"left_open_halfline"::: ) (Set (Var "r1")) ")" )))) "holds" (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "f2")) ($#k1_seq_1 :::"."::: ) (Set (Var "g")))) ")" ) ")" ))) "holds" (Bool (Set (Set (Var "f1")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "f2"))) "is" ($#v7_limfunc1 :::"divergent_in-infty_to+infty"::: ) )) ; theorem :: LIMFUNC1:58 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "f")) "is" ($#v4_limfunc1 :::"divergent_in+infty_to+infty"::: ) ) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f"))) "is" ($#v4_limfunc1 :::"divergent_in+infty_to+infty"::: ) ) ")" & "(" (Bool (Bool (Set (Var "f")) "is" ($#v4_limfunc1 :::"divergent_in+infty_to+infty"::: ) ) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f"))) "is" ($#v5_limfunc1 :::"divergent_in+infty_to-infty"::: ) ) ")" & "(" (Bool (Bool (Set (Var "f")) "is" ($#v5_limfunc1 :::"divergent_in+infty_to-infty"::: ) ) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f"))) "is" ($#v5_limfunc1 :::"divergent_in+infty_to-infty"::: ) ) ")" & "(" (Bool (Bool (Set (Var "f")) "is" ($#v5_limfunc1 :::"divergent_in+infty_to-infty"::: ) ) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f"))) "is" ($#v4_limfunc1 :::"divergent_in+infty_to+infty"::: ) ) ")" ")" ))) ; theorem :: LIMFUNC1:59 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "f")) "is" ($#v7_limfunc1 :::"divergent_in-infty_to+infty"::: ) ) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f"))) "is" ($#v7_limfunc1 :::"divergent_in-infty_to+infty"::: ) ) ")" & "(" (Bool (Bool (Set (Var "f")) "is" ($#v7_limfunc1 :::"divergent_in-infty_to+infty"::: ) ) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f"))) "is" ($#v8_limfunc1 :::"divergent_in-infty_to-infty"::: ) ) ")" & "(" (Bool (Bool (Set (Var "f")) "is" ($#v8_limfunc1 :::"divergent_in-infty_to-infty"::: ) ) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f"))) "is" ($#v8_limfunc1 :::"divergent_in-infty_to-infty"::: ) ) ")" & "(" (Bool (Bool (Set (Var "f")) "is" ($#v8_limfunc1 :::"divergent_in-infty_to-infty"::: ) ) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f"))) "is" ($#v7_limfunc1 :::"divergent_in-infty_to+infty"::: ) ) ")" ")" ))) ; theorem :: LIMFUNC1:60 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool "(" (Bool (Set (Var "f")) "is" ($#v4_limfunc1 :::"divergent_in+infty_to+infty"::: ) ) "or" (Bool (Set (Var "f")) "is" ($#v5_limfunc1 :::"divergent_in+infty_to-infty"::: ) ) ")" )) "holds" (Bool (Set ($#k56_valued_1 :::"abs"::: ) (Set (Var "f"))) "is" ($#v4_limfunc1 :::"divergent_in+infty_to+infty"::: ) )) ; theorem :: LIMFUNC1:61 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool "(" (Bool (Set (Var "f")) "is" ($#v7_limfunc1 :::"divergent_in-infty_to+infty"::: ) ) "or" (Bool (Set (Var "f")) "is" ($#v8_limfunc1 :::"divergent_in-infty_to-infty"::: ) ) ")" )) "holds" (Bool (Set ($#k56_valued_1 :::"abs"::: ) (Set (Var "f"))) "is" ($#v7_limfunc1 :::"divergent_in-infty_to+infty"::: ) )) ; theorem :: LIMFUNC1:62 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set "(" ($#k3_limfunc1 :::"right_open_halfline"::: ) (Set (Var "r")) ")" )) "is" ($#v7_valued_0 :::"non-decreasing"::: ) ) & (Bool (Bool "not" (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set "(" ($#k3_limfunc1 :::"right_open_halfline"::: ) (Set (Var "r")) ")" )) "is" ($#v1_seq_2 :::"bounded_above"::: ) )) ")" )) & (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "g"))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) ")" )) ")" )) "holds" (Bool (Set (Var "f")) "is" ($#v4_limfunc1 :::"divergent_in+infty_to+infty"::: ) )) ; theorem :: LIMFUNC1:63 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set "(" ($#k3_limfunc1 :::"right_open_halfline"::: ) (Set (Var "r")) ")" )) "is" ($#v5_valued_0 :::"increasing"::: ) ) & (Bool (Bool "not" (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set "(" ($#k3_limfunc1 :::"right_open_halfline"::: ) (Set (Var "r")) ")" )) "is" ($#v1_seq_2 :::"bounded_above"::: ) )) ")" )) & (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "g"))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) ")" )) ")" )) "holds" (Bool (Set (Var "f")) "is" ($#v4_limfunc1 :::"divergent_in+infty_to+infty"::: ) )) ; theorem :: LIMFUNC1:64 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set "(" ($#k3_limfunc1 :::"right_open_halfline"::: ) (Set (Var "r")) ")" )) "is" ($#v8_valued_0 :::"non-increasing"::: ) ) & (Bool (Bool "not" (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set "(" ($#k3_limfunc1 :::"right_open_halfline"::: ) (Set (Var "r")) ")" )) "is" ($#v2_seq_2 :::"bounded_below"::: ) )) ")" )) & (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "g"))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) ")" )) ")" )) "holds" (Bool (Set (Var "f")) "is" ($#v5_limfunc1 :::"divergent_in+infty_to-infty"::: ) )) ; theorem :: LIMFUNC1:65 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set "(" ($#k3_limfunc1 :::"right_open_halfline"::: ) (Set (Var "r")) ")" )) "is" ($#v6_valued_0 :::"decreasing"::: ) ) & (Bool (Bool "not" (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set "(" ($#k3_limfunc1 :::"right_open_halfline"::: ) (Set (Var "r")) ")" )) "is" ($#v2_seq_2 :::"bounded_below"::: ) )) ")" )) & (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "g"))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) ")" )) ")" )) "holds" (Bool (Set (Var "f")) "is" ($#v5_limfunc1 :::"divergent_in+infty_to-infty"::: ) )) ; theorem :: LIMFUNC1:66 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set "(" ($#k10_prob_1 :::"left_open_halfline"::: ) (Set (Var "r")) ")" )) "is" ($#v8_valued_0 :::"non-increasing"::: ) ) & (Bool (Bool "not" (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set "(" ($#k10_prob_1 :::"left_open_halfline"::: ) (Set (Var "r")) ")" )) "is" ($#v1_seq_2 :::"bounded_above"::: ) )) ")" )) & (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "g")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) ")" )) ")" )) "holds" (Bool (Set (Var "f")) "is" ($#v7_limfunc1 :::"divergent_in-infty_to+infty"::: ) )) ; theorem :: LIMFUNC1:67 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set "(" ($#k10_prob_1 :::"left_open_halfline"::: ) (Set (Var "r")) ")" )) "is" ($#v6_valued_0 :::"decreasing"::: ) ) & (Bool (Bool "not" (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set "(" ($#k10_prob_1 :::"left_open_halfline"::: ) (Set (Var "r")) ")" )) "is" ($#v1_seq_2 :::"bounded_above"::: ) )) ")" )) & (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "g")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) ")" )) ")" )) "holds" (Bool (Set (Var "f")) "is" ($#v7_limfunc1 :::"divergent_in-infty_to+infty"::: ) )) ; theorem :: LIMFUNC1:68 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set "(" ($#k10_prob_1 :::"left_open_halfline"::: ) (Set (Var "r")) ")" )) "is" ($#v7_valued_0 :::"non-decreasing"::: ) ) & (Bool (Bool "not" (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set "(" ($#k10_prob_1 :::"left_open_halfline"::: ) (Set (Var "r")) ")" )) "is" ($#v2_seq_2 :::"bounded_below"::: ) )) ")" )) & (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "g")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) ")" )) ")" )) "holds" (Bool (Set (Var "f")) "is" ($#v8_limfunc1 :::"divergent_in-infty_to-infty"::: ) )) ; theorem :: LIMFUNC1:69 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set "(" ($#k10_prob_1 :::"left_open_halfline"::: ) (Set (Var "r")) ")" )) "is" ($#v5_valued_0 :::"increasing"::: ) ) & (Bool (Bool "not" (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set "(" ($#k10_prob_1 :::"left_open_halfline"::: ) (Set (Var "r")) ")" )) "is" ($#v2_seq_2 :::"bounded_below"::: ) )) ")" )) & (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "g")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) ")" )) ")" )) "holds" (Bool (Set (Var "f")) "is" ($#v8_limfunc1 :::"divergent_in-infty_to-infty"::: ) )) ; theorem :: LIMFUNC1:70 (Bool "for" (Set (Var "f1")) "," (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f1")) "is" ($#v4_limfunc1 :::"divergent_in+infty_to+infty"::: ) ) & (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "g"))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) ")" )) ")" ) & (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k3_limfunc1 :::"right_open_halfline"::: ) (Set (Var "r")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f1")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k3_limfunc1 :::"right_open_halfline"::: ) (Set (Var "r")) ")" ))) & (Bool "(" "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k3_limfunc1 :::"right_open_halfline"::: ) (Set (Var "r")) ")" )))) "holds" (Bool (Set (Set (Var "f1")) ($#k1_seq_1 :::"."::: ) (Set (Var "g"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "g")))) ")" ) ")" ))) "holds" (Bool (Set (Var "f")) "is" ($#v4_limfunc1 :::"divergent_in+infty_to+infty"::: ) )) ; theorem :: LIMFUNC1:71 (Bool "for" (Set (Var "f1")) "," (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f1")) "is" ($#v5_limfunc1 :::"divergent_in+infty_to-infty"::: ) ) & (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "g"))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) ")" )) ")" ) & (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k3_limfunc1 :::"right_open_halfline"::: ) (Set (Var "r")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f1")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k3_limfunc1 :::"right_open_halfline"::: ) (Set (Var "r")) ")" ))) & (Bool "(" "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k3_limfunc1 :::"right_open_halfline"::: ) (Set (Var "r")) ")" )))) "holds" (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "g"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "f1")) ($#k1_seq_1 :::"."::: ) (Set (Var "g")))) ")" ) ")" ))) "holds" (Bool (Set (Var "f")) "is" ($#v5_limfunc1 :::"divergent_in+infty_to-infty"::: ) )) ; theorem :: LIMFUNC1:72 (Bool "for" (Set (Var "f1")) "," (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f1")) "is" ($#v7_limfunc1 :::"divergent_in-infty_to+infty"::: ) ) & (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "g")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) ")" )) ")" ) & (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k10_prob_1 :::"left_open_halfline"::: ) (Set (Var "r")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f1")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k10_prob_1 :::"left_open_halfline"::: ) (Set (Var "r")) ")" ))) & (Bool "(" "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k10_prob_1 :::"left_open_halfline"::: ) (Set (Var "r")) ")" )))) "holds" (Bool (Set (Set (Var "f1")) ($#k1_seq_1 :::"."::: ) (Set (Var "g"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "g")))) ")" ) ")" ))) "holds" (Bool (Set (Var "f")) "is" ($#v7_limfunc1 :::"divergent_in-infty_to+infty"::: ) )) ; theorem :: LIMFUNC1:73 (Bool "for" (Set (Var "f1")) "," (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f1")) "is" ($#v8_limfunc1 :::"divergent_in-infty_to-infty"::: ) ) & (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "g")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) ")" )) ")" ) & (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k10_prob_1 :::"left_open_halfline"::: ) (Set (Var "r")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f1")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k10_prob_1 :::"left_open_halfline"::: ) (Set (Var "r")) ")" ))) & (Bool "(" "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k10_prob_1 :::"left_open_halfline"::: ) (Set (Var "r")) ")" )))) "holds" (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "g"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "f1")) ($#k1_seq_1 :::"."::: ) (Set (Var "g")))) ")" ) ")" ))) "holds" (Bool (Set (Var "f")) "is" ($#v8_limfunc1 :::"divergent_in-infty_to-infty"::: ) )) ; theorem :: LIMFUNC1:74 (Bool "for" (Set (Var "f1")) "," (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f1")) "is" ($#v4_limfunc1 :::"divergent_in+infty_to+infty"::: ) ) & (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set ($#k3_limfunc1 :::"right_open_halfline"::: ) (Set (Var "r"))) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f1")) ")" ))) & (Bool "(" "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k3_limfunc1 :::"right_open_halfline"::: ) (Set (Var "r"))))) "holds" (Bool (Set (Set (Var "f1")) ($#k1_seq_1 :::"."::: ) (Set (Var "g"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "g")))) ")" ) ")" ))) "holds" (Bool (Set (Var "f")) "is" ($#v4_limfunc1 :::"divergent_in+infty_to+infty"::: ) )) ; theorem :: LIMFUNC1:75 (Bool "for" (Set (Var "f1")) "," (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f1")) "is" ($#v5_limfunc1 :::"divergent_in+infty_to-infty"::: ) ) & (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set ($#k3_limfunc1 :::"right_open_halfline"::: ) (Set (Var "r"))) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f1")) ")" ))) & (Bool "(" "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k3_limfunc1 :::"right_open_halfline"::: ) (Set (Var "r"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "g"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "f1")) ($#k1_seq_1 :::"."::: ) (Set (Var "g")))) ")" ) ")" ))) "holds" (Bool (Set (Var "f")) "is" ($#v5_limfunc1 :::"divergent_in+infty_to-infty"::: ) )) ; theorem :: LIMFUNC1:76 (Bool "for" (Set (Var "f1")) "," (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f1")) "is" ($#v7_limfunc1 :::"divergent_in-infty_to+infty"::: ) ) & (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set ($#k10_prob_1 :::"left_open_halfline"::: ) (Set (Var "r"))) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f1")) ")" ))) & (Bool "(" "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k10_prob_1 :::"left_open_halfline"::: ) (Set (Var "r"))))) "holds" (Bool (Set (Set (Var "f1")) ($#k1_seq_1 :::"."::: ) (Set (Var "g"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "g")))) ")" ) ")" ))) "holds" (Bool (Set (Var "f")) "is" ($#v7_limfunc1 :::"divergent_in-infty_to+infty"::: ) )) ; theorem :: LIMFUNC1:77 (Bool "for" (Set (Var "f1")) "," (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f1")) "is" ($#v8_limfunc1 :::"divergent_in-infty_to-infty"::: ) ) & (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set ($#k10_prob_1 :::"left_open_halfline"::: ) (Set (Var "r"))) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f1")) ")" ))) & (Bool "(" "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k10_prob_1 :::"left_open_halfline"::: ) (Set (Var "r"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "g"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "f1")) ($#k1_seq_1 :::"."::: ) (Set (Var "g")))) ")" ) ")" ))) "holds" (Bool (Set (Var "f")) "is" ($#v8_limfunc1 :::"divergent_in-infty_to-infty"::: ) )) ; definitionlet "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ); assume (Bool (Set (Const "f")) "is" ($#v3_limfunc1 :::"convergent_in+infty"::: ) ) ; func :::"lim_in+infty"::: "f" -> ($#m1_subset_1 :::"Real":::) means :: LIMFUNC1:def 12 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v1_limfunc1 :::"divergent_to+infty"::: ) ) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "seq"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) "f"))) "holds" (Bool "(" (Bool (Set "f" ($#k8_funct_2 :::"/*"::: ) (Set (Var "seq"))) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set "(" "f" ($#k8_funct_2 :::"/*"::: ) (Set (Var "seq")) ")" )) ($#r1_hidden :::"="::: ) it) ")" )); end; :: deftheorem defines :::"lim_in+infty"::: LIMFUNC1:def 12 : (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) "is" ($#v3_limfunc1 :::"convergent_in+infty"::: ) )) "holds" (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k4_limfunc1 :::"lim_in+infty"::: ) (Set (Var "f")))) "iff" (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v1_limfunc1 :::"divergent_to+infty"::: ) ) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "seq"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k8_funct_2 :::"/*"::: ) (Set (Var "seq"))) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set "(" (Set (Var "f")) ($#k8_funct_2 :::"/*"::: ) (Set (Var "seq")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "b2"))) ")" )) ")" ))); definitionlet "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ); assume (Bool (Set (Const "f")) "is" ($#v6_limfunc1 :::"convergent_in-infty"::: ) ) ; func :::"lim_in-infty"::: "f" -> ($#m1_subset_1 :::"Real":::) means :: LIMFUNC1:def 13 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v2_limfunc1 :::"divergent_to-infty"::: ) ) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "seq"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) "f"))) "holds" (Bool "(" (Bool (Set "f" ($#k8_funct_2 :::"/*"::: ) (Set (Var "seq"))) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set "(" "f" ($#k8_funct_2 :::"/*"::: ) (Set (Var "seq")) ")" )) ($#r1_hidden :::"="::: ) it) ")" )); end; :: deftheorem defines :::"lim_in-infty"::: LIMFUNC1:def 13 : (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) "is" ($#v6_limfunc1 :::"convergent_in-infty"::: ) )) "holds" (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k5_limfunc1 :::"lim_in-infty"::: ) (Set (Var "f")))) "iff" (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v2_limfunc1 :::"divergent_to-infty"::: ) ) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "seq"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k8_funct_2 :::"/*"::: ) (Set (Var "seq"))) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set "(" (Set (Var "f")) ($#k8_funct_2 :::"/*"::: ) (Set (Var "seq")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "b2"))) ")" )) ")" ))); theorem :: LIMFUNC1:78 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "f")) "is" ($#v6_limfunc1 :::"convergent_in-infty"::: ) )) "holds" (Bool "(" (Bool (Set ($#k5_limfunc1 :::"lim_in-infty"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "g"))) "iff" (Bool "for" (Set (Var "g1")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "g1")))) "holds" (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "for" (Set (Var "r1")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "r1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set (Var "r1")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set "(" (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "r1")) ")" ) ($#k9_real_1 :::"-"::: ) (Set (Var "g")) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "g1")))))) ")" ))) ; theorem :: LIMFUNC1:79 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "f")) "is" ($#v3_limfunc1 :::"convergent_in+infty"::: ) )) "holds" (Bool "(" (Bool (Set ($#k4_limfunc1 :::"lim_in+infty"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "g"))) "iff" (Bool "for" (Set (Var "g1")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "g1")))) "holds" (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "for" (Set (Var "r1")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r1"))) & (Bool (Set (Var "r1")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set "(" (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "r1")) ")" ) ($#k9_real_1 :::"-"::: ) (Set (Var "g")) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "g1")))))) ")" ))) ; theorem :: LIMFUNC1:80 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "f")) "is" ($#v3_limfunc1 :::"convergent_in+infty"::: ) )) "holds" (Bool "(" (Bool (Set (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f"))) "is" ($#v3_limfunc1 :::"convergent_in+infty"::: ) ) & (Bool (Set ($#k4_limfunc1 :::"lim_in+infty"::: ) (Set "(" (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k4_limfunc1 :::"lim_in+infty"::: ) (Set (Var "f")) ")" ))) ")" ))) ; theorem :: LIMFUNC1:81 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) "is" ($#v3_limfunc1 :::"convergent_in+infty"::: ) )) "holds" (Bool "(" (Bool (Set ($#k32_valued_1 :::"-"::: ) (Set (Var "f"))) "is" ($#v3_limfunc1 :::"convergent_in+infty"::: ) ) & (Bool (Set ($#k4_limfunc1 :::"lim_in+infty"::: ) (Set "(" ($#k32_valued_1 :::"-"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" ($#k4_limfunc1 :::"lim_in+infty"::: ) (Set (Var "f")) ")" ))) ")" )) ; theorem :: LIMFUNC1:82 (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f1")) "is" ($#v3_limfunc1 :::"convergent_in+infty"::: ) ) & (Bool (Set (Var "f2")) "is" ($#v3_limfunc1 :::"convergent_in+infty"::: ) ) & (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "g"))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f1")) ($#k3_valued_1 :::"+"::: ) (Set (Var "f2")) ")" ))) ")" )) ")" )) "holds" (Bool "(" (Bool (Set (Set (Var "f1")) ($#k3_valued_1 :::"+"::: ) (Set (Var "f2"))) "is" ($#v3_limfunc1 :::"convergent_in+infty"::: ) ) & (Bool (Set ($#k4_limfunc1 :::"lim_in+infty"::: ) (Set "(" (Set (Var "f1")) ($#k3_valued_1 :::"+"::: ) (Set (Var "f2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_limfunc1 :::"lim_in+infty"::: ) (Set (Var "f1")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k4_limfunc1 :::"lim_in+infty"::: ) (Set (Var "f2")) ")" ))) ")" )) ; theorem :: LIMFUNC1:83 (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f1")) "is" ($#v3_limfunc1 :::"convergent_in+infty"::: ) ) & (Bool (Set (Var "f2")) "is" ($#v3_limfunc1 :::"convergent_in+infty"::: ) ) & (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "g"))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f1")) ($#k47_valued_1 :::"-"::: ) (Set (Var "f2")) ")" ))) ")" )) ")" )) "holds" (Bool "(" (Bool (Set (Set (Var "f1")) ($#k47_valued_1 :::"-"::: ) (Set (Var "f2"))) "is" ($#v3_limfunc1 :::"convergent_in+infty"::: ) ) & (Bool (Set ($#k4_limfunc1 :::"lim_in+infty"::: ) (Set "(" (Set (Var "f1")) ($#k47_valued_1 :::"-"::: ) (Set (Var "f2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_limfunc1 :::"lim_in+infty"::: ) (Set (Var "f1")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k4_limfunc1 :::"lim_in+infty"::: ) (Set (Var "f2")) ")" ))) ")" )) ; theorem :: LIMFUNC1:84 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) "is" ($#v3_limfunc1 :::"convergent_in+infty"::: ) ) & (Bool (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k4_limfunc1 :::"lim_in+infty"::: ) (Set (Var "f"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k6_rfunct_1 :::"^"::: ) ) "is" ($#v3_limfunc1 :::"convergent_in+infty"::: ) ) & (Bool (Set ($#k4_limfunc1 :::"lim_in+infty"::: ) (Set "(" (Set (Var "f")) ($#k6_rfunct_1 :::"^"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_limfunc1 :::"lim_in+infty"::: ) (Set (Var "f")) ")" ) ($#k2_real_1 :::"""::: ) )) ")" )) ; theorem :: LIMFUNC1:85 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) "is" ($#v3_limfunc1 :::"convergent_in+infty"::: ) )) "holds" (Bool "(" (Bool (Set ($#k56_valued_1 :::"abs"::: ) (Set (Var "f"))) "is" ($#v3_limfunc1 :::"convergent_in+infty"::: ) ) & (Bool (Set ($#k4_limfunc1 :::"lim_in+infty"::: ) (Set "(" ($#k56_valued_1 :::"abs"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k18_complex1 :::"abs"::: ) (Set "(" ($#k4_limfunc1 :::"lim_in+infty"::: ) (Set (Var "f")) ")" ))) ")" )) ; theorem :: LIMFUNC1:86 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) "is" ($#v3_limfunc1 :::"convergent_in+infty"::: ) ) & (Bool (Set ($#k4_limfunc1 :::"lim_in+infty"::: ) (Set (Var "f"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "g"))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "g"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) ")" )) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k6_rfunct_1 :::"^"::: ) ) "is" ($#v3_limfunc1 :::"convergent_in+infty"::: ) ) & (Bool (Set ($#k4_limfunc1 :::"lim_in+infty"::: ) (Set "(" (Set (Var "f")) ($#k6_rfunct_1 :::"^"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_limfunc1 :::"lim_in+infty"::: ) (Set (Var "f")) ")" ) ($#k2_real_1 :::"""::: ) )) ")" )) ; theorem :: LIMFUNC1:87 (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f1")) "is" ($#v3_limfunc1 :::"convergent_in+infty"::: ) ) & (Bool (Set (Var "f2")) "is" ($#v3_limfunc1 :::"convergent_in+infty"::: ) ) & (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "g"))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f1")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "f2")) ")" ))) ")" )) ")" )) "holds" (Bool "(" (Bool (Set (Set (Var "f1")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "f2"))) "is" ($#v3_limfunc1 :::"convergent_in+infty"::: ) ) & (Bool (Set ($#k4_limfunc1 :::"lim_in+infty"::: ) (Set "(" (Set (Var "f1")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "f2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_limfunc1 :::"lim_in+infty"::: ) (Set (Var "f1")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k4_limfunc1 :::"lim_in+infty"::: ) (Set (Var "f2")) ")" ))) ")" )) ; theorem :: LIMFUNC1:88 (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f1")) "is" ($#v3_limfunc1 :::"convergent_in+infty"::: ) ) & (Bool (Set (Var "f2")) "is" ($#v3_limfunc1 :::"convergent_in+infty"::: ) ) & (Bool (Set ($#k4_limfunc1 :::"lim_in+infty"::: ) (Set (Var "f2"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "g"))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f1")) ($#k3_rfunct_1 :::"/"::: ) (Set (Var "f2")) ")" ))) ")" )) ")" )) "holds" (Bool "(" (Bool (Set (Set (Var "f1")) ($#k3_rfunct_1 :::"/"::: ) (Set (Var "f2"))) "is" ($#v3_limfunc1 :::"convergent_in+infty"::: ) ) & (Bool (Set ($#k4_limfunc1 :::"lim_in+infty"::: ) (Set "(" (Set (Var "f1")) ($#k3_rfunct_1 :::"/"::: ) (Set (Var "f2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_limfunc1 :::"lim_in+infty"::: ) (Set (Var "f1")) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" ($#k4_limfunc1 :::"lim_in+infty"::: ) (Set (Var "f2")) ")" ))) ")" )) ; theorem :: LIMFUNC1:89 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "f")) "is" ($#v6_limfunc1 :::"convergent_in-infty"::: ) )) "holds" (Bool "(" (Bool (Set (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f"))) "is" ($#v6_limfunc1 :::"convergent_in-infty"::: ) ) & (Bool (Set ($#k5_limfunc1 :::"lim_in-infty"::: ) (Set "(" (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k5_limfunc1 :::"lim_in-infty"::: ) (Set (Var "f")) ")" ))) ")" ))) ; theorem :: LIMFUNC1:90 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) "is" ($#v6_limfunc1 :::"convergent_in-infty"::: ) )) "holds" (Bool "(" (Bool (Set ($#k32_valued_1 :::"-"::: ) (Set (Var "f"))) "is" ($#v6_limfunc1 :::"convergent_in-infty"::: ) ) & (Bool (Set ($#k5_limfunc1 :::"lim_in-infty"::: ) (Set "(" ($#k32_valued_1 :::"-"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" ($#k5_limfunc1 :::"lim_in-infty"::: ) (Set (Var "f")) ")" ))) ")" )) ; theorem :: LIMFUNC1:91 (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f1")) "is" ($#v6_limfunc1 :::"convergent_in-infty"::: ) ) & (Bool (Set (Var "f2")) "is" ($#v6_limfunc1 :::"convergent_in-infty"::: ) ) & (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "g")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f1")) ($#k3_valued_1 :::"+"::: ) (Set (Var "f2")) ")" ))) ")" )) ")" )) "holds" (Bool "(" (Bool (Set (Set (Var "f1")) ($#k3_valued_1 :::"+"::: ) (Set (Var "f2"))) "is" ($#v6_limfunc1 :::"convergent_in-infty"::: ) ) & (Bool (Set ($#k5_limfunc1 :::"lim_in-infty"::: ) (Set "(" (Set (Var "f1")) ($#k3_valued_1 :::"+"::: ) (Set (Var "f2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_limfunc1 :::"lim_in-infty"::: ) (Set (Var "f1")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k5_limfunc1 :::"lim_in-infty"::: ) (Set (Var "f2")) ")" ))) ")" )) ; theorem :: LIMFUNC1:92 (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f1")) "is" ($#v6_limfunc1 :::"convergent_in-infty"::: ) ) & (Bool (Set (Var "f2")) "is" ($#v6_limfunc1 :::"convergent_in-infty"::: ) ) & (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "g")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f1")) ($#k47_valued_1 :::"-"::: ) (Set (Var "f2")) ")" ))) ")" )) ")" )) "holds" (Bool "(" (Bool (Set (Set (Var "f1")) ($#k47_valued_1 :::"-"::: ) (Set (Var "f2"))) "is" ($#v6_limfunc1 :::"convergent_in-infty"::: ) ) & (Bool (Set ($#k5_limfunc1 :::"lim_in-infty"::: ) (Set "(" (Set (Var "f1")) ($#k47_valued_1 :::"-"::: ) (Set (Var "f2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_limfunc1 :::"lim_in-infty"::: ) (Set (Var "f1")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k5_limfunc1 :::"lim_in-infty"::: ) (Set (Var "f2")) ")" ))) ")" )) ; theorem :: LIMFUNC1:93 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) "is" ($#v6_limfunc1 :::"convergent_in-infty"::: ) ) & (Bool (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k5_limfunc1 :::"lim_in-infty"::: ) (Set (Var "f"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k6_rfunct_1 :::"^"::: ) ) "is" ($#v6_limfunc1 :::"convergent_in-infty"::: ) ) & (Bool (Set ($#k5_limfunc1 :::"lim_in-infty"::: ) (Set "(" (Set (Var "f")) ($#k6_rfunct_1 :::"^"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_limfunc1 :::"lim_in-infty"::: ) (Set (Var "f")) ")" ) ($#k2_real_1 :::"""::: ) )) ")" )) ; theorem :: LIMFUNC1:94 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) "is" ($#v6_limfunc1 :::"convergent_in-infty"::: ) )) "holds" (Bool "(" (Bool (Set ($#k56_valued_1 :::"abs"::: ) (Set (Var "f"))) "is" ($#v6_limfunc1 :::"convergent_in-infty"::: ) ) & (Bool (Set ($#k5_limfunc1 :::"lim_in-infty"::: ) (Set "(" ($#k56_valued_1 :::"abs"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k18_complex1 :::"abs"::: ) (Set "(" ($#k5_limfunc1 :::"lim_in-infty"::: ) (Set (Var "f")) ")" ))) ")" )) ; theorem :: LIMFUNC1:95 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) "is" ($#v6_limfunc1 :::"convergent_in-infty"::: ) ) & (Bool (Set ($#k5_limfunc1 :::"lim_in-infty"::: ) (Set (Var "f"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "g")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "g"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) ")" )) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k6_rfunct_1 :::"^"::: ) ) "is" ($#v6_limfunc1 :::"convergent_in-infty"::: ) ) & (Bool (Set ($#k5_limfunc1 :::"lim_in-infty"::: ) (Set "(" (Set (Var "f")) ($#k6_rfunct_1 :::"^"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_limfunc1 :::"lim_in-infty"::: ) (Set (Var "f")) ")" ) ($#k2_real_1 :::"""::: ) )) ")" )) ; theorem :: LIMFUNC1:96 (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f1")) "is" ($#v6_limfunc1 :::"convergent_in-infty"::: ) ) & (Bool (Set (Var "f2")) "is" ($#v6_limfunc1 :::"convergent_in-infty"::: ) ) & (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "g")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f1")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "f2")) ")" ))) ")" )) ")" )) "holds" (Bool "(" (Bool (Set (Set (Var "f1")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "f2"))) "is" ($#v6_limfunc1 :::"convergent_in-infty"::: ) ) & (Bool (Set ($#k5_limfunc1 :::"lim_in-infty"::: ) (Set "(" (Set (Var "f1")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "f2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_limfunc1 :::"lim_in-infty"::: ) (Set (Var "f1")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k5_limfunc1 :::"lim_in-infty"::: ) (Set (Var "f2")) ")" ))) ")" )) ; theorem :: LIMFUNC1:97 (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f1")) "is" ($#v6_limfunc1 :::"convergent_in-infty"::: ) ) & (Bool (Set (Var "f2")) "is" ($#v6_limfunc1 :::"convergent_in-infty"::: ) ) & (Bool (Set ($#k5_limfunc1 :::"lim_in-infty"::: ) (Set (Var "f2"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "g")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f1")) ($#k3_rfunct_1 :::"/"::: ) (Set (Var "f2")) ")" ))) ")" )) ")" )) "holds" (Bool "(" (Bool (Set (Set (Var "f1")) ($#k3_rfunct_1 :::"/"::: ) (Set (Var "f2"))) "is" ($#v6_limfunc1 :::"convergent_in-infty"::: ) ) & (Bool (Set ($#k5_limfunc1 :::"lim_in-infty"::: ) (Set "(" (Set (Var "f1")) ($#k3_rfunct_1 :::"/"::: ) (Set (Var "f2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_limfunc1 :::"lim_in-infty"::: ) (Set (Var "f1")) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" ($#k5_limfunc1 :::"lim_in-infty"::: ) (Set (Var "f2")) ")" ))) ")" )) ; theorem :: LIMFUNC1:98 (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f1")) "is" ($#v3_limfunc1 :::"convergent_in+infty"::: ) ) & (Bool (Set ($#k4_limfunc1 :::"lim_in+infty"::: ) (Set (Var "f1"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "g"))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f1")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "f2")) ")" ))) ")" )) ")" ) & (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Set (Set (Var "f2")) ($#k2_partfun1 :::"|"::: ) (Set "(" ($#k3_limfunc1 :::"right_open_halfline"::: ) (Set (Var "r")) ")" )) "is" ($#v1_comseq_2 :::"bounded"::: ) ))) "holds" (Bool "(" (Bool (Set (Set (Var "f1")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "f2"))) "is" ($#v3_limfunc1 :::"convergent_in+infty"::: ) ) & (Bool (Set ($#k4_limfunc1 :::"lim_in+infty"::: ) (Set "(" (Set (Var "f1")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "f2")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) ; theorem :: LIMFUNC1:99 (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f1")) "is" ($#v6_limfunc1 :::"convergent_in-infty"::: ) ) & (Bool (Set ($#k5_limfunc1 :::"lim_in-infty"::: ) (Set (Var "f1"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "g")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f1")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "f2")) ")" ))) ")" )) ")" ) & (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Set (Set (Var "f2")) ($#k2_partfun1 :::"|"::: ) (Set "(" ($#k10_prob_1 :::"left_open_halfline"::: ) (Set (Var "r")) ")" )) "is" ($#v1_comseq_2 :::"bounded"::: ) ))) "holds" (Bool "(" (Bool (Set (Set (Var "f1")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "f2"))) "is" ($#v6_limfunc1 :::"convergent_in-infty"::: ) ) & (Bool (Set ($#k5_limfunc1 :::"lim_in-infty"::: ) (Set "(" (Set (Var "f1")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "f2")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) ; theorem :: LIMFUNC1:100 (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f1")) "is" ($#v3_limfunc1 :::"convergent_in+infty"::: ) ) & (Bool (Set (Var "f2")) "is" ($#v3_limfunc1 :::"convergent_in+infty"::: ) ) & (Bool (Set ($#k4_limfunc1 :::"lim_in+infty"::: ) (Set (Var "f1"))) ($#r1_hidden :::"="::: ) (Set ($#k4_limfunc1 :::"lim_in+infty"::: ) (Set (Var "f2")))) & (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "g"))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) ")" )) ")" ) & (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool "(" (Bool "(" (Bool (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f1")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k3_limfunc1 :::"right_open_halfline"::: ) (Set (Var "r")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f2")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k3_limfunc1 :::"right_open_halfline"::: ) (Set (Var "r")) ")" ))) & (Bool (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k3_limfunc1 :::"right_open_halfline"::: ) (Set (Var "r")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f1")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k3_limfunc1 :::"right_open_halfline"::: ) (Set (Var "r")) ")" ))) ")" ) "or" (Bool "(" (Bool (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f2")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k3_limfunc1 :::"right_open_halfline"::: ) (Set (Var "r")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f1")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k3_limfunc1 :::"right_open_halfline"::: ) (Set (Var "r")) ")" ))) & (Bool (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k3_limfunc1 :::"right_open_halfline"::: ) (Set (Var "r")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f2")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k3_limfunc1 :::"right_open_halfline"::: ) (Set (Var "r")) ")" ))) ")" ) ")" ) & (Bool "(" "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k3_limfunc1 :::"right_open_halfline"::: ) (Set (Var "r")) ")" )))) "holds" (Bool "(" (Bool (Set (Set (Var "f1")) ($#k1_seq_1 :::"."::: ) (Set (Var "g"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "g")))) & (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "g"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "f2")) ($#k1_seq_1 :::"."::: ) (Set (Var "g")))) ")" ) ")" ) ")" ))) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v3_limfunc1 :::"convergent_in+infty"::: ) ) & (Bool (Set ($#k4_limfunc1 :::"lim_in+infty"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k4_limfunc1 :::"lim_in+infty"::: ) (Set (Var "f1")))) ")" )) ; theorem :: LIMFUNC1:101 (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f1")) "is" ($#v3_limfunc1 :::"convergent_in+infty"::: ) ) & (Bool (Set (Var "f2")) "is" ($#v3_limfunc1 :::"convergent_in+infty"::: ) ) & (Bool (Set ($#k4_limfunc1 :::"lim_in+infty"::: ) (Set (Var "f1"))) ($#r1_hidden :::"="::: ) (Set ($#k4_limfunc1 :::"lim_in+infty"::: ) (Set (Var "f2")))) & (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set ($#k3_limfunc1 :::"right_open_halfline"::: ) (Set (Var "r"))) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f1")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f2")) ")" ) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")) ")" ))) & (Bool "(" "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k3_limfunc1 :::"right_open_halfline"::: ) (Set (Var "r"))))) "holds" (Bool "(" (Bool (Set (Set (Var "f1")) ($#k1_seq_1 :::"."::: ) (Set (Var "g"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "g")))) & (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "g"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "f2")) ($#k1_seq_1 :::"."::: ) (Set (Var "g")))) ")" ) ")" ) ")" ))) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v3_limfunc1 :::"convergent_in+infty"::: ) ) & (Bool (Set ($#k4_limfunc1 :::"lim_in+infty"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k4_limfunc1 :::"lim_in+infty"::: ) (Set (Var "f1")))) ")" )) ; theorem :: LIMFUNC1:102 (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f1")) "is" ($#v6_limfunc1 :::"convergent_in-infty"::: ) ) & (Bool (Set (Var "f2")) "is" ($#v6_limfunc1 :::"convergent_in-infty"::: ) ) & (Bool (Set ($#k5_limfunc1 :::"lim_in-infty"::: ) (Set (Var "f1"))) ($#r1_hidden :::"="::: ) (Set ($#k5_limfunc1 :::"lim_in-infty"::: ) (Set (Var "f2")))) & (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "g")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) ")" )) ")" ) & (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool "(" (Bool "(" (Bool (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f1")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k10_prob_1 :::"left_open_halfline"::: ) (Set (Var "r")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f2")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k10_prob_1 :::"left_open_halfline"::: ) (Set (Var "r")) ")" ))) & (Bool (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k10_prob_1 :::"left_open_halfline"::: ) (Set (Var "r")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f1")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k10_prob_1 :::"left_open_halfline"::: ) (Set (Var "r")) ")" ))) ")" ) "or" (Bool "(" (Bool (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f2")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k10_prob_1 :::"left_open_halfline"::: ) (Set (Var "r")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f1")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k10_prob_1 :::"left_open_halfline"::: ) (Set (Var "r")) ")" ))) & (Bool (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k10_prob_1 :::"left_open_halfline"::: ) (Set (Var "r")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f2")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k10_prob_1 :::"left_open_halfline"::: ) (Set (Var "r")) ")" ))) ")" ) ")" ) & (Bool "(" "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k10_prob_1 :::"left_open_halfline"::: ) (Set (Var "r")) ")" )))) "holds" (Bool "(" (Bool (Set (Set (Var "f1")) ($#k1_seq_1 :::"."::: ) (Set (Var "g"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "g")))) & (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "g"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "f2")) ($#k1_seq_1 :::"."::: ) (Set (Var "g")))) ")" ) ")" ) ")" ))) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v6_limfunc1 :::"convergent_in-infty"::: ) ) & (Bool (Set ($#k5_limfunc1 :::"lim_in-infty"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k5_limfunc1 :::"lim_in-infty"::: ) (Set (Var "f1")))) ")" )) ; theorem :: LIMFUNC1:103 (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f1")) "is" ($#v6_limfunc1 :::"convergent_in-infty"::: ) ) & (Bool (Set (Var "f2")) "is" ($#v6_limfunc1 :::"convergent_in-infty"::: ) ) & (Bool (Set ($#k5_limfunc1 :::"lim_in-infty"::: ) (Set (Var "f1"))) ($#r1_hidden :::"="::: ) (Set ($#k5_limfunc1 :::"lim_in-infty"::: ) (Set (Var "f2")))) & (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set ($#k10_prob_1 :::"left_open_halfline"::: ) (Set (Var "r"))) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f1")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f2")) ")" ) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")) ")" ))) & (Bool "(" "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k10_prob_1 :::"left_open_halfline"::: ) (Set (Var "r"))))) "holds" (Bool "(" (Bool (Set (Set (Var "f1")) ($#k1_seq_1 :::"."::: ) (Set (Var "g"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "g")))) & (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "g"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "f2")) ($#k1_seq_1 :::"."::: ) (Set (Var "g")))) ")" ) ")" ) ")" ))) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v6_limfunc1 :::"convergent_in-infty"::: ) ) & (Bool (Set ($#k5_limfunc1 :::"lim_in-infty"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k5_limfunc1 :::"lim_in-infty"::: ) (Set (Var "f1")))) ")" )) ; theorem :: LIMFUNC1:104 (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f1")) "is" ($#v3_limfunc1 :::"convergent_in+infty"::: ) ) & (Bool (Set (Var "f2")) "is" ($#v3_limfunc1 :::"convergent_in+infty"::: ) ) & (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool "(" (Bool (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f1")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k3_limfunc1 :::"right_open_halfline"::: ) (Set (Var "r")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f2")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k3_limfunc1 :::"right_open_halfline"::: ) (Set (Var "r")) ")" ))) & (Bool "(" "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f1")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k3_limfunc1 :::"right_open_halfline"::: ) (Set (Var "r")) ")" )))) "holds" (Bool (Set (Set (Var "f1")) ($#k1_seq_1 :::"."::: ) (Set (Var "g"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "f2")) ($#k1_seq_1 :::"."::: ) (Set (Var "g")))) ")" ) ")" ) "or" (Bool "(" (Bool (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f2")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k3_limfunc1 :::"right_open_halfline"::: ) (Set (Var "r")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f1")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k3_limfunc1 :::"right_open_halfline"::: ) (Set (Var "r")) ")" ))) & (Bool "(" "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f2")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k3_limfunc1 :::"right_open_halfline"::: ) (Set (Var "r")) ")" )))) "holds" (Bool (Set (Set (Var "f1")) ($#k1_seq_1 :::"."::: ) (Set (Var "g"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "f2")) ($#k1_seq_1 :::"."::: ) (Set (Var "g")))) ")" ) ")" ) ")" ))) "holds" (Bool (Set ($#k4_limfunc1 :::"lim_in+infty"::: ) (Set (Var "f1"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k4_limfunc1 :::"lim_in+infty"::: ) (Set (Var "f2"))))) ; theorem :: LIMFUNC1:105 (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f1")) "is" ($#v6_limfunc1 :::"convergent_in-infty"::: ) ) & (Bool (Set (Var "f2")) "is" ($#v6_limfunc1 :::"convergent_in-infty"::: ) ) & (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool "(" (Bool (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f1")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k10_prob_1 :::"left_open_halfline"::: ) (Set (Var "r")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f2")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k10_prob_1 :::"left_open_halfline"::: ) (Set (Var "r")) ")" ))) & (Bool "(" "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f1")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k10_prob_1 :::"left_open_halfline"::: ) (Set (Var "r")) ")" )))) "holds" (Bool (Set (Set (Var "f1")) ($#k1_seq_1 :::"."::: ) (Set (Var "g"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "f2")) ($#k1_seq_1 :::"."::: ) (Set (Var "g")))) ")" ) ")" ) "or" (Bool "(" (Bool (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f2")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k10_prob_1 :::"left_open_halfline"::: ) (Set (Var "r")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f1")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k10_prob_1 :::"left_open_halfline"::: ) (Set (Var "r")) ")" ))) & (Bool "(" "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f2")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k10_prob_1 :::"left_open_halfline"::: ) (Set (Var "r")) ")" )))) "holds" (Bool (Set (Set (Var "f1")) ($#k1_seq_1 :::"."::: ) (Set (Var "g"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "f2")) ($#k1_seq_1 :::"."::: ) (Set (Var "g")))) ")" ) ")" ) ")" ))) "holds" (Bool (Set ($#k5_limfunc1 :::"lim_in-infty"::: ) (Set (Var "f1"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k5_limfunc1 :::"lim_in-infty"::: ) (Set (Var "f2"))))) ; theorem :: LIMFUNC1:106 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool "(" (Bool (Set (Var "f")) "is" ($#v4_limfunc1 :::"divergent_in+infty_to+infty"::: ) ) "or" (Bool (Set (Var "f")) "is" ($#v5_limfunc1 :::"divergent_in+infty_to-infty"::: ) ) ")" ) & (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "g"))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "g"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) ")" )) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k6_rfunct_1 :::"^"::: ) ) "is" ($#v3_limfunc1 :::"convergent_in+infty"::: ) ) & (Bool (Set ($#k4_limfunc1 :::"lim_in+infty"::: ) (Set "(" (Set (Var "f")) ($#k6_rfunct_1 :::"^"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) ; theorem :: LIMFUNC1:107 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool "(" (Bool (Set (Var "f")) "is" ($#v7_limfunc1 :::"divergent_in-infty_to+infty"::: ) ) "or" (Bool (Set (Var "f")) "is" ($#v8_limfunc1 :::"divergent_in-infty_to-infty"::: ) ) ")" ) & (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "g")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "g"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) ")" )) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k6_rfunct_1 :::"^"::: ) ) "is" ($#v6_limfunc1 :::"convergent_in-infty"::: ) ) & (Bool (Set ($#k5_limfunc1 :::"lim_in-infty"::: ) (Set "(" (Set (Var "f")) ($#k6_rfunct_1 :::"^"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) ; theorem :: LIMFUNC1:108 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) "is" ($#v3_limfunc1 :::"convergent_in+infty"::: ) ) & (Bool (Set ($#k4_limfunc1 :::"lim_in+infty"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "g"))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "g"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) ")" ) & (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k3_limfunc1 :::"right_open_halfline"::: ) (Set (Var "r")) ")" )))) "holds" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "g"))))))) "holds" (Bool (Set (Set (Var "f")) ($#k6_rfunct_1 :::"^"::: ) ) "is" ($#v4_limfunc1 :::"divergent_in+infty_to+infty"::: ) )) ; theorem :: LIMFUNC1:109 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) "is" ($#v3_limfunc1 :::"convergent_in+infty"::: ) ) & (Bool (Set ($#k4_limfunc1 :::"lim_in+infty"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "g"))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "g"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) ")" ) & (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k3_limfunc1 :::"right_open_halfline"::: ) (Set (Var "r")) ")" )))) "holds" (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "g"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) ))))) "holds" (Bool (Set (Set (Var "f")) ($#k6_rfunct_1 :::"^"::: ) ) "is" ($#v5_limfunc1 :::"divergent_in+infty_to-infty"::: ) )) ; theorem :: LIMFUNC1:110 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) "is" ($#v6_limfunc1 :::"convergent_in-infty"::: ) ) & (Bool (Set ($#k5_limfunc1 :::"lim_in-infty"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "g")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "g"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) ")" ) & (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k10_prob_1 :::"left_open_halfline"::: ) (Set (Var "r")) ")" )))) "holds" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "g"))))))) "holds" (Bool (Set (Set (Var "f")) ($#k6_rfunct_1 :::"^"::: ) ) "is" ($#v7_limfunc1 :::"divergent_in-infty_to+infty"::: ) )) ; theorem :: LIMFUNC1:111 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) "is" ($#v6_limfunc1 :::"convergent_in-infty"::: ) ) & (Bool (Set ($#k5_limfunc1 :::"lim_in-infty"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "g")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "g"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) ")" ) & (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k10_prob_1 :::"left_open_halfline"::: ) (Set (Var "r")) ")" )))) "holds" (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "g"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) ))))) "holds" (Bool (Set (Set (Var "f")) ($#k6_rfunct_1 :::"^"::: ) ) "is" ($#v8_limfunc1 :::"divergent_in-infty_to-infty"::: ) )) ; theorem :: LIMFUNC1:112 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) "is" ($#v3_limfunc1 :::"convergent_in+infty"::: ) ) & (Bool (Set ($#k4_limfunc1 :::"lim_in+infty"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k3_limfunc1 :::"right_open_halfline"::: ) (Set (Var "r")) ")" )))) "holds" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "g"))))))) "holds" (Bool (Set (Set (Var "f")) ($#k6_rfunct_1 :::"^"::: ) ) "is" ($#v4_limfunc1 :::"divergent_in+infty_to+infty"::: ) )) ; theorem :: LIMFUNC1:113 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) "is" ($#v3_limfunc1 :::"convergent_in+infty"::: ) ) & (Bool (Set ($#k4_limfunc1 :::"lim_in+infty"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k3_limfunc1 :::"right_open_halfline"::: ) (Set (Var "r")) ")" )))) "holds" (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "g"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) ))))) "holds" (Bool (Set (Set (Var "f")) ($#k6_rfunct_1 :::"^"::: ) ) "is" ($#v5_limfunc1 :::"divergent_in+infty_to-infty"::: ) )) ; theorem :: LIMFUNC1:114 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) "is" ($#v6_limfunc1 :::"convergent_in-infty"::: ) ) & (Bool (Set ($#k5_limfunc1 :::"lim_in-infty"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k10_prob_1 :::"left_open_halfline"::: ) (Set (Var "r")) ")" )))) "holds" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "g"))))))) "holds" (Bool (Set (Set (Var "f")) ($#k6_rfunct_1 :::"^"::: ) ) "is" ($#v7_limfunc1 :::"divergent_in-infty_to+infty"::: ) )) ; theorem :: LIMFUNC1:115 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) "is" ($#v6_limfunc1 :::"convergent_in-infty"::: ) ) & (Bool (Set ($#k5_limfunc1 :::"lim_in-infty"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k10_prob_1 :::"left_open_halfline"::: ) (Set (Var "r")) ")" )))) "holds" (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "g"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) ))))) "holds" (Bool (Set (Set (Var "f")) ($#k6_rfunct_1 :::"^"::: ) ) "is" ($#v8_limfunc1 :::"divergent_in-infty_to-infty"::: ) )) ;