:: INTEGRA1 semantic presentation begin registration cluster ($#v2_measure5 :::"closed_interval"::: ) -> ($#v1_rcomp_1 :::"compact"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k1_numbers :::"REAL"::: ) )); end; theorem :: INTEGRA1:1 canceled; theorem :: INTEGRA1:2 canceled; theorem :: INTEGRA1:3 (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"::: ) ) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v3_xxreal_2 :::"bounded_below"::: ) ) & (Bool (Set (Var "A")) "is" ($#v4_xxreal_2 :::"bounded_above"::: ) ) ")" )) ; registration cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_measure5 :::"closed_interval"::: ) -> ($#v5_xxreal_2 :::"real-bounded"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k1_numbers :::"REAL"::: ) )); end; theorem :: INTEGRA1:4 (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"::: ) ) "holds" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" ($#k5_seq_4 :::"lower_bound"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k4_seq_4 :::"upper_bound"::: ) (Set (Var "A")) ")" ) ($#k1_rcomp_1 :::".]"::: ) ))) ; theorem :: INTEGRA1:5 (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 "a1")) "," (Set (Var "a2")) "," (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a1")) "," (Set (Var "b1")) ($#k1_rcomp_1 :::".]"::: ) )) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a2")) "," (Set (Var "b2")) ($#k1_rcomp_1 :::".]"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set (Var "a2"))) & (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set (Var "b2"))) ")" ))) ; begin definitioncanceled; let "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_rcomp_1 :::"compact"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ); mode :::"Division"::: "of" "A" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v5_valued_0 :::"increasing"::: ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) means :: INTEGRA1:def 2 (Bool "(" (Bool (Set ($#k1_rvsum_1 :::"rng"::: ) it) ($#r1_tarski :::"c="::: ) "A") & (Bool (Set it ($#k1_seq_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) it ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_seq_4 :::"upper_bound"::: ) "A")) ")" ); end; :: deftheorem INTEGRA1:def 1 : canceled; :: deftheorem defines :::"Division"::: INTEGRA1:def 2 : (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_rcomp_1 :::"compact"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "b2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v5_valued_0 :::"increasing"::: ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m1_integra1 :::"Division"::: ) "of" (Set (Var "A"))) "iff" (Bool "(" (Bool (Set ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "b2"))) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) & (Bool (Set (Set (Var "b2")) ($#k1_seq_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "b2")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_seq_4 :::"upper_bound"::: ) (Set (Var "A")))) ")" ) ")" ))); definitionlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_rcomp_1 :::"compact"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ); func :::"divs"::: "A" -> ($#m1_hidden :::"set"::: ) means :: INTEGRA1:def 3 (Bool "for" (Set (Var "x1")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool (Set (Var "x1")) "is" ($#m1_integra1 :::"Division"::: ) "of" "A") ")" )); end; :: deftheorem defines :::"divs"::: INTEGRA1:def 3 : (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_rcomp_1 :::"compact"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k1_integra1 :::"divs"::: ) (Set (Var "A")))) "iff" (Bool "for" (Set (Var "x1")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "iff" (Bool (Set (Var "x1")) "is" ($#m1_integra1 :::"Division"::: ) "of" (Set (Var "A"))) ")" )) ")" ))); registrationlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_rcomp_1 :::"compact"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set ($#k1_integra1 :::"divs"::: ) "A") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; registrationlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_rcomp_1 :::"compact"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ); cluster -> ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_integra1 :::"divs"::: ) "A"); end; registrationlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_rcomp_1 :::"compact"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ); cluster -> ($#v1_finseq_1 :::"FinSequence-like"::: ) ($#v3_valued_0 :::"real-valued"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_integra1 :::"divs"::: ) "A"); end; theorem :: INTEGRA1:6 (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (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 "D")) "being" ($#m1_integra1 :::"Division"::: ) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "D"))))) "holds" (Bool (Set (Set (Var "D")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r2_hidden :::"in"::: ) (Set (Var "A")))))) ; theorem :: INTEGRA1:7 (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (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 "D")) "being" ($#m1_integra1 :::"Division"::: ) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "D")))) & (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) (Num 1))) "holds" (Bool "(" (Bool (Set (Set (Var "i")) ($#k9_real_1 :::"-"::: ) (Num 1)) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "D")))) & (Bool (Set (Set (Var "D")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k9_real_1 :::"-"::: ) (Num 1) ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Set (Var "i")) ($#k9_real_1 :::"-"::: ) (Num 1)) ($#r2_hidden :::"in"::: ) (Set ($#k5_numbers :::"NAT"::: ) )) ")" )))) ; 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 "D" be ($#m1_integra1 :::"Division"::: ) "of" (Set (Const "A")); let "i" be ($#m1_hidden :::"Nat":::); assume (Bool (Set (Const "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Const "D")))) ; func :::"divset"::: "(" "D" "," "i" ")" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_measure5 :::"closed_interval"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) means :: INTEGRA1:def 4 (Bool "(" (Bool (Set ($#k5_seq_4 :::"lower_bound"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k5_seq_4 :::"lower_bound"::: ) "A")) & (Bool (Set ($#k4_seq_4 :::"upper_bound"::: ) it) ($#r1_hidden :::"="::: ) (Set "D" ($#k1_seq_1 :::"."::: ) "i")) ")" ) if (Bool "i" ($#r1_hidden :::"="::: ) (Num 1)) otherwise (Bool "(" (Bool (Set ($#k5_seq_4 :::"lower_bound"::: ) it) ($#r1_hidden :::"="::: ) (Set "D" ($#k1_seq_1 :::"."::: ) (Set "(" "i" ($#k5_real_1 :::"-"::: ) (Num 1) ")" ))) & (Bool (Set ($#k4_seq_4 :::"upper_bound"::: ) it) ($#r1_hidden :::"="::: ) (Set "D" ($#k1_seq_1 :::"."::: ) "i")) ")" ); end; :: deftheorem defines :::"divset"::: INTEGRA1:def 4 : (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 "D")) "being" ($#m1_integra1 :::"Division"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "D"))))) "holds" (Bool "for" (Set (Var "b4")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_measure5 :::"closed_interval"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Num 1))) "implies" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k2_integra1 :::"divset"::: ) "(" (Set (Var "D")) "," (Set (Var "i")) ")" )) "iff" (Bool "(" (Bool (Set ($#k5_seq_4 :::"lower_bound"::: ) (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set ($#k5_seq_4 :::"lower_bound"::: ) (Set (Var "A")))) & (Bool (Set ($#k4_seq_4 :::"upper_bound"::: ) (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "D")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) ")" ) ")" ) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "i")) ($#r1_hidden :::"="::: ) (Num 1)))) "implies" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k2_integra1 :::"divset"::: ) "(" (Set (Var "D")) "," (Set (Var "i")) ")" )) "iff" (Bool "(" (Bool (Set ($#k5_seq_4 :::"lower_bound"::: ) (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "D")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k5_real_1 :::"-"::: ) (Num 1) ")" ))) & (Bool (Set ($#k4_seq_4 :::"upper_bound"::: ) (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "D")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))) ")" ) ")" ) ")" ")" ))))); theorem :: INTEGRA1:8 (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (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 "D")) "being" ($#m1_integra1 :::"Division"::: ) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "D"))))) "holds" (Bool (Set ($#k2_integra1 :::"divset"::: ) "(" (Set (Var "D")) "," (Set (Var "i")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "A")))))) ; definitionlet "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ); func :::"vol"::: "A" -> ($#m1_subset_1 :::"Real":::) equals :: INTEGRA1:def 5 (Set (Set "(" ($#k4_seq_4 :::"upper_bound"::: ) "A" ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k5_seq_4 :::"lower_bound"::: ) "A" ")" )); end; :: deftheorem defines :::"vol"::: INTEGRA1:def 5 : (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k3_integra1 :::"vol"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_seq_4 :::"upper_bound"::: ) (Set (Var "A")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k5_seq_4 :::"lower_bound"::: ) (Set (Var "A")) ")" )))); theorem :: INTEGRA1:9 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v5_xxreal_2 :::"real-bounded"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_integra1 :::"vol"::: ) (Set (Var "A"))))) ; begin 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 (Const "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ); let "D" be ($#m1_integra1 :::"Division"::: ) "of" (Set (Const "A")); func :::"upper_volume"::: "(" "f" "," "D" ")" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) means :: INTEGRA1:def 6 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "D")) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "D"))) "holds" (Bool (Set it ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_seq_4 :::"upper_bound"::: ) (Set "(" ($#k1_rvsum_1 :::"rng"::: ) (Set "(" "f" ($#k2_partfun1 :::"|"::: ) (Set "(" ($#k2_integra1 :::"divset"::: ) "(" "D" "," (Set (Var "i")) ")" ")" ) ")" ) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k3_integra1 :::"vol"::: ) (Set "(" ($#k2_integra1 :::"divset"::: ) "(" "D" "," (Set (Var "i")) ")" ")" ) ")" ))) ")" ) ")" ); func :::"lower_volume"::: "(" "f" "," "D" ")" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) means :: INTEGRA1:def 7 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "D")) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "D"))) "holds" (Bool (Set it ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_seq_4 :::"lower_bound"::: ) (Set "(" ($#k1_rvsum_1 :::"rng"::: ) (Set "(" "f" ($#k2_partfun1 :::"|"::: ) (Set "(" ($#k2_integra1 :::"divset"::: ) "(" "D" "," (Set (Var "i")) ")" ")" ) ")" ) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k3_integra1 :::"vol"::: ) (Set "(" ($#k2_integra1 :::"divset"::: ) "(" "D" "," (Set (Var "i")) ")" ")" ) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"upper_volume"::: INTEGRA1:def 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 (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "D")) "being" ($#m1_integra1 :::"Division"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "b4")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k4_integra1 :::"upper_volume"::: ) "(" (Set (Var "f")) "," (Set (Var "D")) ")" )) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "D")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "D"))))) "holds" (Bool (Set (Set (Var "b4")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_seq_4 :::"upper_bound"::: ) (Set "(" ($#k1_rvsum_1 :::"rng"::: ) (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set "(" ($#k2_integra1 :::"divset"::: ) "(" (Set (Var "D")) "," (Set (Var "i")) ")" ")" ) ")" ) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k3_integra1 :::"vol"::: ) (Set "(" ($#k2_integra1 :::"divset"::: ) "(" (Set (Var "D")) "," (Set (Var "i")) ")" ")" ) ")" ))) ")" ) ")" ) ")" ))))); :: deftheorem defines :::"lower_volume"::: INTEGRA1:def 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 (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "D")) "being" ($#m1_integra1 :::"Division"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "b4")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k5_integra1 :::"lower_volume"::: ) "(" (Set (Var "f")) "," (Set (Var "D")) ")" )) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "D")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "D"))))) "holds" (Bool (Set (Set (Var "b4")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_seq_4 :::"lower_bound"::: ) (Set "(" ($#k1_rvsum_1 :::"rng"::: ) (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set "(" ($#k2_integra1 :::"divset"::: ) "(" (Set (Var "D")) "," (Set (Var "i")) ")" ")" ) ")" ) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k3_integra1 :::"vol"::: ) (Set "(" ($#k2_integra1 :::"divset"::: ) "(" (Set (Var "D")) "," (Set (Var "i")) ")" ")" ) ")" ))) ")" ) ")" ) ")" ))))); 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 (Const "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ); let "D" be ($#m1_integra1 :::"Division"::: ) "of" (Set (Const "A")); func :::"upper_sum"::: "(" "f" "," "D" ")" -> ($#m1_subset_1 :::"Real":::) equals :: INTEGRA1:def 8 (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" ($#k4_integra1 :::"upper_volume"::: ) "(" "f" "," "D" ")" ")" )); func :::"lower_sum"::: "(" "f" "," "D" ")" -> ($#m1_subset_1 :::"Real":::) equals :: INTEGRA1:def 9 (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" ($#k5_integra1 :::"lower_volume"::: ) "(" "f" "," "D" ")" ")" )); end; :: deftheorem defines :::"upper_sum"::: INTEGRA1:def 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 (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "D")) "being" ($#m1_integra1 :::"Division"::: ) "of" (Set (Var "A")) "holds" (Bool (Set ($#k6_integra1 :::"upper_sum"::: ) "(" (Set (Var "f")) "," (Set (Var "D")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" ($#k4_integra1 :::"upper_volume"::: ) "(" (Set (Var "f")) "," (Set (Var "D")) ")" ")" )))))); :: deftheorem defines :::"lower_sum"::: INTEGRA1:def 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 (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "D")) "being" ($#m1_integra1 :::"Division"::: ) "of" (Set (Var "A")) "holds" (Bool (Set ($#k7_integra1 :::"lower_sum"::: ) "(" (Set (Var "f")) "," (Set (Var "D")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" ($#k5_integra1 :::"lower_volume"::: ) "(" (Set (Var "f")) "," (Set (Var "D")) ")" ")" )))))); 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 (Const "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ); func :::"upper_sum_set"::: "f" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k1_integra1 :::"divs"::: ) "A" ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) means :: INTEGRA1:def 10 (Bool "for" (Set (Var "D")) "being" ($#m1_integra1 :::"Division"::: ) "of" "A" "holds" (Bool (Set it ($#k1_seq_1 :::"."::: ) (Set (Var "D"))) ($#r1_hidden :::"="::: ) (Set ($#k6_integra1 :::"upper_sum"::: ) "(" "f" "," (Set (Var "D")) ")" ))); func :::"lower_sum_set"::: "f" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k1_integra1 :::"divs"::: ) "A" ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) means :: INTEGRA1:def 11 (Bool "for" (Set (Var "D")) "being" ($#m1_integra1 :::"Division"::: ) "of" "A" "holds" (Bool (Set it ($#k1_seq_1 :::"."::: ) (Set (Var "D"))) ($#r1_hidden :::"="::: ) (Set ($#k7_integra1 :::"lower_sum"::: ) "(" "f" "," (Set (Var "D")) ")" ))); end; :: deftheorem defines :::"upper_sum_set"::: INTEGRA1:def 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 (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k1_integra1 :::"divs"::: ) (Set (Var "A")) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k8_integra1 :::"upper_sum_set"::: ) (Set (Var "f")))) "iff" (Bool "for" (Set (Var "D")) "being" ($#m1_integra1 :::"Division"::: ) "of" (Set (Var "A")) "holds" (Bool (Set (Set (Var "b3")) ($#k1_seq_1 :::"."::: ) (Set (Var "D"))) ($#r1_hidden :::"="::: ) (Set ($#k6_integra1 :::"upper_sum"::: ) "(" (Set (Var "f")) "," (Set (Var "D")) ")" ))) ")" )))); :: deftheorem defines :::"lower_sum_set"::: INTEGRA1:def 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 (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k1_integra1 :::"divs"::: ) (Set (Var "A")) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k9_integra1 :::"lower_sum_set"::: ) (Set (Var "f")))) "iff" (Bool "for" (Set (Var "D")) "being" ($#m1_integra1 :::"Division"::: ) "of" (Set (Var "A")) "holds" (Bool (Set (Set (Var "b3")) ($#k1_seq_1 :::"."::: ) (Set (Var "D"))) ($#r1_hidden :::"="::: ) (Set ($#k7_integra1 :::"lower_sum"::: ) "(" (Set (Var "f")) "," (Set (Var "D")) ")" ))) ")" )))); 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 (Const "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ); attr "f" is :::"upper_integrable"::: means :: INTEGRA1:def 12 (Bool (Set ($#k1_rvsum_1 :::"rng"::: ) (Set "(" ($#k8_integra1 :::"upper_sum_set"::: ) "f" ")" )) "is" ($#v3_xxreal_2 :::"bounded_below"::: ) ); attr "f" is :::"lower_integrable"::: means :: INTEGRA1:def 13 (Bool (Set ($#k1_rvsum_1 :::"rng"::: ) (Set "(" ($#k9_integra1 :::"lower_sum_set"::: ) "f" ")" )) "is" ($#v4_xxreal_2 :::"bounded_above"::: ) ); end; :: deftheorem defines :::"upper_integrable"::: INTEGRA1:def 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 "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v1_integra1 :::"upper_integrable"::: ) ) "iff" (Bool (Set ($#k1_rvsum_1 :::"rng"::: ) (Set "(" ($#k8_integra1 :::"upper_sum_set"::: ) (Set (Var "f")) ")" )) "is" ($#v3_xxreal_2 :::"bounded_below"::: ) ) ")" ))); :: deftheorem defines :::"lower_integrable"::: INTEGRA1:def 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 "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v2_integra1 :::"lower_integrable"::: ) ) "iff" (Bool (Set ($#k1_rvsum_1 :::"rng"::: ) (Set "(" ($#k9_integra1 :::"lower_sum_set"::: ) (Set (Var "f")) ")" )) "is" ($#v4_xxreal_2 :::"bounded_above"::: ) ) ")" ))); 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 (Const "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ); func :::"upper_integral"::: "f" -> ($#m1_subset_1 :::"Real":::) equals :: INTEGRA1:def 14 (Set ($#k5_seq_4 :::"lower_bound"::: ) (Set "(" ($#k1_rvsum_1 :::"rng"::: ) (Set "(" ($#k8_integra1 :::"upper_sum_set"::: ) "f" ")" ) ")" )); end; :: deftheorem defines :::"upper_integral"::: INTEGRA1:def 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 (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k10_integra1 :::"upper_integral"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k5_seq_4 :::"lower_bound"::: ) (Set "(" ($#k1_rvsum_1 :::"rng"::: ) (Set "(" ($#k8_integra1 :::"upper_sum_set"::: ) (Set (Var "f")) ")" ) ")" ))))); 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 (Const "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ); func :::"lower_integral"::: "f" -> ($#m1_subset_1 :::"Real":::) equals :: INTEGRA1:def 15 (Set ($#k4_seq_4 :::"upper_bound"::: ) (Set "(" ($#k1_rvsum_1 :::"rng"::: ) (Set "(" ($#k9_integra1 :::"lower_sum_set"::: ) "f" ")" ) ")" )); end; :: deftheorem defines :::"lower_integral"::: INTEGRA1:def 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 (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k11_integra1 :::"lower_integral"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k4_seq_4 :::"upper_bound"::: ) (Set "(" ($#k1_rvsum_1 :::"rng"::: ) (Set "(" ($#k9_integra1 :::"lower_sum_set"::: ) (Set (Var "f")) ")" ) ")" ))))); 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 (Const "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ); attr "f" is :::"integrable"::: means :: INTEGRA1:def 16 (Bool "(" (Bool "f" "is" ($#v1_integra1 :::"upper_integrable"::: ) ) & (Bool "f" "is" ($#v2_integra1 :::"lower_integrable"::: ) ) & (Bool (Set ($#k10_integra1 :::"upper_integral"::: ) "f") ($#r1_hidden :::"="::: ) (Set ($#k11_integra1 :::"lower_integral"::: ) "f")) ")" ); end; :: deftheorem defines :::"integrable"::: INTEGRA1:def 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 (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v3_integra1 :::"integrable"::: ) ) "iff" (Bool "(" (Bool (Set (Var "f")) "is" ($#v1_integra1 :::"upper_integrable"::: ) ) & (Bool (Set (Var "f")) "is" ($#v2_integra1 :::"lower_integrable"::: ) ) & (Bool (Set ($#k10_integra1 :::"upper_integral"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k11_integra1 :::"lower_integral"::: ) (Set (Var "f")))) ")" ) ")" ))); 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 (Const "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ); func :::"integral"::: "f" -> ($#m1_subset_1 :::"Real":::) equals :: INTEGRA1:def 17 (Set ($#k10_integra1 :::"upper_integral"::: ) "f"); end; :: deftheorem defines :::"integral"::: INTEGRA1:def 17 : (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 (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k12_integra1 :::"integral"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k10_integra1 :::"upper_integral"::: ) (Set (Var "f")))))); begin theorem :: INTEGRA1:10 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k1_rvsum_1 :::"rng"::: ) (Set "(" (Set (Var "f")) ($#k3_valued_1 :::"+"::: ) (Set (Var "g")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "f")) ")" ) ($#k9_member_1 :::"++"::: ) (Set "(" ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "g")) ")" ))))) ; theorem :: INTEGRA1:11 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) "is" ($#v2_seq_2 :::"bounded_below"::: ) )) "holds" (Bool (Set ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "f"))) "is" ($#v3_xxreal_2 :::"bounded_below"::: ) ))) ; theorem :: INTEGRA1:12 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "f"))) "is" ($#v3_xxreal_2 :::"bounded_below"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) "is" ($#v2_seq_2 :::"bounded_below"::: ) ))) ; theorem :: INTEGRA1:13 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) "is" ($#v1_seq_2 :::"bounded_above"::: ) )) "holds" (Bool (Set ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "f"))) "is" ($#v4_xxreal_2 :::"bounded_above"::: ) ))) ; theorem :: INTEGRA1:14 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "f"))) "is" ($#v4_xxreal_2 :::"bounded_above"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) "is" ($#v1_seq_2 :::"bounded_above"::: ) ))) ; theorem :: INTEGRA1:15 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) "is" ($#v1_comseq_2 :::"bounded"::: ) )) "holds" (Bool (Set ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "f"))) "is" ($#v5_xxreal_2 :::"real-bounded"::: ) ))) ; begin theorem :: INTEGRA1:16 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" ($#k7_rfunct_1 :::"chi"::: ) "(" (Set (Var "A")) "," (Set (Var "A")) ")" ")" ) ($#k2_partfun1 :::"|"::: ) (Set (Var "A"))) "is" bbbadV3_FUNCT_1())) ; theorem :: INTEGRA1:17 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k1_rvsum_1 :::"rng"::: ) (Set "(" ($#k7_rfunct_1 :::"chi"::: ) "(" (Set (Var "A")) "," (Set (Var "A")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_seq_4 :::"{"::: ) (Num 1) ($#k1_seq_4 :::"}"::: ) )))) ; theorem :: INTEGRA1:18 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "B")) ($#r1_xboole_0 :::"meets"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k7_rfunct_1 :::"chi"::: ) "(" (Set (Var "A")) "," (Set (Var "A")) ")" ")" )))) "holds" (Bool (Set ($#k1_rvsum_1 :::"rng"::: ) (Set "(" (Set "(" ($#k7_rfunct_1 :::"chi"::: ) "(" (Set (Var "A")) "," (Set (Var "A")) ")" ")" ) ($#k2_partfun1 :::"|"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_seq_4 :::"{"::: ) (Num 1) ($#k1_seq_4 :::"}"::: ) ))))) ; theorem :: INTEGRA1:19 (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (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 "D")) "being" ($#m1_integra1 :::"Division"::: ) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "D"))))) "holds" (Bool (Set ($#k3_integra1 :::"vol"::: ) (Set "(" ($#k2_integra1 :::"divset"::: ) "(" (Set (Var "D")) "," (Set (Var "i")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_integra1 :::"lower_volume"::: ) "(" (Set "(" ($#k7_rfunct_1 :::"chi"::: ) "(" (Set (Var "A")) "," (Set (Var "A")) ")" ")" ) "," (Set (Var "D")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))))))) ; theorem :: INTEGRA1:20 (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (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 "D")) "being" ($#m1_integra1 :::"Division"::: ) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "D"))))) "holds" (Bool (Set ($#k3_integra1 :::"vol"::: ) (Set "(" ($#k2_integra1 :::"divset"::: ) "(" (Set (Var "D")) "," (Set (Var "i")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_integra1 :::"upper_volume"::: ) "(" (Set "(" ($#k7_rfunct_1 :::"chi"::: ) "(" (Set (Var "A")) "," (Set (Var "A")) ")" ")" ) "," (Set (Var "D")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))))))) ; theorem :: INTEGRA1:21 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "," (Set (Var "H")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "H")))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool (Set (Set (Var "H")) ($#k1_seq_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k7_partfun1 :::"/."::: ) (Set (Var "k")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "G")) ($#k7_partfun1 :::"/."::: ) (Set (Var "k")) ")" ))) ")" )) "holds" (Bool (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k18_rvsum_1 :::"Sum"::: ) (Set (Var "F")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k18_rvsum_1 :::"Sum"::: ) (Set (Var "G")) ")" )))) ; theorem :: INTEGRA1:22 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "," (Set (Var "H")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "H")))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool (Set (Set (Var "H")) ($#k1_seq_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k7_partfun1 :::"/."::: ) (Set (Var "k")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "G")) ($#k7_partfun1 :::"/."::: ) (Set (Var "k")) ")" ))) ")" )) "holds" (Bool (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k18_rvsum_1 :::"Sum"::: ) (Set (Var "F")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k18_rvsum_1 :::"Sum"::: ) (Set (Var "G")) ")" )))) ; theorem :: INTEGRA1:23 (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 "D")) "being" ($#m1_integra1 :::"Division"::: ) "of" (Set (Var "A")) "holds" (Bool (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" ($#k5_integra1 :::"lower_volume"::: ) "(" (Set "(" ($#k7_rfunct_1 :::"chi"::: ) "(" (Set (Var "A")) "," (Set (Var "A")) ")" ")" ) "," (Set (Var "D")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_integra1 :::"vol"::: ) (Set (Var "A")))))) ; theorem :: INTEGRA1:24 (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 "D")) "being" ($#m1_integra1 :::"Division"::: ) "of" (Set (Var "A")) "holds" (Bool (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" ($#k4_integra1 :::"upper_volume"::: ) "(" (Set "(" ($#k7_rfunct_1 :::"chi"::: ) "(" (Set (Var "A")) "," (Set (Var "A")) ")" ")" ) "," (Set (Var "D")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_integra1 :::"vol"::: ) (Set (Var "A")))))) ; begin registrationlet "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 (Const "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ); let "D" be ($#m1_integra1 :::"Division"::: ) "of" (Set (Const "A")); cluster (Set ($#k4_integra1 :::"upper_volume"::: ) "(" "f" "," "D" ")" ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; cluster (Set ($#k5_integra1 :::"lower_volume"::: ) "(" "f" "," "D" ")" ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: INTEGRA1:25 (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 "D")) "being" ($#m1_integra1 :::"Division"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (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 "(" ($#k5_seq_4 :::"lower_bound"::: ) (Set "(" ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "f")) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k3_integra1 :::"vol"::: ) (Set (Var "A")) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k7_integra1 :::"lower_sum"::: ) "(" (Set (Var "f")) "," (Set (Var "D")) ")" ))))) ; theorem :: INTEGRA1:26 (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (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 "D")) "being" ($#m1_integra1 :::"Division"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A"))) "is" ($#v1_seq_2 :::"bounded_above"::: ) ) & (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "D"))))) "holds" (Bool (Set (Set "(" ($#k4_seq_4 :::"upper_bound"::: ) (Set "(" ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "f")) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k3_integra1 :::"vol"::: ) (Set "(" ($#k2_integra1 :::"divset"::: ) "(" (Set (Var "D")) "," (Set (Var "i")) ")" ")" ) ")" )) ($#r1_xxreal_0 :::">="::: ) (Set (Set "(" ($#k4_seq_4 :::"upper_bound"::: ) (Set "(" ($#k1_rvsum_1 :::"rng"::: ) (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set "(" ($#k2_integra1 :::"divset"::: ) "(" (Set (Var "D")) "," (Set (Var "i")) ")" ")" ) ")" ) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k3_integra1 :::"vol"::: ) (Set "(" ($#k2_integra1 :::"divset"::: ) "(" (Set (Var "D")) "," (Set (Var "i")) ")" ")" ) ")" ))))))) ; theorem :: INTEGRA1:27 (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 "D")) "being" ($#m1_integra1 :::"Division"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (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 ($#k6_integra1 :::"upper_sum"::: ) "(" (Set (Var "f")) "," (Set (Var "D")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k4_seq_4 :::"upper_bound"::: ) (Set "(" ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "f")) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k3_integra1 :::"vol"::: ) (Set (Var "A")) ")" )))))) ; theorem :: INTEGRA1:28 (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 "D")) "being" ($#m1_integra1 :::"Division"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A"))) "is" ($#v1_comseq_2 :::"bounded"::: ) )) "holds" (Bool (Set ($#k7_integra1 :::"lower_sum"::: ) "(" (Set (Var "f")) "," (Set (Var "D")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_integra1 :::"upper_sum"::: ) "(" (Set (Var "f")) "," (Set (Var "D")) ")" ))))) ; definitionlet "D1", "D2" be ($#m1_hidden :::"FinSequence":::); pred "D1" :::"<="::: "D2" means :: INTEGRA1:def 18 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) "D1") ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "D2")) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) "D1") ($#r1_tarski :::"c="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) "D2")) ")" ); reflexivity (Bool "for" (Set (Var "D1")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "D1"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "D1")))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "D1"))) ($#r1_tarski :::"c="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "D1")))) ")" )) ; end; :: deftheorem defines :::"<="::: INTEGRA1:def 18 : (Bool "for" (Set (Var "D1")) "," (Set (Var "D2")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool (Set (Var "D1")) ($#r1_integra1 :::"<="::: ) (Set (Var "D2"))) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "D1"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "D2")))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "D1"))) ($#r1_tarski :::"c="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "D2")))) ")" ) ")" )); notationlet "D1", "D2" be ($#m1_hidden :::"FinSequence":::); synonym "D2" :::">="::: "D1" for "D1" :::"<="::: "D2"; end; theorem :: INTEGRA1:29 (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 "D1")) "," (Set (Var "D2")) "being" ($#m1_integra1 :::"Division"::: ) "of" (Set (Var "A")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "D1"))) ($#r1_hidden :::"="::: ) (Num 1))) "holds" (Bool (Set (Var "D1")) ($#r1_integra1 :::"<="::: ) (Set (Var "D2"))))) ; theorem :: INTEGRA1:30 (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 "D1")) "," (Set (Var "D2")) "being" ($#m1_integra1 :::"Division"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A"))) "is" ($#v1_seq_2 :::"bounded_above"::: ) ) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "D1"))) ($#r1_hidden :::"="::: ) (Num 1))) "holds" (Bool (Set ($#k6_integra1 :::"upper_sum"::: ) "(" (Set (Var "f")) "," (Set (Var "D1")) ")" ) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_integra1 :::"upper_sum"::: ) "(" (Set (Var "f")) "," (Set (Var "D2")) ")" ))))) ; theorem :: INTEGRA1:31 (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 "D1")) "," (Set (Var "D2")) "being" ($#m1_integra1 :::"Division"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A"))) "is" ($#v2_seq_2 :::"bounded_below"::: ) ) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "D1"))) ($#r1_hidden :::"="::: ) (Num 1))) "holds" (Bool (Set ($#k7_integra1 :::"lower_sum"::: ) "(" (Set (Var "f")) "," (Set (Var "D1")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k7_integra1 :::"lower_sum"::: ) "(" (Set (Var "f")) "," (Set (Var "D2")) ")" ))))) ; theorem :: INTEGRA1:32 (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (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 "D")) "being" ($#m1_integra1 :::"Division"::: ) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "D"))))) "holds" (Bool "ex" (Set (Var "A1")) "," (Set (Var "A2")) "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 "A1")) ($#r1_hidden :::"="::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" ($#k5_seq_4 :::"lower_bound"::: ) (Set (Var "A")) ")" ) "," (Set "(" (Set (Var "D")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k1_rcomp_1 :::".]"::: ) )) & (Bool (Set (Var "A2")) ($#r1_hidden :::"="::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" (Set (Var "D")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")) ")" ) "," (Set "(" ($#k4_seq_4 :::"upper_bound"::: ) (Set (Var "A")) ")" ) ($#k1_rcomp_1 :::".]"::: ) )) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set (Var "A1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "A2")))) ")" ))))) ; theorem :: INTEGRA1:33 (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (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 "D1")) "," (Set (Var "D2")) "being" ($#m1_integra1 :::"Division"::: ) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "D1")))) & (Bool (Set (Var "D1")) ($#r1_integra1 :::"<="::: ) (Set (Var "D2")))) "holds" (Bool "ex" (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "D2")))) & (Bool (Set (Set (Var "D1")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "D2")) ($#k1_seq_1 :::"."::: ) (Set (Var "j")))) ")" ))))) ; 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 "D1", "D2" be ($#m1_integra1 :::"Division"::: ) "of" (Set (Const "A")); let "i" be ($#m1_hidden :::"Nat":::); assume (Bool (Set (Const "D1")) ($#r1_integra1 :::"<="::: ) (Set (Const "D2"))) ; func :::"indx"::: "(" "D2" "," "D1" "," "i" ")" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) means :: INTEGRA1:def 19 (Bool "(" (Bool it ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "D2")) & (Bool (Set "D1" ($#k1_seq_1 :::"."::: ) "i") ($#r1_hidden :::"="::: ) (Set "D2" ($#k1_seq_1 :::"."::: ) it)) ")" ) if (Bool "i" ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "D1")) otherwise (Bool it ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )); end; :: deftheorem defines :::"indx"::: INTEGRA1:def 19 : (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 "D1")) "," (Set (Var "D2")) "being" ($#m1_integra1 :::"Division"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "D1")) ($#r1_integra1 :::"<="::: ) (Set (Var "D2")))) "holds" (Bool "for" (Set (Var "b5")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "D1"))))) "implies" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k13_integra1 :::"indx"::: ) "(" (Set (Var "D2")) "," (Set (Var "D1")) "," (Set (Var "i")) ")" )) "iff" (Bool "(" (Bool (Set (Var "b5")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "D2")))) & (Bool (Set (Set (Var "D1")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "D2")) ($#k1_seq_1 :::"."::: ) (Set (Var "b5")))) ")" ) ")" ) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "D1")))))) "implies" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k13_integra1 :::"indx"::: ) "(" (Set (Var "D2")) "," (Set (Var "D1")) "," (Set (Var "i")) ")" )) "iff" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" ")" ))))); theorem :: INTEGRA1:34 (Bool "for" (Set (Var "p")) "being" ($#v5_valued_0 :::"increasing"::: ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set (Var "p")) ($#k2_rfinseq :::"/^"::: ) (Set (Var "n"))) "is" ($#v5_valued_0 :::"increasing"::: ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) )))) ; theorem :: INTEGRA1:35 (Bool "for" (Set (Var "p")) "being" ($#v5_valued_0 :::"increasing"::: ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p")))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j")))) "holds" (Bool (Set ($#k3_finseq_6 :::"mid"::: ) "(" (Set (Var "p")) "," (Set (Var "i")) "," (Set (Var "j")) ")" ) "is" ($#v5_valued_0 :::"increasing"::: ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) )))) ; theorem :: INTEGRA1:36 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (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 "D")) "being" ($#m1_integra1 :::"Division"::: ) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "D")))) & (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "D")))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j")))) "holds" (Bool "ex" (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 ($#k5_seq_4 :::"lower_bound"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_finseq_6 :::"mid"::: ) "(" (Set (Var "D")) "," (Set (Var "i")) "," (Set (Var "j")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Num 1))) & (Bool (Set ($#k4_seq_4 :::"upper_bound"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_finseq_6 :::"mid"::: ) "(" (Set (Var "D")) "," (Set (Var "i")) "," (Set (Var "j")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k3_finseq_6 :::"mid"::: ) "(" (Set (Var "D")) "," (Set (Var "i")) "," (Set (Var "j")) ")" ")" ) ")" ))) & (Bool (Set ($#k3_finseq_6 :::"mid"::: ) "(" (Set (Var "D")) "," (Set (Var "i")) "," (Set (Var "j")) ")" ) "is" ($#m1_integra1 :::"Division"::: ) "of" (Set (Var "B"))) ")" ))))) ; theorem :: INTEGRA1:37 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (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"::: ) ) (Bool "for" (Set (Var "D")) "being" ($#m1_integra1 :::"Division"::: ) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "D")))) & (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "D")))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Set (Var "D")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::">="::: ) (Set ($#k5_seq_4 :::"lower_bound"::: ) (Set (Var "B")))) & (Bool (Set (Set (Var "D")) ($#k1_seq_1 :::"."::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set ($#k4_seq_4 :::"upper_bound"::: ) (Set (Var "B"))))) "holds" (Bool (Set ($#k3_finseq_6 :::"mid"::: ) "(" (Set (Var "D")) "," (Set (Var "i")) "," (Set (Var "j")) ")" ) "is" ($#m1_integra1 :::"Division"::: ) "of" (Set (Var "B")))))) ; definitionlet "p" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ); func :::"PartSums"::: "p" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) means :: INTEGRA1:def 20 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "p")) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "p"))) "holds" (Bool (Set it ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" "p" ($#k17_finseq_1 :::"|"::: ) (Set (Var "i")) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"PartSums"::: INTEGRA1:def 20 : (Bool "for" (Set (Var "p")) "," (Set (Var "b2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k14_integra1 :::"PartSums"::: ) (Set (Var "p")))) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set (Var "b2")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" (Set (Var "p")) ($#k17_finseq_1 :::"|"::: ) (Set (Var "i")) ")" ))) ")" ) ")" ) ")" )); theorem :: INTEGRA1:38 (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 "D1")) "," (Set (Var "D2")) "being" ($#m1_integra1 :::"Division"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "D1")) ($#r1_integra1 :::"<="::: ) (Set (Var "D2"))) & (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A"))) "is" ($#v1_seq_2 :::"bounded_above"::: ) )) "holds" (Bool "for" (Set (Var "i")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#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 "D1"))))) "holds" (Bool (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" (Set "(" ($#k4_integra1 :::"upper_volume"::: ) "(" (Set (Var "f")) "," (Set (Var "D1")) ")" ")" ) ($#k17_finseq_1 :::"|"::: ) (Set (Var "i")) ")" )) ($#r1_xxreal_0 :::">="::: ) (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" (Set "(" ($#k4_integra1 :::"upper_volume"::: ) "(" (Set (Var "f")) "," (Set (Var "D2")) ")" ")" ) ($#k17_finseq_1 :::"|"::: ) (Set "(" ($#k13_integra1 :::"indx"::: ) "(" (Set (Var "D2")) "," (Set (Var "D1")) "," (Set (Var "i")) ")" ")" ) ")" ))))))) ; theorem :: INTEGRA1:39 (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 "D1")) "," (Set (Var "D2")) "being" ($#m1_integra1 :::"Division"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "D1")) ($#r1_integra1 :::"<="::: ) (Set (Var "D2"))) & (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A"))) "is" ($#v2_seq_2 :::"bounded_below"::: ) )) "holds" (Bool "for" (Set (Var "i")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#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 "D1"))))) "holds" (Bool (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" (Set "(" ($#k5_integra1 :::"lower_volume"::: ) "(" (Set (Var "f")) "," (Set (Var "D1")) ")" ")" ) ($#k17_finseq_1 :::"|"::: ) (Set (Var "i")) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" (Set "(" ($#k5_integra1 :::"lower_volume"::: ) "(" (Set (Var "f")) "," (Set (Var "D2")) ")" ")" ) ($#k17_finseq_1 :::"|"::: ) (Set "(" ($#k13_integra1 :::"indx"::: ) "(" (Set (Var "D2")) "," (Set (Var "D1")) "," (Set (Var "i")) ")" ")" ) ")" ))))))) ; theorem :: INTEGRA1:40 (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (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 "D1")) "," (Set (Var "D2")) "being" ($#m1_integra1 :::"Division"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "D1")) ($#r1_integra1 :::"<="::: ) (Set (Var "D2"))) & (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "D1")))) & (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A"))) "is" ($#v1_seq_2 :::"bounded_above"::: ) )) "holds" (Bool (Set (Set "(" ($#k14_integra1 :::"PartSums"::: ) (Set "(" ($#k4_integra1 :::"upper_volume"::: ) "(" (Set (Var "f")) "," (Set (Var "D1")) ")" ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::">="::: ) (Set (Set "(" ($#k14_integra1 :::"PartSums"::: ) (Set "(" ($#k4_integra1 :::"upper_volume"::: ) "(" (Set (Var "f")) "," (Set (Var "D2")) ")" ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set "(" ($#k13_integra1 :::"indx"::: ) "(" (Set (Var "D2")) "," (Set (Var "D1")) "," (Set (Var "i")) ")" ")" ))))))) ; theorem :: INTEGRA1:41 (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (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 "D1")) "," (Set (Var "D2")) "being" ($#m1_integra1 :::"Division"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "D1")) ($#r1_integra1 :::"<="::: ) (Set (Var "D2"))) & (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "D1")))) & (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A"))) "is" ($#v2_seq_2 :::"bounded_below"::: ) )) "holds" (Bool (Set (Set "(" ($#k14_integra1 :::"PartSums"::: ) (Set "(" ($#k5_integra1 :::"lower_volume"::: ) "(" (Set (Var "f")) "," (Set (Var "D1")) ")" ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k14_integra1 :::"PartSums"::: ) (Set "(" ($#k5_integra1 :::"lower_volume"::: ) "(" (Set (Var "f")) "," (Set (Var "D2")) ")" ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set "(" ($#k13_integra1 :::"indx"::: ) "(" (Set (Var "D2")) "," (Set (Var "D1")) "," (Set (Var "i")) ")" ")" ))))))) ; theorem :: INTEGRA1:42 (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 "D")) "being" ($#m1_integra1 :::"Division"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set "(" ($#k14_integra1 :::"PartSums"::: ) (Set "(" ($#k4_integra1 :::"upper_volume"::: ) "(" (Set (Var "f")) "," (Set (Var "D")) ")" ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "D")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_integra1 :::"upper_sum"::: ) "(" (Set (Var "f")) "," (Set (Var "D")) ")" ))))) ; theorem :: INTEGRA1:43 (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 "D")) "being" ($#m1_integra1 :::"Division"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set "(" ($#k14_integra1 :::"PartSums"::: ) (Set "(" ($#k5_integra1 :::"lower_volume"::: ) "(" (Set (Var "f")) "," (Set (Var "D")) ")" ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "D")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k7_integra1 :::"lower_sum"::: ) "(" (Set (Var "f")) "," (Set (Var "D")) ")" ))))) ; theorem :: INTEGRA1:44 (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 "D1")) "," (Set (Var "D2")) "being" ($#m1_integra1 :::"Division"::: ) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "D1")) ($#r1_integra1 :::"<="::: ) (Set (Var "D2")))) "holds" (Bool (Set ($#k13_integra1 :::"indx"::: ) "(" (Set (Var "D2")) "," (Set (Var "D1")) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "D1")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "D2")))))) ; theorem :: INTEGRA1:45 (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 "D1")) "," (Set (Var "D2")) "being" ($#m1_integra1 :::"Division"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "D1")) ($#r1_integra1 :::"<="::: ) (Set (Var "D2"))) & (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A"))) "is" ($#v1_seq_2 :::"bounded_above"::: ) )) "holds" (Bool (Set ($#k6_integra1 :::"upper_sum"::: ) "(" (Set (Var "f")) "," (Set (Var "D2")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_integra1 :::"upper_sum"::: ) "(" (Set (Var "f")) "," (Set (Var "D1")) ")" ))))) ; theorem :: INTEGRA1:46 (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 "D1")) "," (Set (Var "D2")) "being" ($#m1_integra1 :::"Division"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "D1")) ($#r1_integra1 :::"<="::: ) (Set (Var "D2"))) & (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A"))) "is" ($#v2_seq_2 :::"bounded_below"::: ) )) "holds" (Bool (Set ($#k7_integra1 :::"lower_sum"::: ) "(" (Set (Var "f")) "," (Set (Var "D2")) ")" ) ($#r1_xxreal_0 :::">="::: ) (Set ($#k7_integra1 :::"lower_sum"::: ) "(" (Set (Var "f")) "," (Set (Var "D1")) ")" ))))) ; theorem :: INTEGRA1:47 (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 "D1")) "," (Set (Var "D2")) "being" ($#m1_integra1 :::"Division"::: ) "of" (Set (Var "A")) (Bool "ex" (Set (Var "D")) "being" ($#m1_integra1 :::"Division"::: ) "of" (Set (Var "A")) "st" (Bool "(" (Bool (Set (Var "D1")) ($#r1_integra1 :::"<="::: ) (Set (Var "D"))) & (Bool (Set (Var "D2")) ($#r1_integra1 :::"<="::: ) (Set (Var "D"))) ")" )))) ; theorem :: INTEGRA1:48 (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 "D1")) "," (Set (Var "D2")) "being" ($#m1_integra1 :::"Division"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A"))) "is" ($#v1_comseq_2 :::"bounded"::: ) )) "holds" (Bool (Set ($#k7_integra1 :::"lower_sum"::: ) "(" (Set (Var "f")) "," (Set (Var "D1")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_integra1 :::"upper_sum"::: ) "(" (Set (Var "f")) "," (Set (Var "D2")) ")" ))))) ; begin theorem :: INTEGRA1:49 (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 :::"Function":::) "of" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A"))) "is" ($#v1_comseq_2 :::"bounded"::: ) )) "holds" (Bool (Set ($#k10_integra1 :::"upper_integral"::: ) (Set (Var "f"))) ($#r1_xxreal_0 :::">="::: ) (Set ($#k11_integra1 :::"lower_integral"::: ) (Set (Var "f")))))) ; theorem :: INTEGRA1:50 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set "(" ($#k4_measure6 :::"--"::: ) (Set (Var "X")) ")" ) ($#k9_member_1 :::"++"::: ) (Set "(" ($#k4_measure6 :::"--"::: ) (Set (Var "Y")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_member_1 :::"--"::: ) (Set "(" (Set (Var "X")) ($#k9_member_1 :::"++"::: ) (Set (Var "Y")) ")" )))) ; theorem :: INTEGRA1:51 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "X")) "is" ($#v4_xxreal_2 :::"bounded_above"::: ) ) & (Bool (Set (Var "Y")) "is" ($#v4_xxreal_2 :::"bounded_above"::: ) )) "holds" (Bool (Set (Set (Var "X")) ($#k9_member_1 :::"++"::: ) (Set (Var "Y"))) "is" ($#v4_xxreal_2 :::"bounded_above"::: ) )) ; theorem :: INTEGRA1:52 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "X")) "is" ($#v4_xxreal_2 :::"bounded_above"::: ) ) & (Bool (Set (Var "Y")) "is" ($#v4_xxreal_2 :::"bounded_above"::: ) )) "holds" (Bool (Set ($#k2_seq_4 :::"upper_bound"::: ) (Set "(" (Set (Var "X")) ($#k9_member_1 :::"++"::: ) (Set (Var "Y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_seq_4 :::"upper_bound"::: ) (Set (Var "X")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k4_seq_4 :::"upper_bound"::: ) (Set (Var "Y")) ")" )))) ; theorem :: INTEGRA1:53 (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (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 "D")) "being" ($#m1_integra1 :::"Division"::: ) "of" (Set (Var "A")) (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 (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "D")))) & (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A"))) "is" ($#v1_seq_2 :::"bounded_above"::: ) ) & (Bool (Set (Set (Var "g")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A"))) "is" ($#v1_seq_2 :::"bounded_above"::: ) )) "holds" (Bool (Set (Set "(" ($#k4_integra1 :::"upper_volume"::: ) "(" (Set "(" (Set (Var "f")) ($#k3_valued_1 :::"+"::: ) (Set (Var "g")) ")" ) "," (Set (Var "D")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set "(" ($#k4_integra1 :::"upper_volume"::: ) "(" (Set (Var "f")) "," (Set (Var "D")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k4_integra1 :::"upper_volume"::: ) "(" (Set (Var "g")) "," (Set (Var "D")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "i")) ")" ))))))) ; theorem :: INTEGRA1:54 (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (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 "D")) "being" ($#m1_integra1 :::"Division"::: ) "of" (Set (Var "A")) (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 (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "D")))) & (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A"))) "is" ($#v2_seq_2 :::"bounded_below"::: ) ) & (Bool (Set (Set (Var "g")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A"))) "is" ($#v2_seq_2 :::"bounded_below"::: ) )) "holds" (Bool (Set (Set "(" (Set "(" ($#k5_integra1 :::"lower_volume"::: ) "(" (Set (Var "f")) "," (Set (Var "D")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k5_integra1 :::"lower_volume"::: ) "(" (Set (Var "g")) "," (Set (Var "D")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "i")) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k5_integra1 :::"lower_volume"::: ) "(" (Set "(" (Set (Var "f")) ($#k3_valued_1 :::"+"::: ) (Set (Var "g")) ")" ) "," (Set (Var "D")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))))))) ; theorem :: INTEGRA1:55 (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 "D")) "being" ($#m1_integra1 :::"Division"::: ) "of" (Set (Var "A")) (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 (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A"))) "is" ($#v1_seq_2 :::"bounded_above"::: ) ) & (Bool (Set (Set (Var "g")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A"))) "is" ($#v1_seq_2 :::"bounded_above"::: ) )) "holds" (Bool (Set ($#k6_integra1 :::"upper_sum"::: ) "(" (Set "(" (Set (Var "f")) ($#k3_valued_1 :::"+"::: ) (Set (Var "g")) ")" ) "," (Set (Var "D")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k6_integra1 :::"upper_sum"::: ) "(" (Set (Var "f")) "," (Set (Var "D")) ")" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k6_integra1 :::"upper_sum"::: ) "(" (Set (Var "g")) "," (Set (Var "D")) ")" ")" )))))) ; theorem :: INTEGRA1:56 (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 "D")) "being" ($#m1_integra1 :::"Division"::: ) "of" (Set (Var "A")) (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 (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A"))) "is" ($#v2_seq_2 :::"bounded_below"::: ) ) & (Bool (Set (Set (Var "g")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A"))) "is" ($#v2_seq_2 :::"bounded_below"::: ) )) "holds" (Bool (Set (Set "(" ($#k7_integra1 :::"lower_sum"::: ) "(" (Set (Var "f")) "," (Set (Var "D")) ")" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k7_integra1 :::"lower_sum"::: ) "(" (Set (Var "g")) "," (Set (Var "D")) ")" ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k7_integra1 :::"lower_sum"::: ) "(" (Set "(" (Set (Var "f")) ($#k3_valued_1 :::"+"::: ) (Set (Var "g")) ")" ) "," (Set (Var "D")) ")" ))))) ; theorem :: INTEGRA1:57 (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 :::"Function":::) "of" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A"))) "is" ($#v1_comseq_2 :::"bounded"::: ) ) & (Bool (Set (Set (Var "g")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A"))) "is" ($#v1_comseq_2 :::"bounded"::: ) ) & (Bool (Set (Var "f")) "is" ($#v3_integra1 :::"integrable"::: ) ) & (Bool (Set (Var "g")) "is" ($#v3_integra1 :::"integrable"::: ) )) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k3_valued_1 :::"+"::: ) (Set (Var "g"))) "is" ($#v3_integra1 :::"integrable"::: ) ) & (Bool (Set ($#k12_integra1 :::"integral"::: ) (Set "(" (Set (Var "f")) ($#k3_valued_1 :::"+"::: ) (Set (Var "g")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k12_integra1 :::"integral"::: ) (Set (Var "f")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k12_integra1 :::"integral"::: ) (Set (Var "g")) ")" ))) ")" ))) ; theorem :: INTEGRA1:58 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j")))) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k2_finseq_6 :::"mid"::: ) "(" (Set (Var "f")) "," (Set (Var "i")) "," (Set (Var "j")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "j")) ($#k9_real_1 :::"-"::: ) (Set (Var "i")) ")" ) ($#k7_real_1 :::"+"::: ) (Num 1))))) ;