:: INTEGR10 semantic presentation begin theorem :: INTEGR10:1 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "g1")) "," (Set (Var "M")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "b"))) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "g1"))) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "M")))) "holds" (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "b"))) & (Bool (Set (Set "(" (Set (Var "b")) ($#k5_real_1 :::"-"::: ) (Set (Var "r")) ")" ) ($#k8_real_1 :::"*"::: ) (Set (Var "M"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "g1"))) ")" ))) ; theorem :: INTEGR10:2 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "g1")) "," (Set (Var "M")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "b"))) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "g1"))) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "M")))) "holds" (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "b"))) & (Bool (Set (Set "(" (Set (Var "r")) ($#k9_real_1 :::"-"::: ) (Set (Var "a")) ")" ) ($#k8_real_1 :::"*"::: ) (Set (Var "M"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "g1"))) ")" ))) ; theorem :: INTEGR10:3 (Bool "for" (Set (Var "b")) "," (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "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")) ")" ))) ; begin definitionlet "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ); let "a", "b" be ($#m1_subset_1 :::"Real":::); pred "f" :::"is_right_ext_Riemann_integrable_on"::: "a" "," "b" means :: INTEGR10:def 1 (Bool "(" (Bool "(" "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool "a" ($#r1_xxreal_0 :::"<="::: ) (Set (Var "d"))) & (Bool (Set (Var "d")) ($#r1_xxreal_0 :::"<"::: ) "b")) "holds" (Bool "(" (Bool "f" ($#r1_integra5 :::"is_integrable_on"::: ) (Set ($#k3_integra5 :::"['"::: ) "a" "," (Set (Var "d")) ($#k3_integra5 :::"']"::: ) )) & (Bool (Set "f" ($#k2_partfun1 :::"|"::: ) (Set ($#k3_integra5 :::"['"::: ) "a" "," (Set (Var "d")) ($#k3_integra5 :::"']"::: ) )) "is" ($#v1_comseq_2 :::"bounded"::: ) ) ")" ) ")" ) & (Bool "ex" (Set (Var "Intf")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "Intf"))) ($#r1_hidden :::"="::: ) (Set ($#k3_rcomp_1 :::"[."::: ) "a" "," "b" ($#k3_rcomp_1 :::".["::: ) )) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "Intf"))))) "holds" (Bool (Set (Set (Var "Intf")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_integra5 :::"integral"::: ) "(" "f" "," "a" "," (Set (Var "x")) ")" )) ")" ) & (Bool (Set (Var "Intf")) ($#r1_limfunc2 :::"is_left_convergent_in"::: ) "b") ")" )) ")" ); end; :: deftheorem defines :::"is_right_ext_Riemann_integrable_on"::: INTEGR10:def 1 : (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_integr10 :::"is_right_ext_Riemann_integrable_on"::: ) (Set (Var "a")) "," (Set (Var "b"))) "iff" (Bool "(" (Bool "(" "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "d"))) & (Bool (Set (Var "d")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "b")))) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_integra5 :::"is_integrable_on"::: ) (Set ($#k3_integra5 :::"['"::: ) (Set (Var "a")) "," (Set (Var "d")) ($#k3_integra5 :::"']"::: ) )) & (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set ($#k3_integra5 :::"['"::: ) (Set (Var "a")) "," (Set (Var "d")) ($#k3_integra5 :::"']"::: ) )) "is" ($#v1_comseq_2 :::"bounded"::: ) ) ")" ) ")" ) & (Bool "ex" (Set (Var "Intf")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "Intf"))) ($#r1_hidden :::"="::: ) (Set ($#k3_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k3_rcomp_1 :::".["::: ) )) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "Intf"))))) "holds" (Bool (Set (Set (Var "Intf")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_integra5 :::"integral"::: ) "(" (Set (Var "f")) "," (Set (Var "a")) "," (Set (Var "x")) ")" )) ")" ) & (Bool (Set (Var "Intf")) ($#r1_limfunc2 :::"is_left_convergent_in"::: ) (Set (Var "b"))) ")" )) ")" ) ")" ))); definitionlet "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ); let "a", "b" be ($#m1_subset_1 :::"Real":::); pred "f" :::"is_left_ext_Riemann_integrable_on"::: "a" "," "b" means :: INTEGR10:def 2 (Bool "(" (Bool "(" "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool "a" ($#r1_xxreal_0 :::"<"::: ) (Set (Var "d"))) & (Bool (Set (Var "d")) ($#r1_xxreal_0 :::"<="::: ) "b")) "holds" (Bool "(" (Bool "f" ($#r1_integra5 :::"is_integrable_on"::: ) (Set ($#k3_integra5 :::"['"::: ) (Set (Var "d")) "," "b" ($#k3_integra5 :::"']"::: ) )) & (Bool (Set "f" ($#k2_partfun1 :::"|"::: ) (Set ($#k3_integra5 :::"['"::: ) (Set (Var "d")) "," "b" ($#k3_integra5 :::"']"::: ) )) "is" ($#v1_comseq_2 :::"bounded"::: ) ) ")" ) ")" ) & (Bool "ex" (Set (Var "Intf")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "Intf"))) ($#r1_hidden :::"="::: ) (Set ($#k4_rcomp_1 :::"]."::: ) "a" "," "b" ($#k4_rcomp_1 :::".]"::: ) )) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "Intf"))))) "holds" (Bool (Set (Set (Var "Intf")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_integra5 :::"integral"::: ) "(" "f" "," (Set (Var "x")) "," "b" ")" )) ")" ) & (Bool (Set (Var "Intf")) ($#r4_limfunc2 :::"is_right_convergent_in"::: ) "a") ")" )) ")" ); end; :: deftheorem defines :::"is_left_ext_Riemann_integrable_on"::: INTEGR10:def 2 : (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_integr10 :::"is_left_ext_Riemann_integrable_on"::: ) (Set (Var "a")) "," (Set (Var "b"))) "iff" (Bool "(" (Bool "(" "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "d"))) & (Bool (Set (Var "d")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "b")))) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_integra5 :::"is_integrable_on"::: ) (Set ($#k3_integra5 :::"['"::: ) (Set (Var "d")) "," (Set (Var "b")) ($#k3_integra5 :::"']"::: ) )) & (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set ($#k3_integra5 :::"['"::: ) (Set (Var "d")) "," (Set (Var "b")) ($#k3_integra5 :::"']"::: ) )) "is" ($#v1_comseq_2 :::"bounded"::: ) ) ")" ) ")" ) & (Bool "ex" (Set (Var "Intf")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "Intf"))) ($#r1_hidden :::"="::: ) (Set ($#k4_rcomp_1 :::"]."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_rcomp_1 :::".]"::: ) )) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "Intf"))))) "holds" (Bool (Set (Set (Var "Intf")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_integra5 :::"integral"::: ) "(" (Set (Var "f")) "," (Set (Var "x")) "," (Set (Var "b")) ")" )) ")" ) & (Bool (Set (Var "Intf")) ($#r4_limfunc2 :::"is_right_convergent_in"::: ) (Set (Var "a"))) ")" )) ")" ) ")" ))); definitionlet "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ); let "a", "b" be ($#m1_subset_1 :::"Real":::); assume (Bool (Set (Const "f")) ($#r1_integr10 :::"is_right_ext_Riemann_integrable_on"::: ) (Set (Const "a")) "," (Set (Const "b"))) ; func :::"ext_right_integral"::: "(" "f" "," "a" "," "b" ")" -> ($#m1_subset_1 :::"Real":::) means :: INTEGR10:def 3 (Bool "ex" (Set (Var "Intf")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "Intf"))) ($#r1_hidden :::"="::: ) (Set ($#k3_rcomp_1 :::"[."::: ) "a" "," "b" ($#k3_rcomp_1 :::".["::: ) )) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "Intf"))))) "holds" (Bool (Set (Set (Var "Intf")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_integra5 :::"integral"::: ) "(" "f" "," "a" "," (Set (Var "x")) ")" )) ")" ) & (Bool (Set (Var "Intf")) ($#r1_limfunc2 :::"is_left_convergent_in"::: ) "b") & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k1_limfunc2 :::"lim_left"::: ) "(" (Set (Var "Intf")) "," "b" ")" )) ")" )); end; :: deftheorem defines :::"ext_right_integral"::: INTEGR10:def 3 : (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "f")) ($#r1_integr10 :::"is_right_ext_Riemann_integrable_on"::: ) (Set (Var "a")) "," (Set (Var "b")))) "holds" (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k1_integr10 :::"ext_right_integral"::: ) "(" (Set (Var "f")) "," (Set (Var "a")) "," (Set (Var "b")) ")" )) "iff" (Bool "ex" (Set (Var "Intf")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "Intf"))) ($#r1_hidden :::"="::: ) (Set ($#k3_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k3_rcomp_1 :::".["::: ) )) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "Intf"))))) "holds" (Bool (Set (Set (Var "Intf")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_integra5 :::"integral"::: ) "(" (Set (Var "f")) "," (Set (Var "a")) "," (Set (Var "x")) ")" )) ")" ) & (Bool (Set (Var "Intf")) ($#r1_limfunc2 :::"is_left_convergent_in"::: ) (Set (Var "b"))) & (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k1_limfunc2 :::"lim_left"::: ) "(" (Set (Var "Intf")) "," (Set (Var "b")) ")" )) ")" )) ")" )))); definitionlet "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ); let "a", "b" be ($#m1_subset_1 :::"Real":::); assume (Bool (Set (Const "f")) ($#r2_integr10 :::"is_left_ext_Riemann_integrable_on"::: ) (Set (Const "a")) "," (Set (Const "b"))) ; func :::"ext_left_integral"::: "(" "f" "," "a" "," "b" ")" -> ($#m1_subset_1 :::"Real":::) means :: INTEGR10:def 4 (Bool "ex" (Set (Var "Intf")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "Intf"))) ($#r1_hidden :::"="::: ) (Set ($#k4_rcomp_1 :::"]."::: ) "a" "," "b" ($#k4_rcomp_1 :::".]"::: ) )) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "Intf"))))) "holds" (Bool (Set (Set (Var "Intf")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_integra5 :::"integral"::: ) "(" "f" "," (Set (Var "x")) "," "b" ")" )) ")" ) & (Bool (Set (Var "Intf")) ($#r4_limfunc2 :::"is_right_convergent_in"::: ) "a") & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k2_limfunc2 :::"lim_right"::: ) "(" (Set (Var "Intf")) "," "a" ")" )) ")" )); end; :: deftheorem defines :::"ext_left_integral"::: INTEGR10:def 4 : (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "f")) ($#r2_integr10 :::"is_left_ext_Riemann_integrable_on"::: ) (Set (Var "a")) "," (Set (Var "b")))) "holds" (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k2_integr10 :::"ext_left_integral"::: ) "(" (Set (Var "f")) "," (Set (Var "a")) "," (Set (Var "b")) ")" )) "iff" (Bool "ex" (Set (Var "Intf")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "Intf"))) ($#r1_hidden :::"="::: ) (Set ($#k4_rcomp_1 :::"]."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_rcomp_1 :::".]"::: ) )) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "Intf"))))) "holds" (Bool (Set (Set (Var "Intf")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_integra5 :::"integral"::: ) "(" (Set (Var "f")) "," (Set (Var "x")) "," (Set (Var "b")) ")" )) ")" ) & (Bool (Set (Var "Intf")) ($#r4_limfunc2 :::"is_right_convergent_in"::: ) (Set (Var "a"))) & (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k2_limfunc2 :::"lim_right"::: ) "(" (Set (Var "Intf")) "," (Set (Var "a")) ")" )) ")" )) ")" )))); definitionlet "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ); let "a" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; pred "f" :::"is_+infty_ext_Riemann_integrable_on"::: "a" means :: INTEGR10:def 5 (Bool "(" (Bool "(" "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool "a" ($#r1_xxreal_0 :::"<="::: ) (Set (Var "b")))) "holds" (Bool "(" (Bool "f" ($#r1_integra5 :::"is_integrable_on"::: ) (Set ($#k3_integra5 :::"['"::: ) "a" "," (Set (Var "b")) ($#k3_integra5 :::"']"::: ) )) & (Bool (Set "f" ($#k2_partfun1 :::"|"::: ) (Set ($#k3_integra5 :::"['"::: ) "a" "," (Set (Var "b")) ($#k3_integra5 :::"']"::: ) )) "is" ($#v1_comseq_2 :::"bounded"::: ) ) ")" ) ")" ) & (Bool "ex" (Set (Var "Intf")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "Intf"))) ($#r1_hidden :::"="::: ) (Set ($#k2_limfunc1 :::"right_closed_halfline"::: ) "a")) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "Intf"))))) "holds" (Bool (Set (Set (Var "Intf")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_integra5 :::"integral"::: ) "(" "f" "," "a" "," (Set (Var "x")) ")" )) ")" ) & (Bool (Set (Var "Intf")) "is" ($#v3_limfunc1 :::"convergent_in+infty"::: ) ) ")" )) ")" ); end; :: deftheorem defines :::"is_+infty_ext_Riemann_integrable_on"::: INTEGR10:def 5 : (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r3_integr10 :::"is_+infty_ext_Riemann_integrable_on"::: ) (Set (Var "a"))) "iff" (Bool "(" (Bool "(" "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "b")))) "holds" (Bool "(" (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"::: ) ) ")" ) ")" ) & (Bool "ex" (Set (Var "Intf")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "Intf"))) ($#r1_hidden :::"="::: ) (Set ($#k2_limfunc1 :::"right_closed_halfline"::: ) (Set (Var "a")))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "Intf"))))) "holds" (Bool (Set (Set (Var "Intf")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_integra5 :::"integral"::: ) "(" (Set (Var "f")) "," (Set (Var "a")) "," (Set (Var "x")) ")" )) ")" ) & (Bool (Set (Var "Intf")) "is" ($#v3_limfunc1 :::"convergent_in+infty"::: ) ) ")" )) ")" ) ")" ))); definitionlet "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ); let "b" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; pred "f" :::"is_-infty_ext_Riemann_integrable_on"::: "b" means :: INTEGR10:def 6 (Bool "(" (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<="::: ) "b")) "holds" (Bool "(" (Bool "f" ($#r1_integra5 :::"is_integrable_on"::: ) (Set ($#k3_integra5 :::"['"::: ) (Set (Var "a")) "," "b" ($#k3_integra5 :::"']"::: ) )) & (Bool (Set "f" ($#k2_partfun1 :::"|"::: ) (Set ($#k3_integra5 :::"['"::: ) (Set (Var "a")) "," "b" ($#k3_integra5 :::"']"::: ) )) "is" ($#v1_comseq_2 :::"bounded"::: ) ) ")" ) ")" ) & (Bool "ex" (Set (Var "Intf")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "Intf"))) ($#r1_hidden :::"="::: ) (Set ($#k1_limfunc1 :::"left_closed_halfline"::: ) "b")) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "Intf"))))) "holds" (Bool (Set (Set (Var "Intf")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_integra5 :::"integral"::: ) "(" "f" "," (Set (Var "x")) "," "b" ")" )) ")" ) & (Bool (Set (Var "Intf")) "is" ($#v6_limfunc1 :::"convergent_in-infty"::: ) ) ")" )) ")" ); end; :: deftheorem defines :::"is_-infty_ext_Riemann_integrable_on"::: INTEGR10:def 6 : (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r4_integr10 :::"is_-infty_ext_Riemann_integrable_on"::: ) (Set (Var "b"))) "iff" (Bool "(" (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "b")))) "holds" (Bool "(" (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"::: ) ) ")" ) ")" ) & (Bool "ex" (Set (Var "Intf")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "Intf"))) ($#r1_hidden :::"="::: ) (Set ($#k1_limfunc1 :::"left_closed_halfline"::: ) (Set (Var "b")))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "Intf"))))) "holds" (Bool (Set (Set (Var "Intf")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_integra5 :::"integral"::: ) "(" (Set (Var "f")) "," (Set (Var "x")) "," (Set (Var "b")) ")" )) ")" ) & (Bool (Set (Var "Intf")) "is" ($#v6_limfunc1 :::"convergent_in-infty"::: ) ) ")" )) ")" ) ")" ))); definitionlet "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ); let "a" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; assume (Bool (Set (Const "f")) ($#r3_integr10 :::"is_+infty_ext_Riemann_integrable_on"::: ) (Set (Const "a"))) ; func :::"infty_ext_right_integral"::: "(" "f" "," "a" ")" -> ($#m1_subset_1 :::"Real":::) means :: INTEGR10:def 7 (Bool "ex" (Set (Var "Intf")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "Intf"))) ($#r1_hidden :::"="::: ) (Set ($#k2_limfunc1 :::"right_closed_halfline"::: ) "a")) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "Intf"))))) "holds" (Bool (Set (Set (Var "Intf")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_integra5 :::"integral"::: ) "(" "f" "," "a" "," (Set (Var "x")) ")" )) ")" ) & (Bool (Set (Var "Intf")) "is" ($#v3_limfunc1 :::"convergent_in+infty"::: ) ) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k4_limfunc1 :::"lim_in+infty"::: ) (Set (Var "Intf")))) ")" )); end; :: deftheorem defines :::"infty_ext_right_integral"::: INTEGR10:def 7 : (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "f")) ($#r3_integr10 :::"is_+infty_ext_Riemann_integrable_on"::: ) (Set (Var "a")))) "holds" (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k3_integr10 :::"infty_ext_right_integral"::: ) "(" (Set (Var "f")) "," (Set (Var "a")) ")" )) "iff" (Bool "ex" (Set (Var "Intf")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "Intf"))) ($#r1_hidden :::"="::: ) (Set ($#k2_limfunc1 :::"right_closed_halfline"::: ) (Set (Var "a")))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "Intf"))))) "holds" (Bool (Set (Set (Var "Intf")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_integra5 :::"integral"::: ) "(" (Set (Var "f")) "," (Set (Var "a")) "," (Set (Var "x")) ")" )) ")" ) & (Bool (Set (Var "Intf")) "is" ($#v3_limfunc1 :::"convergent_in+infty"::: ) ) & (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k4_limfunc1 :::"lim_in+infty"::: ) (Set (Var "Intf")))) ")" )) ")" )))); definitionlet "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ); let "b" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; assume (Bool (Set (Const "f")) ($#r4_integr10 :::"is_-infty_ext_Riemann_integrable_on"::: ) (Set (Const "b"))) ; func :::"infty_ext_left_integral"::: "(" "f" "," "b" ")" -> ($#m1_subset_1 :::"Real":::) means :: INTEGR10:def 8 (Bool "ex" (Set (Var "Intf")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "Intf"))) ($#r1_hidden :::"="::: ) (Set ($#k1_limfunc1 :::"left_closed_halfline"::: ) "b")) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "Intf"))))) "holds" (Bool (Set (Set (Var "Intf")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_integra5 :::"integral"::: ) "(" "f" "," (Set (Var "x")) "," "b" ")" )) ")" ) & (Bool (Set (Var "Intf")) "is" ($#v6_limfunc1 :::"convergent_in-infty"::: ) ) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k5_limfunc1 :::"lim_in-infty"::: ) (Set (Var "Intf")))) ")" )); end; :: deftheorem defines :::"infty_ext_left_integral"::: INTEGR10:def 8 : (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "f")) ($#r4_integr10 :::"is_-infty_ext_Riemann_integrable_on"::: ) (Set (Var "b")))) "holds" (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k4_integr10 :::"infty_ext_left_integral"::: ) "(" (Set (Var "f")) "," (Set (Var "b")) ")" )) "iff" (Bool "ex" (Set (Var "Intf")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "Intf"))) ($#r1_hidden :::"="::: ) (Set ($#k1_limfunc1 :::"left_closed_halfline"::: ) (Set (Var "b")))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "Intf"))))) "holds" (Bool (Set (Set (Var "Intf")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_integra5 :::"integral"::: ) "(" (Set (Var "f")) "," (Set (Var "x")) "," (Set (Var "b")) ")" )) ")" ) & (Bool (Set (Var "Intf")) "is" ($#v6_limfunc1 :::"convergent_in-infty"::: ) ) & (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k5_limfunc1 :::"lim_in-infty"::: ) (Set (Var "Intf")))) ")" )) ")" )))); definitionlet "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ); attr "f" is :::"infty_ext_Riemann_integrable"::: means :: INTEGR10:def 9 (Bool "(" (Bool "f" ($#r3_integr10 :::"is_+infty_ext_Riemann_integrable_on"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "f" ($#r4_integr10 :::"is_-infty_ext_Riemann_integrable_on"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ); end; :: deftheorem defines :::"infty_ext_Riemann_integrable"::: INTEGR10:def 9 : (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v1_integr10 :::"infty_ext_Riemann_integrable"::: ) ) "iff" (Bool "(" (Bool (Set (Var "f")) ($#r3_integr10 :::"is_+infty_ext_Riemann_integrable_on"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "f")) ($#r4_integr10 :::"is_-infty_ext_Riemann_integrable_on"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" )); definitionlet "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ); func :::"infty_ext_integral"::: "f" -> ($#m1_subset_1 :::"Real":::) equals :: INTEGR10:def 10 (Set (Set "(" ($#k3_integr10 :::"infty_ext_right_integral"::: ) "(" "f" "," (Set ($#k6_numbers :::"0"::: ) ) ")" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k4_integr10 :::"infty_ext_left_integral"::: ) "(" "f" "," (Set ($#k6_numbers :::"0"::: ) ) ")" ")" )); end; :: deftheorem defines :::"infty_ext_integral"::: INTEGR10:def 10 : (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k5_integr10 :::"infty_ext_integral"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_integr10 :::"infty_ext_right_integral"::: ) "(" (Set (Var "f")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k4_integr10 :::"infty_ext_left_integral"::: ) "(" (Set (Var "f")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ")" )))); begin theorem :: INTEGR10:4 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"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 ($#k3_integra5 :::"['"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k3_integra5 :::"']"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "g")))) & (Bool (Set (Var "f")) ($#r1_integr10 :::"is_right_ext_Riemann_integrable_on"::: ) (Set (Var "a")) "," (Set (Var "b"))) & (Bool (Set (Var "g")) ($#r1_integr10 :::"is_right_ext_Riemann_integrable_on"::: ) (Set (Var "a")) "," (Set (Var "b")))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k3_valued_1 :::"+"::: ) (Set (Var "g"))) ($#r1_integr10 :::"is_right_ext_Riemann_integrable_on"::: ) (Set (Var "a")) "," (Set (Var "b"))) & (Bool (Set ($#k1_integr10 :::"ext_right_integral"::: ) "(" (Set "(" (Set (Var "f")) ($#k3_valued_1 :::"+"::: ) (Set (Var "g")) ")" ) "," (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_integr10 :::"ext_right_integral"::: ) "(" (Set (Var "f")) "," (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k1_integr10 :::"ext_right_integral"::: ) "(" (Set (Var "g")) "," (Set (Var "a")) "," (Set (Var "b")) ")" ")" ))) ")" ))) ; theorem :: INTEGR10:5 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"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 (Var "f")) ($#r1_integr10 :::"is_right_ext_Riemann_integrable_on"::: ) (Set (Var "a")) "," (Set (Var "b")))) "holds" (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" (Bool (Set (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f"))) ($#r1_integr10 :::"is_right_ext_Riemann_integrable_on"::: ) (Set (Var "a")) "," (Set (Var "b"))) & (Bool (Set ($#k1_integr10 :::"ext_right_integral"::: ) "(" (Set "(" (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f")) ")" ) "," (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k1_integr10 :::"ext_right_integral"::: ) "(" (Set (Var "f")) "," (Set (Var "a")) "," (Set (Var "b")) ")" ")" ))) ")" )))) ; theorem :: INTEGR10:6 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"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 ($#k3_integra5 :::"['"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k3_integra5 :::"']"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "g")))) & (Bool (Set (Var "f")) ($#r2_integr10 :::"is_left_ext_Riemann_integrable_on"::: ) (Set (Var "a")) "," (Set (Var "b"))) & (Bool (Set (Var "g")) ($#r2_integr10 :::"is_left_ext_Riemann_integrable_on"::: ) (Set (Var "a")) "," (Set (Var "b")))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k3_valued_1 :::"+"::: ) (Set (Var "g"))) ($#r2_integr10 :::"is_left_ext_Riemann_integrable_on"::: ) (Set (Var "a")) "," (Set (Var "b"))) & (Bool (Set ($#k2_integr10 :::"ext_left_integral"::: ) "(" (Set "(" (Set (Var "f")) ($#k3_valued_1 :::"+"::: ) (Set (Var "g")) ")" ) "," (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_integr10 :::"ext_left_integral"::: ) "(" (Set (Var "f")) "," (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k2_integr10 :::"ext_left_integral"::: ) "(" (Set (Var "g")) "," (Set (Var "a")) "," (Set (Var "b")) ")" ")" ))) ")" ))) ; theorem :: INTEGR10:7 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"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 (Var "f")) ($#r2_integr10 :::"is_left_ext_Riemann_integrable_on"::: ) (Set (Var "a")) "," (Set (Var "b")))) "holds" (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" (Bool (Set (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f"))) ($#r2_integr10 :::"is_left_ext_Riemann_integrable_on"::: ) (Set (Var "a")) "," (Set (Var "b"))) & (Bool (Set ($#k2_integr10 :::"ext_left_integral"::: ) "(" (Set "(" (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f")) ")" ) "," (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k2_integr10 :::"ext_left_integral"::: ) "(" (Set (Var "f")) "," (Set (Var "a")) "," (Set (Var "b")) ")" ")" ))) ")" )))) ; theorem :: INTEGR10:8 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k2_limfunc1 :::"right_closed_halfline"::: ) (Set (Var "a"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set ($#k2_limfunc1 :::"right_closed_halfline"::: ) (Set (Var "a"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "g")))) & (Bool (Set (Var "f")) ($#r3_integr10 :::"is_+infty_ext_Riemann_integrable_on"::: ) (Set (Var "a"))) & (Bool (Set (Var "g")) ($#r3_integr10 :::"is_+infty_ext_Riemann_integrable_on"::: ) (Set (Var "a")))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k3_valued_1 :::"+"::: ) (Set (Var "g"))) ($#r3_integr10 :::"is_+infty_ext_Riemann_integrable_on"::: ) (Set (Var "a"))) & (Bool (Set ($#k3_integr10 :::"infty_ext_right_integral"::: ) "(" (Set "(" (Set (Var "f")) ($#k3_valued_1 :::"+"::: ) (Set (Var "g")) ")" ) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_integr10 :::"infty_ext_right_integral"::: ) "(" (Set (Var "f")) "," (Set (Var "a")) ")" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k3_integr10 :::"infty_ext_right_integral"::: ) "(" (Set (Var "g")) "," (Set (Var "a")) ")" ")" ))) ")" ))) ; theorem :: INTEGR10:9 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k2_limfunc1 :::"right_closed_halfline"::: ) (Set (Var "a"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "f")) ($#r3_integr10 :::"is_+infty_ext_Riemann_integrable_on"::: ) (Set (Var "a")))) "holds" (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" (Bool (Set (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f"))) ($#r3_integr10 :::"is_+infty_ext_Riemann_integrable_on"::: ) (Set (Var "a"))) & (Bool (Set ($#k3_integr10 :::"infty_ext_right_integral"::: ) "(" (Set "(" (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f")) ")" ) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k3_integr10 :::"infty_ext_right_integral"::: ) "(" (Set (Var "f")) "," (Set (Var "a")) ")" ")" ))) ")" )))) ; theorem :: INTEGR10:10 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k1_limfunc1 :::"left_closed_halfline"::: ) (Set (Var "b"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set ($#k1_limfunc1 :::"left_closed_halfline"::: ) (Set (Var "b"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "g")))) & (Bool (Set (Var "f")) ($#r4_integr10 :::"is_-infty_ext_Riemann_integrable_on"::: ) (Set (Var "b"))) & (Bool (Set (Var "g")) ($#r4_integr10 :::"is_-infty_ext_Riemann_integrable_on"::: ) (Set (Var "b")))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k3_valued_1 :::"+"::: ) (Set (Var "g"))) ($#r4_integr10 :::"is_-infty_ext_Riemann_integrable_on"::: ) (Set (Var "b"))) & (Bool (Set ($#k4_integr10 :::"infty_ext_left_integral"::: ) "(" (Set "(" (Set (Var "f")) ($#k3_valued_1 :::"+"::: ) (Set (Var "g")) ")" ) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_integr10 :::"infty_ext_left_integral"::: ) "(" (Set (Var "f")) "," (Set (Var "b")) ")" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k4_integr10 :::"infty_ext_left_integral"::: ) "(" (Set (Var "g")) "," (Set (Var "b")) ")" ")" ))) ")" ))) ; theorem :: INTEGR10:11 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k1_limfunc1 :::"left_closed_halfline"::: ) (Set (Var "b"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "f")) ($#r4_integr10 :::"is_-infty_ext_Riemann_integrable_on"::: ) (Set (Var "b")))) "holds" (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" (Bool (Set (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f"))) ($#r4_integr10 :::"is_-infty_ext_Riemann_integrable_on"::: ) (Set (Var "b"))) & (Bool (Set ($#k4_integr10 :::"infty_ext_left_integral"::: ) "(" (Set "(" (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f")) ")" ) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k4_integr10 :::"infty_ext_left_integral"::: ) "(" (Set (Var "f")) "," (Set (Var "b")) ")" ")" ))) ")" )))) ; theorem :: INTEGR10:12 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"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 (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 ($#k1_integr10 :::"ext_right_integral"::: ) "(" (Set (Var "f")) "," (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_integra5 :::"integral"::: ) "(" (Set (Var "f")) "," (Set (Var "a")) "," (Set (Var "b")) ")" )))) ; theorem :: INTEGR10:13 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"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 (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 ($#k2_integr10 :::"ext_left_integral"::: ) "(" (Set (Var "f")) "," (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_integra5 :::"integral"::: ) "(" (Set (Var "f")) "," (Set (Var "a")) "," (Set (Var "b")) ")" )))) ; begin definitionlet "s" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; func :::"exp*-"::: "s" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) means :: INTEGR10:def 11 (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set it ($#k1_seq_1 :::"."::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" "s" ($#k4_real_1 :::"*"::: ) (Set (Var "t")) ")" ) ")" )))); end; :: deftheorem defines :::"exp*-"::: INTEGR10:def 11 : (Bool "for" (Set (Var "s")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k6_integr10 :::"exp*-"::: ) (Set (Var "s")))) "iff" (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set (Set (Var "b2")) ($#k1_seq_1 :::"."::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set (Var "s")) ($#k4_real_1 :::"*"::: ) (Set (Var "t")) ")" ) ")" )))) ")" ))); definitionlet "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ); func :::"One-sided_Laplace_transform"::: "f" -> ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) means :: INTEGR10:def 12 (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k3_limfunc1 :::"right_open_halfline"::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (Bool "(" "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) it))) "holds" (Bool (Set it ($#k1_seq_1 :::"."::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k3_integr10 :::"infty_ext_right_integral"::: ) "(" (Set "(" "f" ($#k20_valued_1 :::"(#)"::: ) (Set "(" ($#k6_integr10 :::"exp*-"::: ) (Set (Var "s")) ")" ) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ")" )) ")" ) ")" ); end; :: deftheorem defines :::"One-sided_Laplace_transform"::: INTEGR10:def 12 : (Bool "for" (Set (Var "f")) "," (Set (Var "b2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k7_integr10 :::"One-sided_Laplace_transform"::: ) (Set (Var "f")))) "iff" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k3_limfunc1 :::"right_open_halfline"::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (Bool "(" "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "b2"))))) "holds" (Bool (Set (Set (Var "b2")) ($#k1_seq_1 :::"."::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k3_integr10 :::"infty_ext_right_integral"::: ) "(" (Set "(" (Set (Var "f")) ($#k20_valued_1 :::"(#)"::: ) (Set "(" ($#k6_integr10 :::"exp*-"::: ) (Set (Var "s")) ")" ) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ")" )) ")" ) ")" ) ")" )); begin theorem :: INTEGR10:14 (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 ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k2_limfunc1 :::"right_closed_halfline"::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k2_limfunc1 :::"right_closed_halfline"::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (Bool "(" "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set ($#k3_limfunc1 :::"right_open_halfline"::: ) (Set ($#k6_numbers :::"0"::: ) )))) "holds" (Bool (Set (Set (Var "f")) ($#k20_valued_1 :::"(#)"::: ) (Set "(" ($#k6_integr10 :::"exp*-"::: ) (Set (Var "s")) ")" )) ($#r3_integr10 :::"is_+infty_ext_Riemann_integrable_on"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) & (Bool "(" "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set ($#k3_limfunc1 :::"right_open_halfline"::: ) (Set ($#k6_numbers :::"0"::: ) )))) "holds" (Bool (Set (Set (Var "g")) ($#k20_valued_1 :::"(#)"::: ) (Set "(" ($#k6_integr10 :::"exp*-"::: ) (Set (Var "s")) ")" )) ($#r3_integr10 :::"is_+infty_ext_Riemann_integrable_on"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) "holds" (Bool "(" (Bool "(" "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set ($#k3_limfunc1 :::"right_open_halfline"::: ) (Set ($#k6_numbers :::"0"::: ) )))) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k3_valued_1 :::"+"::: ) (Set (Var "g")) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set "(" ($#k6_integr10 :::"exp*-"::: ) (Set (Var "s")) ")" )) ($#r3_integr10 :::"is_+infty_ext_Riemann_integrable_on"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) & (Bool (Set ($#k7_integr10 :::"One-sided_Laplace_transform"::: ) (Set "(" (Set (Var "f")) ($#k3_valued_1 :::"+"::: ) (Set (Var "g")) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set "(" ($#k7_integr10 :::"One-sided_Laplace_transform"::: ) (Set (Var "f")) ")" ) ($#k3_valued_1 :::"+"::: ) (Set "(" ($#k7_integr10 :::"One-sided_Laplace_transform"::: ) (Set (Var "g")) ")" ))) ")" )) ; theorem :: INTEGR10:15 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k2_limfunc1 :::"right_closed_halfline"::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (Bool "(" "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set ($#k3_limfunc1 :::"right_open_halfline"::: ) (Set ($#k6_numbers :::"0"::: ) )))) "holds" (Bool (Set (Set (Var "f")) ($#k20_valued_1 :::"(#)"::: ) (Set "(" ($#k6_integr10 :::"exp*-"::: ) (Set (Var "s")) ")" )) ($#r3_integr10 :::"is_+infty_ext_Riemann_integrable_on"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) "holds" (Bool "(" (Bool "(" "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set ($#k3_limfunc1 :::"right_open_halfline"::: ) (Set ($#k6_numbers :::"0"::: ) )))) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f")) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set "(" ($#k6_integr10 :::"exp*-"::: ) (Set (Var "s")) ")" )) ($#r3_integr10 :::"is_+infty_ext_Riemann_integrable_on"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) & (Bool (Set ($#k7_integr10 :::"One-sided_Laplace_transform"::: ) (Set "(" (Set (Var "a")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f")) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "a")) ($#k26_valued_1 :::"(#)"::: ) (Set "(" ($#k7_integr10 :::"One-sided_Laplace_transform"::: ) (Set (Var "f")) ")" ))) ")" ))) ;