:: INTEGRA5  semantic presentation begin  























theorem :: INTEGRA5:1 (Bool  "for" (Set (Var "F")) "," (Set (Var "F1")) "," (Set (Var "F2")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  )  (Bool  "for" (Set (Var "r1")) "," (Set (Var "r2")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool  "("  (Bool (Set (Var "F1"))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "r1")) ($#k12_finseq_1 :::"*>"::: ) )  ($#k8_finseq_1 :::"^"::: )  (Set (Var "F")))) "or" (Bool (Set (Var "F1"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "F"))  ($#k8_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "r1")) ($#k12_finseq_1 :::"*>"::: ) )))  ")" ) & (Bool  "("  (Bool (Set (Var "F2"))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "r2")) ($#k12_finseq_1 :::"*>"::: ) )  ($#k8_finseq_1 :::"^"::: )  (Set (Var "F")))) "or" (Bool (Set (Var "F2"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "F"))  ($#k8_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "r2")) ($#k12_finseq_1 :::"*>"::: ) )))  ")" )) "holds"  (Bool (Set   ($#k18_rvsum_1 :::"Sum"::: )  (Set  "(" (Set (Var "F1"))  ($#k8_rvsum_1 :::"-"::: )  (Set (Var "F2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "r1"))  ($#k9_real_1 :::"-"::: )  (Set (Var "r2")))))) ; 
 
theorem :: INTEGRA5:2 (Bool  "for" (Set (Var "F1")) "," (Set (Var "F2")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  )  "st" (Bool (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "F1")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "F2"))))) "holds"  (Bool  "("  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set  "(" (Set (Var "F1"))  ($#k4_rvsum_1 :::"+"::: )  (Set (Var "F2")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "F1")))) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set  "(" (Set (Var "F1"))  ($#k8_rvsum_1 :::"-"::: )  (Set (Var "F2")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "F1")))) & (Bool (Set   ($#k18_rvsum_1 :::"Sum"::: )  (Set  "(" (Set (Var "F1"))  ($#k4_rvsum_1 :::"+"::: )  (Set (Var "F2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k18_rvsum_1 :::"Sum"::: )  (Set (Var "F1")) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "("  ($#k18_rvsum_1 :::"Sum"::: )  (Set (Var "F2")) ")" ))) & (Bool (Set   ($#k18_rvsum_1 :::"Sum"::: )  (Set  "(" (Set (Var "F1"))  ($#k8_rvsum_1 :::"-"::: )  (Set (Var "F2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k18_rvsum_1 :::"Sum"::: )  (Set (Var "F1")) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "("  ($#k18_rvsum_1 :::"Sum"::: )  (Set (Var "F2")) ")" )))  ")" )) ; 
 
theorem :: INTEGRA5:3 (Bool  "for" (Set (Var "F1")) "," (Set (Var "F2")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  )  "st" (Bool (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "F1")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "F2")))) & (Bool  "("   "for" (Set (Var "i")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "F1"))))) "holds"  (Bool (Set (Set (Var "F1"))  ($#k1_seq_1 :::"."::: )  (Set (Var "i")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "F2"))  ($#k1_seq_1 :::"."::: )  (Set (Var "i"))))  ")" )) "holds"  (Bool (Set   ($#k18_rvsum_1 :::"Sum"::: )  (Set (Var "F1")))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k18_rvsum_1 :::"Sum"::: )  (Set (Var "F2"))))) ; 
 begin  notationlet "f" be   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) ); let "C" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ); synonym "f" :::"||"::: "C" for "f" :::"|"::: "C"; end; definitionlet "f" be   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) ); let "C" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ); :: original: :::"||"::: redefine func "f" :::"||"::: "C" ->   ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set  ($#k1_numbers :::"REAL"::: ) ); end; 
theorem :: INTEGRA5: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 "C")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"  (Bool (Set (Set  "(" (Set (Var "f"))  ($#k1_integra5 :::"||"::: )  (Set (Var "C")) ")" )  ($#k20_valued_1 :::"(#)"::: )  (Set  "(" (Set (Var "g"))  ($#k1_integra5 :::"||"::: )  (Set (Var "C")) ")" ))  ($#r2_relset_1 :::"="::: )  (Set (Set  "(" (Set (Var "f"))  ($#k20_valued_1 :::"(#)"::: )  (Set (Var "g")) ")" )  ($#k1_integra5 :::"||"::: )  (Set (Var "C")))))) ; 
 
theorem :: INTEGRA5:5 (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 "C")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"  (Bool (Set (Set  "(" (Set (Var "f"))  ($#k3_valued_1 :::"+"::: )  (Set (Var "g")) ")" )  ($#k1_integra5 :::"||"::: )  (Set (Var "C")))  ($#r2_relset_1 :::"="::: )  (Set (Set  "(" (Set (Var "f"))  ($#k1_integra5 :::"||"::: )  (Set (Var "C")) ")" )  ($#k3_valued_1 :::"+"::: )  (Set  "(" (Set (Var "g"))  ($#k1_integra5 :::"||"::: )  (Set (Var "C")) ")" ))))) ; 
 definitionlet "A" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_measure5 :::"closed_interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ); let "f" be   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) ); pred "f" :::"is_integrable_on"::: "A" means :: INTEGRA5:def 1 (Bool (Set "f"  ($#k1_integra5 :::"||"::: )  "A") "is"   ($#v3_integra1 :::"integrable"::: )  ); end; 





:: deftheorem    defines :::"is_integrable_on"::: INTEGRA5:def 1 :  (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_measure5 :::"closed_interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (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"))  ($#r1_integra5 :::"is_integrable_on"::: )  (Set (Var "A"))) "iff" (Bool (Set (Set (Var "f"))  ($#k1_integra5 :::"||"::: )  (Set (Var "A"))) "is"   ($#v3_integra1 :::"integrable"::: )  )  ")" ))); 
 definitionlet "A" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_measure5 :::"closed_interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ); let "f" be   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) ); func  :::"integral":::  "(" "f" "," "A" ")"  ->   ($#m1_subset_1 :::"Real":::) equals :: INTEGRA5:def 2 (Set   ($#k12_integra1 :::"integral"::: )  (Set  "(" "f"  ($#k1_integra5 :::"||"::: )  "A" ")" )); end; 






:: deftheorem    defines :::"integral"::: INTEGRA5:def 2 :  (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_measure5 :::"closed_interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"  (Bool (Set   ($#k2_integra5 :::"integral"::: )   "(" (Set (Var "f")) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k12_integra1 :::"integral"::: )  (Set  "(" (Set (Var "f"))  ($#k1_integra5 :::"||"::: )  (Set (Var "A")) ")" ))))); 
 
theorem :: INTEGRA5:6 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_measure5 :::"closed_interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (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_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f"))))) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_integra5 :::"||"::: )  (Set (Var "A"))) "is"   ($#v1_partfun1 :::"total"::: )  ))) ; 
 
theorem :: INTEGRA5:7 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_measure5 :::"closed_interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (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 "A"))) "is"   ($#v1_seq_2 :::"bounded_above"::: )  )) "holds"  (Bool (Set (Set  "(" (Set (Var "f"))  ($#k1_integra5 :::"||"::: )  (Set (Var "A")) ")" )  ($#k2_partfun1 :::"|"::: )  (Set (Var "A"))) "is"   ($#v1_seq_2 :::"bounded_above"::: )  ))) ; 
 
theorem :: INTEGRA5:8 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_measure5 :::"closed_interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (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 "A"))) "is"   ($#v2_seq_2 :::"bounded_below"::: )  )) "holds"  (Bool (Set (Set  "(" (Set (Var "f"))  ($#k1_integra5 :::"||"::: )  (Set (Var "A")) ")" )  ($#k2_partfun1 :::"|"::: )  (Set (Var "A"))) "is"   ($#v2_seq_2 :::"bounded_below"::: )  ))) ; 
 
theorem :: INTEGRA5:9 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_measure5 :::"closed_interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (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 "A"))) "is"   ($#v1_comseq_2 :::"bounded"::: )  )) "holds"  (Bool (Set (Set  "(" (Set (Var "f"))  ($#k1_integra5 :::"||"::: )  (Set (Var "A")) ")" )  ($#k2_partfun1 :::"|"::: )  (Set (Var "A"))) "is"   ($#v1_comseq_2 :::"bounded"::: )  ))) ; 
 begin  
theorem :: INTEGRA5:10 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_measure5 :::"closed_interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (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_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "A"))) "is"   ($#v1_fcont_1 :::"continuous"::: )  )) "holds"  (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "A"))) "is"   ($#v1_comseq_2 :::"bounded"::: )  ))) ; 
 
theorem :: INTEGRA5:11 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_measure5 :::"closed_interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (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_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "A"))) "is"   ($#v1_fcont_1 :::"continuous"::: )  )) "holds"  (Bool (Set (Var "f"))  ($#r1_integra5 :::"is_integrable_on"::: )  (Set (Var "A"))))) ; 
 
theorem :: INTEGRA5:12 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_measure5 :::"closed_interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (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  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "D")) "being"    ($#m1_integra1 :::"Division"::: )   "of" (Set (Var "A"))  "st" (Bool (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set (Var "X"))) & (Bool (Set (Var "f"))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "X"))) & (Bool (Set (Set  "(" (Set (Var "f"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "X")) ")" )  ($#k2_partfun1 :::"|"::: )  (Set (Var "A"))) "is"   ($#v1_comseq_2 :::"bounded"::: )  )) "holds"  (Bool  "("  (Bool (Set   ($#k7_integra1 :::"lower_sum"::: )   "(" (Set  "(" (Set  "(" (Set (Var "f"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "X")) ")" )  ($#k1_integra5 :::"||"::: )  (Set (Var "A")) ")" ) "," (Set (Var "D")) ")" )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set  "("  ($#k4_seq_4 :::"upper_bound"::: )  (Set (Var "A")) ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set  "("  ($#k5_seq_4 :::"lower_bound"::: )  (Set (Var "A")) ")" ) ")" ))) & (Bool (Set (Set  "(" (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set  "("  ($#k4_seq_4 :::"upper_bound"::: )  (Set (Var "A")) ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set  "("  ($#k5_seq_4 :::"lower_bound"::: )  (Set (Var "A")) ")" ) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k6_integra1 :::"upper_sum"::: )   "(" (Set  "(" (Set  "(" (Set (Var "f"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "X")) ")" )  ($#k1_integra5 :::"||"::: )  (Set (Var "A")) ")" ) "," (Set (Var "D")) ")" ))  ")" ))))) ; 
 
theorem :: INTEGRA5:13 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_measure5 :::"closed_interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (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  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "A"))  ($#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 (Var "A"))) & (Bool (Set (Set  "(" (Set (Var "f"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "X")) ")" )  ($#k2_partfun1 :::"|"::: )  (Set (Var "A"))) "is"   ($#v1_comseq_2 :::"bounded"::: )  )) "holds"  (Bool (Set   ($#k2_integra5 :::"integral"::: )   "(" (Set  "(" (Set (Var "f"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "X")) ")" ) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set  "("  ($#k4_seq_4 :::"upper_bound"::: )  (Set (Var "A")) ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set  "("  ($#k5_seq_4 :::"lower_bound"::: )  (Set (Var "A")) ")" ) ")" )))))) ; 
 
theorem :: INTEGRA5:14 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_measure5 :::"closed_interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (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 "A"))) "is"   ($#v7_valued_0 :::"non-decreasing"::: )  ) & (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f"))))) "holds"  (Bool (Set   ($#k1_rvsum_1 :::"rng"::: )  (Set  "(" (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "A")) ")" )) "is"   ($#v5_xxreal_2 :::"real-bounded"::: )  ))) ; 
 
theorem :: INTEGRA5:15 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_measure5 :::"closed_interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (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 "A"))) "is"   ($#v7_valued_0 :::"non-decreasing"::: )  ) & (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f"))))) "holds"  (Bool  "("  (Bool (Set   ($#k5_seq_4 :::"lower_bound"::: )  (Set  "("  ($#k1_rvsum_1 :::"rng"::: )  (Set  "(" (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "A")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set  "("  ($#k5_seq_4 :::"lower_bound"::: )  (Set (Var "A")) ")" ))) & (Bool (Set   ($#k4_seq_4 :::"upper_bound"::: )  (Set  "("  ($#k1_rvsum_1 :::"rng"::: )  (Set  "(" (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "A")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set  "("  ($#k4_seq_4 :::"upper_bound"::: )  (Set (Var "A")) ")" )))  ")" ))) ; 
 
theorem :: INTEGRA5:16 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_measure5 :::"closed_interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (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 "A"))) "is"   ($#v1_rfunct_2 :::"monotone"::: )  ) & (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f"))))) "holds"  (Bool (Set (Var "f"))  ($#r1_integra5 :::"is_integrable_on"::: )  (Set (Var "A"))))) ; 
 
theorem :: INTEGRA5:17 (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"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_measure5 :::"closed_interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "A"))) "is"   ($#v1_fcont_1 :::"continuous"::: )  ) & (Bool (Set (Var "B"))  ($#r1_tarski :::"c="::: )  (Set (Var "A")))) "holds"  (Bool (Set (Var "f"))  ($#r1_integra5 :::"is_integrable_on"::: )  (Set (Var "B"))))) ; 
 
theorem :: INTEGRA5:18 (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")) "," (Set (Var "C")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_measure5 :::"closed_interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set (Var "X"))) & (Bool (Set (Var "f"))  ($#r2_fdiff_1 :::"is_differentiable_on"::: )  (Set (Var "X"))) & (Bool (Set (Set  "(" (Set (Var "f"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "X")) ")" )  ($#k2_partfun1 :::"|"::: )  (Set (Var "A"))) "is"   ($#v1_fcont_1 :::"continuous"::: )  ) & (Bool (Set   ($#k5_seq_4 :::"lower_bound"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k5_seq_4 :::"lower_bound"::: )  (Set (Var "B")))) & (Bool (Set   ($#k4_seq_4 :::"upper_bound"::: )  (Set (Var "B")))  ($#r1_hidden :::"="::: )  (Set   ($#k5_seq_4 :::"lower_bound"::: )  (Set (Var "C")))) & (Bool (Set   ($#k4_seq_4 :::"upper_bound"::: )  (Set (Var "C")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_seq_4 :::"upper_bound"::: )  (Set (Var "A"))))) "holds"  (Bool  "("  (Bool (Set (Var "B"))  ($#r1_tarski :::"c="::: )  (Set (Var "A"))) & (Bool (Set (Var "C"))  ($#r1_tarski :::"c="::: )  (Set (Var "A"))) & (Bool (Set   ($#k2_integra5 :::"integral"::: )   "(" (Set  "(" (Set (Var "f"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "X")) ")" ) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_integra5 :::"integral"::: )   "(" (Set  "(" (Set (Var "f"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "X")) ")" ) "," (Set (Var "B")) ")"  ")" )  ($#k7_real_1 :::"+"::: )  (Set  "("  ($#k2_integra5 :::"integral"::: )   "(" (Set  "(" (Set (Var "f"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "X")) ")" ) "," (Set (Var "C")) ")"  ")" )))  ")" )))) ; 
 definitionlet "a", "b" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; assume 
(Bool (Set (Const "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Const "b")))
 ; func :::"['":::"a" "," "b":::"']"::: ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_measure5 :::"closed_interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) equals :: INTEGRA5:def 3 (Set  ($#k1_rcomp_1 :::"[."::: ) "a" "," "b" ($#k1_rcomp_1 :::".]"::: ) ); end; 







:: deftheorem    defines :::"['"::: INTEGRA5:def 3 :  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b")))) "holds"  (Bool (Set  ($#k3_integra5 :::"['"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k3_integra5 :::"']"::: ) )  ($#r1_hidden :::"="::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) ))); 
 definitionlet "a", "b" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; let "f" be   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) ); func  :::"integral":::  "(" "f" "," "a" "," "b" ")"  ->   ($#m1_subset_1 :::"Real":::) equals :: INTEGRA5:def 4 (Set   ($#k2_integra5 :::"integral"::: )   "(" "f" "," (Set  ($#k3_integra5 :::"['"::: ) "a" "," "b" ($#k3_integra5 :::"']"::: ) ) ")" ) if (Bool "a"  ($#r1_xxreal_0 :::"<="::: )  "b")  otherwise (Set   ($#k1_real_1 :::"-"::: )  (Set  "("  ($#k2_integra5 :::"integral"::: )   "(" "f" "," (Set  ($#k3_integra5 :::"['"::: ) "b" "," "a" ($#k3_integra5 :::"']"::: ) ) ")"  ")" )); end; 







:: deftheorem    defines :::"integral"::: INTEGRA5:def 4 :  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"   (Bool  "("   "("  (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b")))) "implies" (Bool (Set   ($#k4_integra5 :::"integral"::: )   "(" (Set (Var "f")) "," (Set (Var "a")) "," (Set (Var "b")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k2_integra5 :::"integral"::: )   "(" (Set (Var "f")) "," (Set  ($#k3_integra5 :::"['"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k3_integra5 :::"']"::: ) ) ")" ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b"))))) "implies" (Bool (Set   ($#k4_integra5 :::"integral"::: )   "(" (Set (Var "f")) "," (Set (Var "a")) "," (Set (Var "b")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Set  "("  ($#k2_integra5 :::"integral"::: )   "(" (Set (Var "f")) "," (Set  ($#k3_integra5 :::"['"::: ) (Set (Var "b")) "," (Set (Var "a")) ($#k3_integra5 :::"']"::: ) ) ")"  ")" )))  ")"   ")" ))); 
 
theorem :: INTEGRA5:19 (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_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_measure5 :::"closed_interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) ))) "holds"  (Bool (Set   ($#k2_integra5 :::"integral"::: )   "(" (Set (Var "f")) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k4_integra5 :::"integral"::: )   "(" (Set (Var "f")) "," (Set (Var "a")) "," (Set (Var "b")) ")" ))))) ; 
 
theorem :: INTEGRA5:20 (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_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_measure5 :::"closed_interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "b")) "," (Set (Var "a")) ($#k1_rcomp_1 :::".]"::: ) ))) "holds"  (Bool (Set   ($#k1_real_1 :::"-"::: )  (Set  "("  ($#k2_integra5 :::"integral"::: )   "(" (Set (Var "f")) "," (Set (Var "A")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_integra5 :::"integral"::: )   "(" (Set (Var "f")) "," (Set (Var "a")) "," (Set (Var "b")) ")" ))))) ; 
 
theorem :: INTEGRA5:21 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_measure5 :::"closed_interval"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  (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 "X")) "being"   ($#v3_rcomp_1 :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (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"))) & (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set (Var "X"))) & (Bool (Set (Set (Var "f"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "X")))  ($#r1_integra5 :::"is_integrable_on"::: )  (Set (Var "A"))) & (Bool (Set (Set  "(" (Set (Var "f"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "X")) ")" )  ($#k2_partfun1 :::"|"::: )  (Set (Var "A"))) "is"   ($#v1_comseq_2 :::"bounded"::: )  ) & (Bool (Set (Set (Var "g"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "X")))  ($#r1_integra5 :::"is_integrable_on"::: )  (Set (Var "A"))) & (Bool (Set (Set  "(" (Set (Var "g"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "X")) ")" )  ($#k2_partfun1 :::"|"::: )  (Set (Var "A"))) "is"   ($#v1_comseq_2 :::"bounded"::: )  )) "holds"  (Bool (Set   ($#k2_integra5 :::"integral"::: )   "(" (Set  "(" (Set  "(" (Set (Var "f"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "X")) ")" )  ($#k20_valued_1 :::"(#)"::: )  (Set (Var "g")) ")" ) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set  "("  ($#k4_seq_4 :::"upper_bound"::: )  (Set (Var "A")) ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "g"))  ($#k1_seq_1 :::"."::: )  (Set  "("  ($#k4_seq_4 :::"upper_bound"::: )  (Set (Var "A")) ")" ) ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set  "(" (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set  "("  ($#k5_seq_4 :::"lower_bound"::: )  (Set (Var "A")) ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "g"))  ($#k1_seq_1 :::"."::: )  (Set  "("  ($#k5_seq_4 :::"lower_bound"::: )  (Set (Var "A")) ")" ) ")" ) ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "("  ($#k2_integra5 :::"integral"::: )   "(" (Set  "(" (Set (Var "f"))  ($#k20_valued_1 :::"(#)"::: )  (Set  "(" (Set (Var "g"))  ($#k2_fdiff_1 :::"`|"::: )  (Set (Var "X")) ")" ) ")" ) "," (Set (Var "A")) ")"  ")" )))))) ;