:: SEQFUNC semantic presentation begin definitionlet "D1", "D2" be ($#m1_hidden :::"set"::: ) ; mode Functional_Sequence of "D1" "," "D2" is ($#m1_subset_1 :::"sequence":::) "of" (Set "(" ($#k4_partfun1 :::"PFuncs"::: ) "(" "D1" "," "D2" ")" ")" ); end; definitionlet "D1", "D2" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Const "D1")) "," (Set (Const "D2")); let "n" be ($#m1_hidden :::"Nat":::); :: original: :::"."::: redefine func "F" :::"."::: "n" -> ($#m1_subset_1 :::"PartFunc":::) "of" "D1" "," "D2"; end; theorem :: SEQFUNC:1 (Bool "for" (Set (Var "D1")) "," (Set (Var "D2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "D1")) "," (Set (Var "D2"))) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k5_numbers :::"NAT"::: ) )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) "is" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D1")) "," (Set (Var "D2"))) ")" ) ")" ) ")" ))) ; scheme :: SEQFUNC:sch 1 ExFuncSeq{ F1() -> ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_hidden :::"set"::: ) , F3( ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"PartFunc":::) "of" (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) } : (Bool "ex" (Set (Var "G")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) "st" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "G")) ($#k1_seqfunc :::"."::: ) (Set (Var "n"))) ($#r2_relset_1 :::"="::: ) (Set F3 "(" (Set (Var "n")) ")" )))) proof end; definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "H" be ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Const "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ); let "r" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; func "r" :::"(#)"::: "H" -> ($#m1_subset_1 :::"Functional_Sequence":::) "of" "D" "," (Set ($#k1_numbers :::"REAL"::: ) ) means :: SEQFUNC:def 1 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set it ($#k1_seqfunc :::"."::: ) (Set (Var "n"))) ($#r2_relset_1 :::"="::: ) (Set "r" ($#k26_valued_1 :::"(#)"::: ) (Set "(" "H" ($#k1_seqfunc :::"."::: ) (Set (Var "n")) ")" )))); end; :: deftheorem defines :::"(#)"::: SEQFUNC:def 1 : (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k2_seqfunc :::"(#)"::: ) (Set (Var "H")))) "iff" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "b4")) ($#k1_seqfunc :::"."::: ) (Set (Var "n"))) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set "(" (Set (Var "H")) ($#k1_seqfunc :::"."::: ) (Set (Var "n")) ")" )))) ")" ))))); definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "H" be ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Const "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ); func "H" :::"""::: -> ($#m1_subset_1 :::"Functional_Sequence":::) "of" "D" "," (Set ($#k1_numbers :::"REAL"::: ) ) means :: SEQFUNC:def 2 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set it ($#k1_seqfunc :::"."::: ) (Set (Var "n"))) ($#r2_relset_1 :::"="::: ) (Set (Set "(" "H" ($#k1_seqfunc :::"."::: ) (Set (Var "n")) ")" ) ($#k6_rfunct_1 :::"^"::: ) ))); func :::"-"::: "H" -> ($#m1_subset_1 :::"Functional_Sequence":::) "of" "D" "," (Set ($#k1_numbers :::"REAL"::: ) ) means :: SEQFUNC:def 3 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set it ($#k1_seqfunc :::"."::: ) (Set (Var "n"))) ($#r2_relset_1 :::"="::: ) (Set ($#k32_valued_1 :::"-"::: ) (Set "(" "H" ($#k1_seqfunc :::"."::: ) (Set (Var "n")) ")" )))); involutiveness (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Const "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "b1")) ($#k1_seqfunc :::"."::: ) (Set (Var "n"))) ($#r2_relset_1 :::"="::: ) (Set ($#k32_valued_1 :::"-"::: ) (Set "(" (Set (Var "b2")) ($#k1_seqfunc :::"."::: ) (Set (Var "n")) ")" ))) ")" )) "holds" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "b2")) ($#k1_seqfunc :::"."::: ) (Set (Var "n"))) ($#r2_relset_1 :::"="::: ) (Set ($#k32_valued_1 :::"-"::: ) (Set "(" (Set (Var "b1")) ($#k1_seqfunc :::"."::: ) (Set (Var "n")) ")" ))))) ; func :::"abs"::: "H" -> ($#m1_subset_1 :::"Functional_Sequence":::) "of" "D" "," (Set ($#k1_numbers :::"REAL"::: ) ) means :: SEQFUNC:def 4 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set it ($#k1_seqfunc :::"."::: ) (Set (Var "n"))) ($#r2_relset_1 :::"="::: ) (Set ($#k56_valued_1 :::"abs"::: ) (Set "(" "H" ($#k1_seqfunc :::"."::: ) (Set (Var "n")) ")" )))); projectivity (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Const "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "b1")) ($#k1_seqfunc :::"."::: ) (Set (Var "n"))) ($#r2_relset_1 :::"="::: ) (Set ($#k56_valued_1 :::"abs"::: ) (Set "(" (Set (Var "b2")) ($#k1_seqfunc :::"."::: ) (Set (Var "n")) ")" ))) ")" )) "holds" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "b1")) ($#k1_seqfunc :::"."::: ) (Set (Var "n"))) ($#r2_relset_1 :::"="::: ) (Set ($#k56_valued_1 :::"abs"::: ) (Set "(" (Set (Var "b1")) ($#k1_seqfunc :::"."::: ) (Set (Var "n")) ")" ))))) ; end; :: deftheorem defines :::"""::: SEQFUNC:def 2 : (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "H")) "," (Set (Var "b3")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "H")) ($#k3_seqfunc :::"""::: ) )) "iff" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "b3")) ($#k1_seqfunc :::"."::: ) (Set (Var "n"))) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "H")) ($#k1_seqfunc :::"."::: ) (Set (Var "n")) ")" ) ($#k6_rfunct_1 :::"^"::: ) ))) ")" ))); :: deftheorem defines :::"-"::: SEQFUNC:def 3 : (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "H")) "," (Set (Var "b3")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k4_seqfunc :::"-"::: ) (Set (Var "H")))) "iff" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "b3")) ($#k1_seqfunc :::"."::: ) (Set (Var "n"))) ($#r2_relset_1 :::"="::: ) (Set ($#k32_valued_1 :::"-"::: ) (Set "(" (Set (Var "H")) ($#k1_seqfunc :::"."::: ) (Set (Var "n")) ")" )))) ")" ))); :: deftheorem defines :::"abs"::: SEQFUNC:def 4 : (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "H")) "," (Set (Var "b3")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k5_seqfunc :::"abs"::: ) (Set (Var "H")))) "iff" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "b3")) ($#k1_seqfunc :::"."::: ) (Set (Var "n"))) ($#r2_relset_1 :::"="::: ) (Set ($#k56_valued_1 :::"abs"::: ) (Set "(" (Set (Var "H")) ($#k1_seqfunc :::"."::: ) (Set (Var "n")) ")" )))) ")" ))); definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "G", "H" be ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Const "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ); func "G" :::"+"::: "H" -> ($#m1_subset_1 :::"Functional_Sequence":::) "of" "D" "," (Set ($#k1_numbers :::"REAL"::: ) ) means :: SEQFUNC:def 5 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set it ($#k1_seqfunc :::"."::: ) (Set (Var "n"))) ($#r2_relset_1 :::"="::: ) (Set (Set "(" "G" ($#k1_seqfunc :::"."::: ) (Set (Var "n")) ")" ) ($#k3_valued_1 :::"+"::: ) (Set "(" "H" ($#k1_seqfunc :::"."::: ) (Set (Var "n")) ")" )))); end; :: deftheorem defines :::"+"::: SEQFUNC:def 5 : (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "," (Set (Var "b4")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k6_seqfunc :::"+"::: ) (Set (Var "H")))) "iff" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "b4")) ($#k1_seqfunc :::"."::: ) (Set (Var "n"))) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "G")) ($#k1_seqfunc :::"."::: ) (Set (Var "n")) ")" ) ($#k3_valued_1 :::"+"::: ) (Set "(" (Set (Var "H")) ($#k1_seqfunc :::"."::: ) (Set (Var "n")) ")" )))) ")" ))); definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "G", "H" be ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Const "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ); func "G" :::"-"::: "H" -> ($#m1_subset_1 :::"Functional_Sequence":::) "of" "D" "," (Set ($#k1_numbers :::"REAL"::: ) ) equals :: SEQFUNC:def 6 (Set "G" ($#k6_seqfunc :::"+"::: ) (Set "(" ($#k4_seqfunc :::"-"::: ) "H" ")" )); end; :: deftheorem defines :::"-"::: SEQFUNC:def 6 : (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set (Var "G")) ($#k7_seqfunc :::"-"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k6_seqfunc :::"+"::: ) (Set "(" ($#k4_seqfunc :::"-"::: ) (Set (Var "H")) ")" ))))); definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "G", "H" be ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Const "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ); func "G" :::"(#)"::: "H" -> ($#m1_subset_1 :::"Functional_Sequence":::) "of" "D" "," (Set ($#k1_numbers :::"REAL"::: ) ) means :: SEQFUNC:def 7 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set it ($#k1_seqfunc :::"."::: ) (Set (Var "n"))) ($#r2_relset_1 :::"="::: ) (Set (Set "(" "G" ($#k1_seqfunc :::"."::: ) (Set (Var "n")) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set "(" "H" ($#k1_seqfunc :::"."::: ) (Set (Var "n")) ")" )))); end; :: deftheorem defines :::"(#)"::: SEQFUNC:def 7 : (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "," (Set (Var "b4")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k8_seqfunc :::"(#)"::: ) (Set (Var "H")))) "iff" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "b4")) ($#k1_seqfunc :::"."::: ) (Set (Var "n"))) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "G")) ($#k1_seqfunc :::"."::: ) (Set (Var "n")) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set "(" (Set (Var "H")) ($#k1_seqfunc :::"."::: ) (Set (Var "n")) ")" )))) ")" ))); definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "H", "G" be ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Const "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ); func "G" :::"/"::: "H" -> ($#m1_subset_1 :::"Functional_Sequence":::) "of" "D" "," (Set ($#k1_numbers :::"REAL"::: ) ) equals :: SEQFUNC:def 8 (Set "G" ($#k8_seqfunc :::"(#)"::: ) (Set "(" "H" ($#k3_seqfunc :::"""::: ) ")" )); end; :: deftheorem defines :::"/"::: SEQFUNC:def 8 : (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "H")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set (Var "G")) ($#k9_seqfunc :::"/"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k8_seqfunc :::"(#)"::: ) (Set "(" (Set (Var "H")) ($#k3_seqfunc :::"""::: ) ")" ))))); theorem :: SEQFUNC:2 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "H1")) "," (Set (Var "G")) "," (Set (Var "H")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "H1")) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "G")) ($#k9_seqfunc :::"/"::: ) (Set (Var "H")))) "iff" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "H1")) ($#k1_seqfunc :::"."::: ) (Set (Var "n"))) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "G")) ($#k1_seqfunc :::"."::: ) (Set (Var "n")) ")" ) ($#k3_rfunct_1 :::"/"::: ) (Set "(" (Set (Var "H")) ($#k1_seqfunc :::"."::: ) (Set (Var "n")) ")" )))) ")" ))) ; theorem :: SEQFUNC:3 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "H1")) "," (Set (Var "G")) "," (Set (Var "H")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "H1")) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "G")) ($#k7_seqfunc :::"-"::: ) (Set (Var "H")))) "iff" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "H1")) ($#k1_seqfunc :::"."::: ) (Set (Var "n"))) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "G")) ($#k1_seqfunc :::"."::: ) (Set (Var "n")) ")" ) ($#k47_valued_1 :::"-"::: ) (Set "(" (Set (Var "H")) ($#k1_seqfunc :::"."::: ) (Set (Var "n")) ")" )))) ")" ))) ; theorem :: SEQFUNC:4 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "," (Set (Var "J")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Set (Var "G")) ($#k6_seqfunc :::"+"::: ) (Set (Var "H"))) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "H")) ($#k6_seqfunc :::"+"::: ) (Set (Var "G")))) & (Bool (Set (Set "(" (Set (Var "G")) ($#k6_seqfunc :::"+"::: ) (Set (Var "H")) ")" ) ($#k6_seqfunc :::"+"::: ) (Set (Var "J"))) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "G")) ($#k6_seqfunc :::"+"::: ) (Set "(" (Set (Var "H")) ($#k6_seqfunc :::"+"::: ) (Set (Var "J")) ")" ))) ")" ))) ; theorem :: SEQFUNC:5 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "," (Set (Var "J")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Set (Var "G")) ($#k8_seqfunc :::"(#)"::: ) (Set (Var "H"))) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "H")) ($#k8_seqfunc :::"(#)"::: ) (Set (Var "G")))) & (Bool (Set (Set "(" (Set (Var "G")) ($#k8_seqfunc :::"(#)"::: ) (Set (Var "H")) ")" ) ($#k8_seqfunc :::"(#)"::: ) (Set (Var "J"))) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "G")) ($#k8_seqfunc :::"(#)"::: ) (Set "(" (Set (Var "H")) ($#k8_seqfunc :::"(#)"::: ) (Set (Var "J")) ")" ))) ")" ))) ; theorem :: SEQFUNC:6 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "," (Set (Var "J")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "G")) ($#k6_seqfunc :::"+"::: ) (Set (Var "H")) ")" ) ($#k8_seqfunc :::"(#)"::: ) (Set (Var "J"))) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "G")) ($#k8_seqfunc :::"(#)"::: ) (Set (Var "J")) ")" ) ($#k6_seqfunc :::"+"::: ) (Set "(" (Set (Var "H")) ($#k8_seqfunc :::"(#)"::: ) (Set (Var "J")) ")" ))) & (Bool (Set (Set (Var "J")) ($#k8_seqfunc :::"(#)"::: ) (Set "(" (Set (Var "G")) ($#k6_seqfunc :::"+"::: ) (Set (Var "H")) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "J")) ($#k8_seqfunc :::"(#)"::: ) (Set (Var "G")) ")" ) ($#k6_seqfunc :::"+"::: ) (Set "(" (Set (Var "J")) ($#k8_seqfunc :::"(#)"::: ) (Set (Var "H")) ")" ))) ")" ))) ; theorem :: SEQFUNC:7 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k4_seqfunc :::"-"::: ) (Set (Var "H"))) ($#r2_relset_1 :::"="::: ) (Set (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) ($#k2_seqfunc :::"(#)"::: ) (Set (Var "H")))))) ; theorem :: SEQFUNC:8 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "," (Set (Var "J")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "G")) ($#k7_seqfunc :::"-"::: ) (Set (Var "H")) ")" ) ($#k8_seqfunc :::"(#)"::: ) (Set (Var "J"))) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "G")) ($#k8_seqfunc :::"(#)"::: ) (Set (Var "J")) ")" ) ($#k7_seqfunc :::"-"::: ) (Set "(" (Set (Var "H")) ($#k8_seqfunc :::"(#)"::: ) (Set (Var "J")) ")" ))) & (Bool (Set (Set "(" (Set (Var "J")) ($#k8_seqfunc :::"(#)"::: ) (Set (Var "G")) ")" ) ($#k7_seqfunc :::"-"::: ) (Set "(" (Set (Var "J")) ($#k8_seqfunc :::"(#)"::: ) (Set (Var "H")) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "J")) ($#k8_seqfunc :::"(#)"::: ) (Set "(" (Set (Var "G")) ($#k7_seqfunc :::"-"::: ) (Set (Var "H")) ")" ))) ")" ))) ; theorem :: SEQFUNC:9 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Set (Var "r")) ($#k2_seqfunc :::"(#)"::: ) (Set "(" (Set (Var "G")) ($#k6_seqfunc :::"+"::: ) (Set (Var "H")) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "r")) ($#k2_seqfunc :::"(#)"::: ) (Set (Var "G")) ")" ) ($#k6_seqfunc :::"+"::: ) (Set "(" (Set (Var "r")) ($#k2_seqfunc :::"(#)"::: ) (Set (Var "H")) ")" ))) & (Bool (Set (Set (Var "r")) ($#k2_seqfunc :::"(#)"::: ) (Set "(" (Set (Var "G")) ($#k7_seqfunc :::"-"::: ) (Set (Var "H")) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "r")) ($#k2_seqfunc :::"(#)"::: ) (Set (Var "G")) ")" ) ($#k7_seqfunc :::"-"::: ) (Set "(" (Set (Var "r")) ($#k2_seqfunc :::"(#)"::: ) (Set (Var "H")) ")" ))) ")" )))) ; theorem :: SEQFUNC:10 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "r")) "," (Set (Var "p")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "r")) ($#k8_real_1 :::"*"::: ) (Set (Var "p")) ")" ) ($#k2_seqfunc :::"(#)"::: ) (Set (Var "H"))) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "r")) ($#k2_seqfunc :::"(#)"::: ) (Set "(" (Set (Var "p")) ($#k2_seqfunc :::"(#)"::: ) (Set (Var "H")) ")" )))))) ; theorem :: SEQFUNC:11 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Num 1) ($#k2_seqfunc :::"(#)"::: ) (Set (Var "H"))) ($#r2_relset_1 :::"="::: ) (Set (Var "H"))))) ; theorem :: SEQFUNC:12 canceled; theorem :: SEQFUNC:13 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "G")) ($#k3_seqfunc :::"""::: ) ")" ) ($#k8_seqfunc :::"(#)"::: ) (Set "(" (Set (Var "H")) ($#k3_seqfunc :::"""::: ) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "G")) ($#k8_seqfunc :::"(#)"::: ) (Set (Var "H")) ")" ) ($#k3_seqfunc :::"""::: ) )))) ; theorem :: SEQFUNC:14 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "r")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" (Set (Var "r")) ($#k2_seqfunc :::"(#)"::: ) (Set (Var "H")) ")" ) ($#k3_seqfunc :::"""::: ) ) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "r")) ($#k2_real_1 :::"""::: ) ")" ) ($#k2_seqfunc :::"(#)"::: ) (Set "(" (Set (Var "H")) ($#k3_seqfunc :::"""::: ) ")" )))))) ; theorem :: SEQFUNC:15 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set "(" ($#k5_seqfunc :::"abs"::: ) (Set (Var "H")) ")" ) ($#k3_seqfunc :::"""::: ) ) ($#r2_relset_1 :::"="::: ) (Set ($#k5_seqfunc :::"abs"::: ) (Set "(" (Set (Var "H")) ($#k3_seqfunc :::"""::: ) ")" ))))) ; theorem :: SEQFUNC:16 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k5_seqfunc :::"abs"::: ) (Set "(" (Set (Var "G")) ($#k8_seqfunc :::"(#)"::: ) (Set (Var "H")) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set "(" ($#k5_seqfunc :::"abs"::: ) (Set (Var "G")) ")" ) ($#k8_seqfunc :::"(#)"::: ) (Set "(" ($#k5_seqfunc :::"abs"::: ) (Set (Var "H")) ")" ))))) ; theorem :: SEQFUNC:17 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k5_seqfunc :::"abs"::: ) (Set "(" (Set (Var "G")) ($#k9_seqfunc :::"/"::: ) (Set (Var "H")) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set "(" ($#k5_seqfunc :::"abs"::: ) (Set (Var "G")) ")" ) ($#k9_seqfunc :::"/"::: ) (Set "(" ($#k5_seqfunc :::"abs"::: ) (Set (Var "H")) ")" ))))) ; theorem :: SEQFUNC:18 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k5_seqfunc :::"abs"::: ) (Set "(" (Set (Var "r")) ($#k2_seqfunc :::"(#)"::: ) (Set (Var "H")) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set "(" ($#k18_complex1 :::"abs"::: ) (Set (Var "r")) ")" ) ($#k2_seqfunc :::"(#)"::: ) (Set "(" ($#k5_seqfunc :::"abs"::: ) (Set (Var "H")) ")" )))))) ; definitionlet "D1", "D2" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Const "D1")) "," (Set (Const "D2")); let "X" be ($#m1_hidden :::"set"::: ) ; pred "X" :::"common_on_dom"::: "F" means :: SEQFUNC:def 9 (Bool "(" (Bool "X" ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "X" ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" "F" ($#k1_seqfunc :::"."::: ) (Set (Var "n")) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"common_on_dom"::: SEQFUNC:def 9 : (Bool "for" (Set (Var "D1")) "," (Set (Var "D2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "D1")) "," (Set (Var "D2")) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r1_seqfunc :::"common_on_dom"::: ) (Set (Var "F"))) "iff" (Bool "(" (Bool (Set (Var "X")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k1_seqfunc :::"."::: ) (Set (Var "n")) ")" ))) ")" ) ")" ) ")" )))); definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "H" be ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Const "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ); let "x" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "D")); func "H" :::"#"::: "x" -> ($#m1_subset_1 :::"Real_Sequence":::) means :: SEQFUNC:def 10 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set it ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "H" ($#k1_seqfunc :::"."::: ) (Set (Var "n")) ")" ) ($#k1_seq_1 :::"."::: ) "x"))); end; :: deftheorem defines :::"#"::: SEQFUNC:def 10 : (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "H")) ($#k10_seqfunc :::"#"::: ) (Set (Var "x")))) "iff" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "b4")) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "H")) ($#k1_seqfunc :::"."::: ) (Set (Var "n")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))))) ")" ))))); definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "H" be ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Const "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ); let "X" be ($#m1_hidden :::"set"::: ) ; pred "H" :::"is_point_conv_on"::: "X" means :: SEQFUNC:def 11 (Bool "(" (Bool "X" ($#r1_seqfunc :::"common_on_dom"::: ) "H") & (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" "D" "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool "X" ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "D" "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "X")) "holds" (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "p")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (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 "n")) ($#r1_xxreal_0 :::">="::: ) (Set (Var "k")))) "holds" (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set "(" (Set "(" "H" ($#k1_seqfunc :::"."::: ) (Set (Var "n")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "p")))))) ")" ) ")" )) ")" ); end; :: deftheorem defines :::"is_point_conv_on"::: SEQFUNC:def 11 : (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "H")) ($#r2_seqfunc :::"is_point_conv_on"::: ) (Set (Var "X"))) "iff" (Bool "(" (Bool (Set (Var "X")) ($#r1_seqfunc :::"common_on_dom"::: ) (Set (Var "H"))) & (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "p")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (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 "n")) ($#r1_xxreal_0 :::">="::: ) (Set (Var "k")))) "holds" (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "H")) ($#k1_seqfunc :::"."::: ) (Set (Var "n")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "p")))))) ")" ) ")" )) ")" ) ")" )))); theorem :: SEQFUNC:19 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "H")) ($#r2_seqfunc :::"is_point_conv_on"::: ) (Set (Var "X"))) "iff" (Bool "(" (Bool (Set (Var "X")) ($#r1_seqfunc :::"common_on_dom"::: ) (Set (Var "H"))) & (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool "(" (Bool (Set (Set (Var "H")) ($#k10_seqfunc :::"#"::: ) (Set (Var "x"))) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set "(" (Set (Var "H")) ($#k10_seqfunc :::"#"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x")))) ")" ) ")" ) ")" )) ")" ) ")" )))) ; theorem :: SEQFUNC:20 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "H")) ($#r2_seqfunc :::"is_point_conv_on"::: ) (Set (Var "X"))) "iff" (Bool "(" (Bool (Set (Var "X")) ($#r1_seqfunc :::"common_on_dom"::: ) (Set (Var "H"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "H")) ($#k10_seqfunc :::"#"::: ) (Set (Var "x"))) "is" ($#v2_comseq_2 :::"convergent"::: ) ) ")" ) ")" ) ")" )))) ; definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "H" be ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Const "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ); let "X" be ($#m1_hidden :::"set"::: ) ; pred "H" :::"is_unif_conv_on"::: "X" means :: SEQFUNC:def 12 (Bool "(" (Bool "X" ($#r1_seqfunc :::"common_on_dom"::: ) "H") & (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" "D" "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool "X" ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool "(" "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "p")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (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"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "D" "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Set (Var "k"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "X")) "holds" (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set "(" (Set "(" "H" ($#k1_seqfunc :::"."::: ) (Set (Var "n")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "p")))))) ")" ) ")" )) ")" ); end; :: deftheorem defines :::"is_unif_conv_on"::: SEQFUNC:def 12 : (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "H")) ($#r3_seqfunc :::"is_unif_conv_on"::: ) (Set (Var "X"))) "iff" (Bool "(" (Bool (Set (Var "X")) ($#r1_seqfunc :::"common_on_dom"::: ) (Set (Var "H"))) & (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool "(" "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "p")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (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"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Set (Var "k"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "H")) ($#k1_seqfunc :::"."::: ) (Set (Var "n")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "p")))))) ")" ) ")" )) ")" ) ")" )))); definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "H" be ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Const "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ); let "X" be ($#m1_hidden :::"set"::: ) ; assume (Bool (Set (Const "H")) ($#r2_seqfunc :::"is_point_conv_on"::: ) (Set (Const "X"))) ; func :::"lim"::: "(" "H" "," "X" ")" -> ($#m1_subset_1 :::"PartFunc":::) "of" "D" "," (Set ($#k1_numbers :::"REAL"::: ) ) means :: SEQFUNC:def 13 (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) "X") & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "D" "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) it))) "holds" (Bool (Set it ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k2_seq_2 :::"lim"::: ) (Set "(" "H" ($#k10_seqfunc :::"#"::: ) (Set (Var "x")) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"lim"::: SEQFUNC:def 13 : (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "H")) ($#r2_seqfunc :::"is_point_conv_on"::: ) (Set (Var "X")))) "holds" (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k11_seqfunc :::"lim"::: ) "(" (Set (Var "H")) "," (Set (Var "X")) ")" )) "iff" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set (Var "X"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "b4"))))) "holds" (Bool (Set (Set (Var "b4")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k2_seq_2 :::"lim"::: ) (Set "(" (Set (Var "H")) ($#k10_seqfunc :::"#"::: ) (Set (Var "x")) ")" ))) ")" ) ")" ) ")" ))))); theorem :: SEQFUNC:21 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "H")) ($#r2_seqfunc :::"is_point_conv_on"::: ) (Set (Var "X")))) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_relset_1 :::"="::: ) (Set ($#k11_seqfunc :::"lim"::: ) "(" (Set (Var "H")) "," (Set (Var "X")) ")" )) "iff" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "X"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "p")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (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 "n")) ($#r1_xxreal_0 :::">="::: ) (Set (Var "k")))) "holds" (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "H")) ($#k1_seqfunc :::"."::: ) (Set (Var "n")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "p")))))) ")" ) ")" ) ")" ))))) ; theorem :: SEQFUNC:22 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "H")) ($#r3_seqfunc :::"is_unif_conv_on"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "H")) ($#r2_seqfunc :::"is_point_conv_on"::: ) (Set (Var "X")))))) ; theorem :: SEQFUNC:23 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "Y")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "Y")) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) & (Bool (Set (Var "Y")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "X")) ($#r1_seqfunc :::"common_on_dom"::: ) (Set (Var "H")))) "holds" (Bool (Set (Var "Y")) ($#r1_seqfunc :::"common_on_dom"::: ) (Set (Var "H")))))) ; theorem :: SEQFUNC:24 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "Y")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "Y")) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) & (Bool (Set (Var "Y")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "H")) ($#r2_seqfunc :::"is_point_conv_on"::: ) (Set (Var "X")))) "holds" (Bool "(" (Bool (Set (Var "H")) ($#r2_seqfunc :::"is_point_conv_on"::: ) (Set (Var "Y"))) & (Bool (Set (Set "(" ($#k11_seqfunc :::"lim"::: ) "(" (Set (Var "H")) "," (Set (Var "X")) ")" ")" ) ($#k2_partfun1 :::"|"::: ) (Set (Var "Y"))) ($#r2_relset_1 :::"="::: ) (Set ($#k11_seqfunc :::"lim"::: ) "(" (Set (Var "H")) "," (Set (Var "Y")) ")" )) ")" )))) ; theorem :: SEQFUNC:25 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "Y")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "Y")) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) & (Bool (Set (Var "Y")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "H")) ($#r3_seqfunc :::"is_unif_conv_on"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "H")) ($#r3_seqfunc :::"is_unif_conv_on"::: ) (Set (Var "Y")))))) ; theorem :: SEQFUNC:26 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_seqfunc :::"common_on_dom"::: ) (Set (Var "H")))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ($#r1_seqfunc :::"common_on_dom"::: ) (Set (Var "H"))))))) ; theorem :: SEQFUNC:27 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "H")) ($#r2_seqfunc :::"is_point_conv_on"::: ) (Set (Var "X")))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ($#r1_seqfunc :::"common_on_dom"::: ) (Set (Var "H"))))))) ; theorem :: SEQFUNC:28 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "st" (Bool (Bool (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ($#r1_seqfunc :::"common_on_dom"::: ) (Set (Var "H1"))) & (Bool (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ($#r1_seqfunc :::"common_on_dom"::: ) (Set (Var "H2")))) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "H1")) ($#k10_seqfunc :::"#"::: ) (Set (Var "x")) ")" ) ($#k3_valued_1 :::"+"::: ) (Set "(" (Set (Var "H2")) ($#k10_seqfunc :::"#"::: ) (Set (Var "x")) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "H1")) ($#k6_seqfunc :::"+"::: ) (Set (Var "H2")) ")" ) ($#k10_seqfunc :::"#"::: ) (Set (Var "x")))) & (Bool (Set (Set "(" (Set (Var "H1")) ($#k10_seqfunc :::"#"::: ) (Set (Var "x")) ")" ) ($#k47_valued_1 :::"-"::: ) (Set "(" (Set (Var "H2")) ($#k10_seqfunc :::"#"::: ) (Set (Var "x")) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "H1")) ($#k7_seqfunc :::"-"::: ) (Set (Var "H2")) ")" ) ($#k10_seqfunc :::"#"::: ) (Set (Var "x")))) & (Bool (Set (Set "(" (Set (Var "H1")) ($#k10_seqfunc :::"#"::: ) (Set (Var "x")) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set "(" (Set (Var "H2")) ($#k10_seqfunc :::"#"::: ) (Set (Var "x")) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "H1")) ($#k8_seqfunc :::"(#)"::: ) (Set (Var "H2")) ")" ) ($#k10_seqfunc :::"#"::: ) (Set (Var "x")))) ")" )))) ; theorem :: SEQFUNC:29 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "holds" (Bool "(" (Bool (Set (Set "(" ($#k5_seqfunc :::"abs"::: ) (Set (Var "H")) ")" ) ($#k10_seqfunc :::"#"::: ) (Set (Var "x"))) ($#r2_relset_1 :::"="::: ) (Set ($#k56_valued_1 :::"abs"::: ) (Set "(" (Set (Var "H")) ($#k10_seqfunc :::"#"::: ) (Set (Var "x")) ")" ))) & (Bool (Set (Set "(" ($#k4_seqfunc :::"-"::: ) (Set (Var "H")) ")" ) ($#k10_seqfunc :::"#"::: ) (Set (Var "x"))) ($#r2_relset_1 :::"="::: ) (Set ($#k32_valued_1 :::"-"::: ) (Set "(" (Set (Var "H")) ($#k10_seqfunc :::"#"::: ) (Set (Var "x")) ")" ))) ")" )))) ; theorem :: SEQFUNC:30 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "st" (Bool (Bool (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ($#r1_seqfunc :::"common_on_dom"::: ) (Set (Var "H")))) "holds" (Bool (Set (Set "(" (Set (Var "r")) ($#k2_seqfunc :::"(#)"::: ) (Set (Var "H")) ")" ) ($#k10_seqfunc :::"#"::: ) (Set (Var "x"))) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set "(" (Set (Var "H")) ($#k10_seqfunc :::"#"::: ) (Set (Var "x")) ")" ))))))) ; theorem :: SEQFUNC:31 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_seqfunc :::"common_on_dom"::: ) (Set (Var "H1"))) & (Bool (Set (Var "X")) ($#r1_seqfunc :::"common_on_dom"::: ) (Set (Var "H2")))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "H1")) ($#k10_seqfunc :::"#"::: ) (Set (Var "x")) ")" ) ($#k3_valued_1 :::"+"::: ) (Set "(" (Set (Var "H2")) ($#k10_seqfunc :::"#"::: ) (Set (Var "x")) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "H1")) ($#k6_seqfunc :::"+"::: ) (Set (Var "H2")) ")" ) ($#k10_seqfunc :::"#"::: ) (Set (Var "x")))) & (Bool (Set (Set "(" (Set (Var "H1")) ($#k10_seqfunc :::"#"::: ) (Set (Var "x")) ")" ) ($#k47_valued_1 :::"-"::: ) (Set "(" (Set (Var "H2")) ($#k10_seqfunc :::"#"::: ) (Set (Var "x")) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "H1")) ($#k7_seqfunc :::"-"::: ) (Set (Var "H2")) ")" ) ($#k10_seqfunc :::"#"::: ) (Set (Var "x")))) & (Bool (Set (Set "(" (Set (Var "H1")) ($#k10_seqfunc :::"#"::: ) (Set (Var "x")) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set "(" (Set (Var "H2")) ($#k10_seqfunc :::"#"::: ) (Set (Var "x")) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "H1")) ($#k8_seqfunc :::"(#)"::: ) (Set (Var "H2")) ")" ) ($#k10_seqfunc :::"#"::: ) (Set (Var "x")))) ")" ))))) ; theorem :: SEQFUNC:32 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "holds" (Bool "(" (Bool (Set (Set "(" ($#k5_seqfunc :::"abs"::: ) (Set (Var "H")) ")" ) ($#k10_seqfunc :::"#"::: ) (Set (Var "x"))) ($#r2_relset_1 :::"="::: ) (Set ($#k56_valued_1 :::"abs"::: ) (Set "(" (Set (Var "H")) ($#k10_seqfunc :::"#"::: ) (Set (Var "x")) ")" ))) & (Bool (Set (Set "(" ($#k4_seqfunc :::"-"::: ) (Set (Var "H")) ")" ) ($#k10_seqfunc :::"#"::: ) (Set (Var "x"))) ($#r2_relset_1 :::"="::: ) (Set ($#k32_valued_1 :::"-"::: ) (Set "(" (Set (Var "H")) ($#k10_seqfunc :::"#"::: ) (Set (Var "x")) ")" ))) ")" )))) ; theorem :: SEQFUNC:33 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_seqfunc :::"common_on_dom"::: ) (Set (Var "H")))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set "(" (Set (Var "r")) ($#k2_seqfunc :::"(#)"::: ) (Set (Var "H")) ")" ) ($#k10_seqfunc :::"#"::: ) (Set (Var "x"))) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set "(" (Set (Var "H")) ($#k10_seqfunc :::"#"::: ) (Set (Var "x")) ")" )))))))) ; theorem :: SEQFUNC:34 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "H1")) ($#r2_seqfunc :::"is_point_conv_on"::: ) (Set (Var "X"))) & (Bool (Set (Var "H2")) ($#r2_seqfunc :::"is_point_conv_on"::: ) (Set (Var "X")))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "H1")) ($#k10_seqfunc :::"#"::: ) (Set (Var "x")) ")" ) ($#k3_valued_1 :::"+"::: ) (Set "(" (Set (Var "H2")) ($#k10_seqfunc :::"#"::: ) (Set (Var "x")) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "H1")) ($#k6_seqfunc :::"+"::: ) (Set (Var "H2")) ")" ) ($#k10_seqfunc :::"#"::: ) (Set (Var "x")))) & (Bool (Set (Set "(" (Set (Var "H1")) ($#k10_seqfunc :::"#"::: ) (Set (Var "x")) ")" ) ($#k47_valued_1 :::"-"::: ) (Set "(" (Set (Var "H2")) ($#k10_seqfunc :::"#"::: ) (Set (Var "x")) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "H1")) ($#k7_seqfunc :::"-"::: ) (Set (Var "H2")) ")" ) ($#k10_seqfunc :::"#"::: ) (Set (Var "x")))) & (Bool (Set (Set "(" (Set (Var "H1")) ($#k10_seqfunc :::"#"::: ) (Set (Var "x")) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set "(" (Set (Var "H2")) ($#k10_seqfunc :::"#"::: ) (Set (Var "x")) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "H1")) ($#k8_seqfunc :::"(#)"::: ) (Set (Var "H2")) ")" ) ($#k10_seqfunc :::"#"::: ) (Set (Var "x")))) ")" ))))) ; theorem :: SEQFUNC:35 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "holds" (Bool "(" (Bool (Set (Set "(" ($#k5_seqfunc :::"abs"::: ) (Set (Var "H")) ")" ) ($#k10_seqfunc :::"#"::: ) (Set (Var "x"))) ($#r2_relset_1 :::"="::: ) (Set ($#k56_valued_1 :::"abs"::: ) (Set "(" (Set (Var "H")) ($#k10_seqfunc :::"#"::: ) (Set (Var "x")) ")" ))) & (Bool (Set (Set "(" ($#k4_seqfunc :::"-"::: ) (Set (Var "H")) ")" ) ($#k10_seqfunc :::"#"::: ) (Set (Var "x"))) ($#r2_relset_1 :::"="::: ) (Set ($#k32_valued_1 :::"-"::: ) (Set "(" (Set (Var "H")) ($#k10_seqfunc :::"#"::: ) (Set (Var "x")) ")" ))) ")" )))) ; theorem :: SEQFUNC:36 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "H")) ($#r2_seqfunc :::"is_point_conv_on"::: ) (Set (Var "X")))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set "(" (Set (Var "r")) ($#k2_seqfunc :::"(#)"::: ) (Set (Var "H")) ")" ) ($#k10_seqfunc :::"#"::: ) (Set (Var "x"))) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set "(" (Set (Var "H")) ($#k10_seqfunc :::"#"::: ) (Set (Var "x")) ")" )))))))) ; theorem :: SEQFUNC:37 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_seqfunc :::"common_on_dom"::: ) (Set (Var "H1"))) & (Bool (Set (Var "X")) ($#r1_seqfunc :::"common_on_dom"::: ) (Set (Var "H2")))) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r1_seqfunc :::"common_on_dom"::: ) (Set (Set (Var "H1")) ($#k6_seqfunc :::"+"::: ) (Set (Var "H2")))) & (Bool (Set (Var "X")) ($#r1_seqfunc :::"common_on_dom"::: ) (Set (Set (Var "H1")) ($#k7_seqfunc :::"-"::: ) (Set (Var "H2")))) & (Bool (Set (Var "X")) ($#r1_seqfunc :::"common_on_dom"::: ) (Set (Set (Var "H1")) ($#k8_seqfunc :::"(#)"::: ) (Set (Var "H2")))) ")" )))) ; theorem :: SEQFUNC:38 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_seqfunc :::"common_on_dom"::: ) (Set (Var "H")))) "holds" (Bool "(" (Bool (Set (Var "X")) ($#r1_seqfunc :::"common_on_dom"::: ) (Set ($#k5_seqfunc :::"abs"::: ) (Set (Var "H")))) & (Bool (Set (Var "X")) ($#r1_seqfunc :::"common_on_dom"::: ) (Set ($#k4_seqfunc :::"-"::: ) (Set (Var "H")))) ")" )))) ; theorem :: SEQFUNC:39 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_seqfunc :::"common_on_dom"::: ) (Set (Var "H")))) "holds" (Bool (Set (Var "X")) ($#r1_seqfunc :::"common_on_dom"::: ) (Set (Set (Var "r")) ($#k2_seqfunc :::"(#)"::: ) (Set (Var "H")))))))) ; theorem :: SEQFUNC:40 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "H1")) ($#r2_seqfunc :::"is_point_conv_on"::: ) (Set (Var "X"))) & (Bool (Set (Var "H2")) ($#r2_seqfunc :::"is_point_conv_on"::: ) (Set (Var "X")))) "holds" (Bool "(" (Bool (Set (Set (Var "H1")) ($#k6_seqfunc :::"+"::: ) (Set (Var "H2"))) ($#r2_seqfunc :::"is_point_conv_on"::: ) (Set (Var "X"))) & (Bool (Set ($#k11_seqfunc :::"lim"::: ) "(" (Set "(" (Set (Var "H1")) ($#k6_seqfunc :::"+"::: ) (Set (Var "H2")) ")" ) "," (Set (Var "X")) ")" ) ($#r2_relset_1 :::"="::: ) (Set (Set "(" ($#k11_seqfunc :::"lim"::: ) "(" (Set (Var "H1")) "," (Set (Var "X")) ")" ")" ) ($#k3_valued_1 :::"+"::: ) (Set "(" ($#k11_seqfunc :::"lim"::: ) "(" (Set (Var "H2")) "," (Set (Var "X")) ")" ")" ))) & (Bool (Set (Set (Var "H1")) ($#k7_seqfunc :::"-"::: ) (Set (Var "H2"))) ($#r2_seqfunc :::"is_point_conv_on"::: ) (Set (Var "X"))) & (Bool (Set ($#k11_seqfunc :::"lim"::: ) "(" (Set "(" (Set (Var "H1")) ($#k7_seqfunc :::"-"::: ) (Set (Var "H2")) ")" ) "," (Set (Var "X")) ")" ) ($#r2_relset_1 :::"="::: ) (Set (Set "(" ($#k11_seqfunc :::"lim"::: ) "(" (Set (Var "H1")) "," (Set (Var "X")) ")" ")" ) ($#k47_valued_1 :::"-"::: ) (Set "(" ($#k11_seqfunc :::"lim"::: ) "(" (Set (Var "H2")) "," (Set (Var "X")) ")" ")" ))) & (Bool (Set (Set (Var "H1")) ($#k8_seqfunc :::"(#)"::: ) (Set (Var "H2"))) ($#r2_seqfunc :::"is_point_conv_on"::: ) (Set (Var "X"))) & (Bool (Set ($#k11_seqfunc :::"lim"::: ) "(" (Set "(" (Set (Var "H1")) ($#k8_seqfunc :::"(#)"::: ) (Set (Var "H2")) ")" ) "," (Set (Var "X")) ")" ) ($#r2_relset_1 :::"="::: ) (Set (Set "(" ($#k11_seqfunc :::"lim"::: ) "(" (Set (Var "H1")) "," (Set (Var "X")) ")" ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set "(" ($#k11_seqfunc :::"lim"::: ) "(" (Set (Var "H2")) "," (Set (Var "X")) ")" ")" ))) ")" )))) ; theorem :: SEQFUNC:41 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "H")) ($#r2_seqfunc :::"is_point_conv_on"::: ) (Set (Var "X")))) "holds" (Bool "(" (Bool (Set ($#k5_seqfunc :::"abs"::: ) (Set (Var "H"))) ($#r2_seqfunc :::"is_point_conv_on"::: ) (Set (Var "X"))) & (Bool (Set ($#k11_seqfunc :::"lim"::: ) "(" (Set "(" ($#k5_seqfunc :::"abs"::: ) (Set (Var "H")) ")" ) "," (Set (Var "X")) ")" ) ($#r2_relset_1 :::"="::: ) (Set ($#k56_valued_1 :::"abs"::: ) (Set "(" ($#k11_seqfunc :::"lim"::: ) "(" (Set (Var "H")) "," (Set (Var "X")) ")" ")" ))) & (Bool (Set ($#k4_seqfunc :::"-"::: ) (Set (Var "H"))) ($#r2_seqfunc :::"is_point_conv_on"::: ) (Set (Var "X"))) & (Bool (Set ($#k11_seqfunc :::"lim"::: ) "(" (Set "(" ($#k4_seqfunc :::"-"::: ) (Set (Var "H")) ")" ) "," (Set (Var "X")) ")" ) ($#r2_relset_1 :::"="::: ) (Set ($#k32_valued_1 :::"-"::: ) (Set "(" ($#k11_seqfunc :::"lim"::: ) "(" (Set (Var "H")) "," (Set (Var "X")) ")" ")" ))) ")" )))) ; theorem :: SEQFUNC:42 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "H")) ($#r2_seqfunc :::"is_point_conv_on"::: ) (Set (Var "X")))) "holds" (Bool "(" (Bool (Set (Set (Var "r")) ($#k2_seqfunc :::"(#)"::: ) (Set (Var "H"))) ($#r2_seqfunc :::"is_point_conv_on"::: ) (Set (Var "X"))) & (Bool (Set ($#k11_seqfunc :::"lim"::: ) "(" (Set "(" (Set (Var "r")) ($#k2_seqfunc :::"(#)"::: ) (Set (Var "H")) ")" ) "," (Set (Var "X")) ")" ) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set "(" ($#k11_seqfunc :::"lim"::: ) "(" (Set (Var "H")) "," (Set (Var "X")) ")" ")" ))) ")" ))))) ; theorem :: SEQFUNC:43 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "H")) ($#r3_seqfunc :::"is_unif_conv_on"::: ) (Set (Var "X"))) "iff" (Bool "(" (Bool (Set (Var "X")) ($#r1_seqfunc :::"common_on_dom"::: ) (Set (Var "H"))) & (Bool (Set (Var "H")) ($#r2_seqfunc :::"is_point_conv_on"::: ) (Set (Var "X"))) & (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r")))) "holds" (Bool "ex" (Set (Var "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"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Set (Var "k"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "H")) ($#k1_seqfunc :::"."::: ) (Set (Var "n")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k11_seqfunc :::"lim"::: ) "(" (Set (Var "H")) "," (Set (Var "X")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r")))))) ")" ) ")" ) ")" )))) ; theorem :: SEQFUNC:44 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "H")) ($#r3_seqfunc :::"is_unif_conv_on"::: ) (Set (Var "X"))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "H")) ($#k1_seqfunc :::"."::: ) (Set (Var "n")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) "is" ($#v1_fcont_1 :::"continuous"::: ) ) ")" )) "holds" (Bool (Set (Set "(" ($#k11_seqfunc :::"lim"::: ) "(" (Set (Var "H")) "," (Set (Var "X")) ")" ")" ) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) "is" ($#v1_fcont_1 :::"continuous"::: ) ))) ;