:: INTEGRA7 semantic presentation begin theorem :: INTEGRA7:1 (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "f"))) "is" ($#v4_xxreal_2 :::"bounded_above"::: ) ) & (Bool (Set ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "g"))) "is" ($#v4_xxreal_2 :::"bounded_above"::: ) ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set "(" (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "g")) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "a"))) ")" )) "holds" (Bool "(" (Bool (Set (Set "(" ($#k4_seq_4 :::"upper_bound"::: ) (Set "(" ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "f")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k4_seq_4 :::"upper_bound"::: ) (Set "(" ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "g")) ")" ) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "a"))) & (Bool (Set (Set "(" ($#k4_seq_4 :::"upper_bound"::: ) (Set "(" ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "g")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k4_seq_4 :::"upper_bound"::: ) (Set "(" ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "f")) ")" ) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "a"))) ")" )))) ; theorem :: INTEGRA7:2 (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "f"))) "is" ($#v3_xxreal_2 :::"bounded_below"::: ) ) & (Bool (Set ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "g"))) "is" ($#v3_xxreal_2 :::"bounded_below"::: ) ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set "(" (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "g")) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "a"))) ")" )) "holds" (Bool "(" (Bool (Set (Set "(" ($#k5_seq_4 :::"lower_bound"::: ) (Set "(" ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "f")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k5_seq_4 :::"lower_bound"::: ) (Set "(" ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "g")) ")" ) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "a"))) & (Bool (Set (Set "(" ($#k5_seq_4 :::"lower_bound"::: ) (Set "(" ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "g")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k5_seq_4 :::"lower_bound"::: ) (Set "(" ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "f")) ")" ) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "a"))) ")" )))) ; theorem :: INTEGRA7:3 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) "is" ($#v1_comseq_2 :::"bounded"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) "is" ($#v1_comseq_2 :::"bounded"::: ) ))) ; theorem :: INTEGRA7:4 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "x")))) "holds" (Bool (Set (Var "f")) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "x")))))) ; theorem :: INTEGRA7:5 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "f")) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "X"))))) ; theorem :: INTEGRA7:6 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "X"))) & (Bool (Set (Var "g")) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "X")))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k3_valued_1 :::"+"::: ) (Set (Var "g"))) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "X"))) & (Bool (Set (Set (Var "f")) ($#k47_valued_1 :::"-"::: ) (Set (Var "g"))) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "X"))) & (Bool (Set (Set (Var "f")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "g"))) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "X"))) ")" ))) ; theorem :: INTEGRA7:7 (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (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")) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f"))) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "X")))))) ; theorem :: INTEGRA7:8 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "g")) "," (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "g")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) & (Bool (Set (Var "f")) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "X"))) & (Bool (Set (Var "g")) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "f")) ($#k3_rfunct_1 :::"/"::: ) (Set (Var "g"))) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "X"))))) ; theorem :: INTEGRA7:9 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) & (Bool (Set (Var "f")) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "f")) ($#k6_rfunct_1 :::"^"::: ) ) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "X"))))) ; theorem :: INTEGRA7:10 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "b"))) & (Bool (Set ($#k3_integra5 :::"['"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k3_integra5 :::"']"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) & (Bool (Set (Var "F")) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "X"))) & (Bool (Set (Set (Var "F")) ($#k2_fdiff_1 :::"`|"::: ) (Set (Var "X"))) ($#r1_integra5 :::"is_integrable_on"::: ) (Set ($#k3_integra5 :::"['"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k3_integra5 :::"']"::: ) )) & (Bool (Set (Set "(" (Set (Var "F")) ($#k2_fdiff_1 :::"`|"::: ) (Set (Var "X")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set ($#k3_integra5 :::"['"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k3_integra5 :::"']"::: ) )) "is" ($#v1_comseq_2 :::"bounded"::: ) )) "holds" (Bool (Set (Set (Var "F")) ($#k1_seq_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_integra5 :::"integral"::: ) "(" (Set "(" (Set (Var "F")) ($#k2_fdiff_1 :::"`|"::: ) (Set (Var "X")) ")" ) "," (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "F")) ($#k1_seq_1 :::"."::: ) (Set (Var "a")) ")" )))))) ; begin definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ); func :::"IntegralFuncs"::: "(" "f" "," "X" ")" -> ($#m1_hidden :::"set"::: ) means :: INTEGRA7:def 1 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "F"))) & (Bool (Set (Var "F")) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) "X") & (Bool (Set (Set (Var "F")) ($#k2_fdiff_1 :::"`|"::: ) "X") ($#r2_relset_1 :::"="::: ) (Set "f" ($#k2_partfun1 :::"|"::: ) "X")) ")" )) ")" )); end; :: deftheorem defines :::"IntegralFuncs"::: INTEGRA7:def 1 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k1_integra7 :::"IntegralFuncs"::: ) "(" (Set (Var "f")) "," (Set (Var "X")) ")" )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "F"))) & (Bool (Set (Var "F")) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Var "X"))) & (Bool (Set (Set (Var "F")) ($#k2_fdiff_1 :::"`|"::: ) (Set (Var "X"))) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X")))) ")" )) ")" )) ")" )))); definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "F", "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ); pred "F" :::"is_integral_of"::: "f" "," "X" means :: INTEGRA7:def 2 (Bool "F" ($#r2_hidden :::"in"::: ) (Set ($#k1_integra7 :::"IntegralFuncs"::: ) "(" "f" "," "X" ")" )); end; :: deftheorem defines :::"is_integral_of"::: INTEGRA7:def 2 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "F")) ($#r1_integra7 :::"is_integral_of"::: ) (Set (Var "f")) "," (Set (Var "X"))) "iff" (Bool (Set (Var "F")) ($#r2_hidden :::"in"::: ) (Set ($#k1_integra7 :::"IntegralFuncs"::: ) "(" (Set (Var "f")) "," (Set (Var "X")) ")" )) ")" ))); theorem :: INTEGRA7:11 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "F")) ($#r1_integra7 :::"is_integral_of"::: ) (Set (Var "f")) "," (Set (Var "X")))) "holds" (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "F")))))) ; theorem :: INTEGRA7:12 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "f")) "," (Set (Var "G")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "F")) ($#r1_integra7 :::"is_integral_of"::: ) (Set (Var "f")) "," (Set (Var "X"))) & (Bool (Set (Var "G")) ($#r1_integra7 :::"is_integral_of"::: ) (Set (Var "g")) "," (Set (Var "X")))) "holds" (Bool "(" (Bool (Set (Set (Var "F")) ($#k3_valued_1 :::"+"::: ) (Set (Var "G"))) ($#r1_integra7 :::"is_integral_of"::: ) (Set (Set (Var "f")) ($#k3_valued_1 :::"+"::: ) (Set (Var "g"))) "," (Set (Var "X"))) & (Bool (Set (Set (Var "F")) ($#k47_valued_1 :::"-"::: ) (Set (Var "G"))) ($#r1_integra7 :::"is_integral_of"::: ) (Set (Set (Var "f")) ($#k47_valued_1 :::"-"::: ) (Set (Var "g"))) "," (Set (Var "X"))) ")" ))) ; theorem :: INTEGRA7:13 (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "F")) ($#r1_integra7 :::"is_integral_of"::: ) (Set (Var "f")) "," (Set (Var "X")))) "holds" (Bool (Set (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "F"))) ($#r1_integra7 :::"is_integral_of"::: ) (Set (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f"))) "," (Set (Var "X")))))) ; theorem :: INTEGRA7:14 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "f")) "," (Set (Var "G")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "F")) ($#r1_integra7 :::"is_integral_of"::: ) (Set (Var "f")) "," (Set (Var "X"))) & (Bool (Set (Var "G")) ($#r1_integra7 :::"is_integral_of"::: ) (Set (Var "g")) "," (Set (Var "X")))) "holds" (Bool (Set (Set (Var "F")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "G"))) ($#r1_integra7 :::"is_integral_of"::: ) (Set (Set "(" (Set (Var "f")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "G")) ")" ) ($#k3_valued_1 :::"+"::: ) (Set "(" (Set (Var "F")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "g")) ")" )) "," (Set (Var "X"))))) ; theorem :: INTEGRA7:15 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "," (Set (Var "F")) "," (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "G")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) & (Bool (Set (Var "F")) ($#r1_integra7 :::"is_integral_of"::: ) (Set (Var "f")) "," (Set (Var "X"))) & (Bool (Set (Var "G")) ($#r1_integra7 :::"is_integral_of"::: ) (Set (Var "g")) "," (Set (Var "X")))) "holds" (Bool (Set (Set (Var "F")) ($#k3_rfunct_1 :::"/"::: ) (Set (Var "G"))) ($#r1_integra7 :::"is_integral_of"::: ) (Set (Set "(" (Set "(" (Set (Var "f")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "G")) ")" ) ($#k47_valued_1 :::"-"::: ) (Set "(" (Set (Var "F")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "g")) ")" ) ")" ) ($#k3_rfunct_1 :::"/"::: ) (Set "(" (Set (Var "G")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "G")) ")" )) "," (Set (Var "X"))))) ; theorem :: INTEGRA7:16 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "b"))) & (Bool (Set ($#k3_integra5 :::"['"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k3_integra5 :::"']"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set ($#k3_integra5 :::"['"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k3_integra5 :::"']"::: ) )) "is" ($#v1_fcont_1 :::"continuous"::: ) ) & (Bool (Set ($#k2_rcomp_1 :::"]."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_rcomp_1 :::".["::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "F")))) & (Bool "(" "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_rcomp_1 :::".["::: ) ))) "holds" (Bool (Set (Set (Var "F")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_integra5 :::"integral"::: ) "(" (Set (Var "f")) "," (Set (Var "a")) "," (Set (Var "x")) ")" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "F")) ($#k1_seq_1 :::"."::: ) (Set (Var "a")) ")" ))) ")" )) "holds" (Bool (Set (Var "F")) ($#r1_integra7 :::"is_integral_of"::: ) (Set (Var "f")) "," (Set ($#k2_rcomp_1 :::"]."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_rcomp_1 :::".["::: ) )))) ; theorem :: INTEGRA7:17 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "x")) "," (Set (Var "x0")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) )) "is" ($#v1_fcont_1 :::"continuous"::: ) ) & (Bool (Set ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_rcomp_1 :::".["::: ) )) & (Bool (Set (Var "x0")) ($#r2_hidden :::"in"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_rcomp_1 :::".["::: ) )) & (Bool (Set (Var "F")) ($#r1_integra7 :::"is_integral_of"::: ) (Set (Var "f")) "," (Set ($#k2_rcomp_1 :::"]."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_rcomp_1 :::".["::: ) ))) "holds" (Bool (Set (Set (Var "F")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_integra5 :::"integral"::: ) "(" (Set (Var "f")) "," (Set (Var "x0")) "," (Set (Var "x")) ")" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "F")) ($#k1_seq_1 :::"."::: ) (Set (Var "x0")) ")" )))))) ; theorem :: INTEGRA7:18 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "b"))) & (Bool (Set ($#k3_integra5 :::"['"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k3_integra5 :::"']"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) & (Bool (Set (Var "F")) ($#r1_integra7 :::"is_integral_of"::: ) (Set (Var "f")) "," (Set (Var "X"))) & (Bool (Set (Var "f")) ($#r1_integra5 :::"is_integrable_on"::: ) (Set ($#k3_integra5 :::"['"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k3_integra5 :::"']"::: ) )) & (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set ($#k3_integra5 :::"['"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k3_integra5 :::"']"::: ) )) "is" ($#v1_comseq_2 :::"bounded"::: ) )) "holds" (Bool (Set (Set (Var "F")) ($#k1_seq_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_integra5 :::"integral"::: ) "(" (Set (Var "f")) "," (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "F")) ($#k1_seq_1 :::"."::: ) (Set (Var "a")) ")" )))))) ; theorem :: INTEGRA7:19 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "b"))) & (Bool (Set ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) & (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) "is" ($#v1_fcont_1 :::"continuous"::: ) )) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set ($#k3_integra5 :::"['"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k3_integra5 :::"']"::: ) )) "is" ($#v1_fcont_1 :::"continuous"::: ) ) & (Bool (Set (Var "f")) ($#r1_integra5 :::"is_integrable_on"::: ) (Set ($#k3_integra5 :::"['"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k3_integra5 :::"']"::: ) )) & (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set ($#k3_integra5 :::"['"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k3_integra5 :::"']"::: ) )) "is" ($#v1_comseq_2 :::"bounded"::: ) ) ")" )))) ; theorem :: INTEGRA7:20 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "b"))) & (Bool (Set ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) & (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) "is" ($#v1_fcont_1 :::"continuous"::: ) ) & (Bool (Set (Var "F")) ($#r1_integra7 :::"is_integral_of"::: ) (Set (Var "f")) "," (Set (Var "X")))) "holds" (Bool (Set (Set (Var "F")) ($#k1_seq_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_integra5 :::"integral"::: ) "(" (Set (Var "f")) "," (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "F")) ($#k1_seq_1 :::"."::: ) (Set (Var "a")) ")" )))))) ; theorem :: INTEGRA7:21 (Bool "for" (Set (Var "b")) "," (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "b")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "a"))) & (Bool (Set ($#k3_integra5 :::"['"::: ) (Set (Var "b")) "," (Set (Var "a")) ($#k3_integra5 :::"']"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) & (Bool (Set (Var "f")) ($#r1_integra5 :::"is_integrable_on"::: ) (Set ($#k3_integra5 :::"['"::: ) (Set (Var "b")) "," (Set (Var "a")) ($#k3_integra5 :::"']"::: ) )) & (Bool (Set (Var "g")) ($#r1_integra5 :::"is_integrable_on"::: ) (Set ($#k3_integra5 :::"['"::: ) (Set (Var "b")) "," (Set (Var "a")) ($#k3_integra5 :::"']"::: ) )) & (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set ($#k3_integra5 :::"['"::: ) (Set (Var "b")) "," (Set (Var "a")) ($#k3_integra5 :::"']"::: ) )) "is" ($#v1_comseq_2 :::"bounded"::: ) ) & (Bool (Set (Set (Var "g")) ($#k2_partfun1 :::"|"::: ) (Set ($#k3_integra5 :::"['"::: ) (Set (Var "b")) "," (Set (Var "a")) ($#k3_integra5 :::"']"::: ) )) "is" ($#v1_comseq_2 :::"bounded"::: ) ) & (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "g")))) & (Bool (Set (Var "F")) ($#r1_integra7 :::"is_integral_of"::: ) (Set (Var "f")) "," (Set (Var "X"))) & (Bool (Set (Var "G")) ($#r1_integra7 :::"is_integral_of"::: ) (Set (Var "g")) "," (Set (Var "X")))) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "F")) ($#k1_seq_1 :::"."::: ) (Set (Var "a")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "G")) ($#k1_seq_1 :::"."::: ) (Set (Var "a")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" (Set (Var "F")) ($#k1_seq_1 :::"."::: ) (Set (Var "b")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "G")) ($#k1_seq_1 :::"."::: ) (Set (Var "b")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_integra5 :::"integral"::: ) "(" (Set "(" (Set (Var "f")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "G")) ")" ) "," (Set (Var "b")) "," (Set (Var "a")) ")" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k4_integra5 :::"integral"::: ) "(" (Set "(" (Set (Var "F")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "g")) ")" ) "," (Set (Var "b")) "," (Set (Var "a")) ")" ")" )))))) ; theorem :: INTEGRA7:22 (Bool "for" (Set (Var "b")) "," (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "b")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "a"))) & (Bool (Set ($#k1_rcomp_1 :::"[."::: ) (Set (Var "b")) "," (Set (Var "a")) ($#k1_rcomp_1 :::".]"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) & (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "g")))) & (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) "is" ($#v1_fcont_1 :::"continuous"::: ) ) & (Bool (Set (Set (Var "g")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) "is" ($#v1_fcont_1 :::"continuous"::: ) ) & (Bool (Set (Var "F")) ($#r1_integra7 :::"is_integral_of"::: ) (Set (Var "f")) "," (Set (Var "X"))) & (Bool (Set (Var "G")) ($#r1_integra7 :::"is_integral_of"::: ) (Set (Var "g")) "," (Set (Var "X")))) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "F")) ($#k1_seq_1 :::"."::: ) (Set (Var "a")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "G")) ($#k1_seq_1 :::"."::: ) (Set (Var "a")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" (Set (Var "F")) ($#k1_seq_1 :::"."::: ) (Set (Var "b")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "G")) ($#k1_seq_1 :::"."::: ) (Set (Var "b")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_integra5 :::"integral"::: ) "(" (Set "(" (Set (Var "f")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "G")) ")" ) "," (Set (Var "b")) "," (Set (Var "a")) ")" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k4_integra5 :::"integral"::: ) "(" (Set "(" (Set (Var "F")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "g")) ")" ) "," (Set (Var "b")) "," (Set (Var "a")) ")" ")" )))))) ; begin theorem :: INTEGRA7:23 (Bool (Set ($#k16_sin_cos :::"sin"::: ) ) ($#r1_integra7 :::"is_integral_of"::: ) (Set ($#k19_sin_cos :::"cos"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) )) ; theorem :: INTEGRA7:24 (Bool "for" (Set (Var "b")) "," (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "b")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "a")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_integra5 :::"integral"::: ) "(" (Set ($#k19_sin_cos :::"cos"::: ) ) "," (Set (Var "a")) "," (Set (Var "b")) ")" ))) ; theorem :: INTEGRA7:25 (Bool (Set (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) ($#k26_valued_1 :::"(#)"::: ) (Set ($#k19_sin_cos :::"cos"::: ) )) ($#r1_integra7 :::"is_integral_of"::: ) (Set ($#k16_sin_cos :::"sin"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) )) ; theorem :: INTEGRA7:26 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "a")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_integra5 :::"integral"::: ) "(" (Set ($#k16_sin_cos :::"sin"::: ) ) "," (Set (Var "a")) "," (Set (Var "b")) ")" ))) ; theorem :: INTEGRA7:27 (Bool (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#r1_integra7 :::"is_integral_of"::: ) (Set ($#k24_sin_cos :::"exp_R"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) )) ; theorem :: INTEGRA7:28 (Bool "for" (Set (Var "b")) "," (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "b")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "a")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_integra5 :::"integral"::: ) "(" (Set ($#k24_sin_cos :::"exp_R"::: ) ) "," (Set (Var "a")) "," (Set (Var "b")) ")" ))) ; theorem :: INTEGRA7:29 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k1_taylor_1 :::"#Z"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_integra7 :::"is_integral_of"::: ) (Set (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k26_valued_1 :::"(#)"::: ) (Set "(" ($#k1_taylor_1 :::"#Z"::: ) (Set (Var "n")) ")" )) "," (Set ($#k1_numbers :::"REAL"::: ) ))) ; theorem :: INTEGRA7:30 (Bool "for" (Set (Var "b")) "," (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" (Set "(" ($#k1_taylor_1 :::"#Z"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "b")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k1_taylor_1 :::"#Z"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "a")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_integra5 :::"integral"::: ) "(" (Set "(" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k26_valued_1 :::"(#)"::: ) (Set "(" ($#k1_taylor_1 :::"#Z"::: ) (Set (Var "n")) ")" ) ")" ) "," (Set (Var "a")) "," (Set (Var "b")) ")" )))) ; begin theorem :: INTEGRA7:31 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "rseq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "b"))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Set (Var "H")) ($#k1_seqfunc :::"."::: ) (Set (Var "n"))) ($#r1_integra5 :::"is_integrable_on"::: ) (Set ($#k3_integra5 :::"['"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k3_integra5 :::"']"::: ) )) & (Bool (Set (Set "(" (Set (Var "H")) ($#k1_seqfunc :::"."::: ) (Set (Var "n")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set ($#k3_integra5 :::"['"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k3_integra5 :::"']"::: ) )) "is" ($#v1_comseq_2 :::"bounded"::: ) ) & (Bool (Set (Set (Var "rseq")) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k4_integra5 :::"integral"::: ) "(" (Set "(" (Set (Var "H")) ($#k1_seqfunc :::"."::: ) (Set (Var "n")) ")" ) "," (Set (Var "a")) "," (Set (Var "b")) ")" )) ")" ) ")" ) & (Bool (Set (Var "H")) ($#r3_seqfunc :::"is_unif_conv_on"::: ) (Set ($#k3_integra5 :::"['"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k3_integra5 :::"']"::: ) ))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k11_seqfunc :::"lim"::: ) "(" (Set (Var "H")) "," (Set ($#k3_integra5 :::"['"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k3_integra5 :::"']"::: ) ) ")" ")" ) ($#k2_partfun1 :::"|"::: ) (Set ($#k3_integra5 :::"['"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k3_integra5 :::"']"::: ) )) "is" ($#v1_comseq_2 :::"bounded"::: ) ) & (Bool (Set ($#k11_seqfunc :::"lim"::: ) "(" (Set (Var "H")) "," (Set ($#k3_integra5 :::"['"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k3_integra5 :::"']"::: ) ) ")" ) ($#r1_integra5 :::"is_integrable_on"::: ) (Set ($#k3_integra5 :::"['"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k3_integra5 :::"']"::: ) )) & (Bool (Set (Var "rseq")) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set (Var "rseq"))) ($#r1_hidden :::"="::: ) (Set ($#k4_integra5 :::"integral"::: ) "(" (Set "(" ($#k11_seqfunc :::"lim"::: ) "(" (Set (Var "H")) "," (Set ($#k3_integra5 :::"['"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k3_integra5 :::"']"::: ) ) ")" ")" ) "," (Set (Var "a")) "," (Set (Var "b")) ")" )) ")" )))) ;