:: INTEGRA2 semantic presentation begin theorem :: INTEGRA2: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 "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) "iff" (Bool "(" (Bool (Set ($#k5_seq_4 :::"lower_bound"::: ) (Set (Var "A"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "x"))) & (Bool (Set (Var "x")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k4_seq_4 :::"upper_bound"::: ) (Set (Var "A")))) ")" ) ")" ))) ; definitionlet "IT" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ); attr "IT" is :::"non-decreasing"::: means :: INTEGRA2:def 1 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "IT")) & (Bool (Set (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "IT"))) "holds" (Bool (Set "IT" ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<="::: ) (Set "IT" ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )))); end; :: deftheorem defines :::"non-decreasing"::: INTEGRA2:def 1 : (Bool "for" (Set (Var "IT")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v1_integra2 :::"non-decreasing"::: ) ) "iff" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "IT")))) & (Bool (Set (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "IT"))))) "holds" (Bool (Set (Set (Var "IT")) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "IT")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )))) ")" )); registration cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_VALUED_0() bbbadV2_VALUED_0() bbbadV3_VALUED_0() bbbadV1_FINSET_1() ($#v1_finseq_1 :::"FinSequence-like"::: ) ($#v2_finseq_1 :::"FinSubsequence-like"::: ) ($#v1_integra2 :::"non-decreasing"::: ) for ($#m1_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ); end; theorem :: INTEGRA2:2 (Bool "for" (Set (Var "p")) "being" ($#v1_integra2 :::"non-decreasing"::: ) ($#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 "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p")))) & (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 (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Set (Var "j")))))) ; theorem :: INTEGRA2:3 (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "ex" (Set (Var "q")) "being" ($#v1_integra2 :::"non-decreasing"::: ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r2_classes1 :::"are_fiberwise_equipotent"::: ) ))) ; theorem :: INTEGRA2:4 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "k1")) "," (Set (Var "k2")) "," (Set (Var "k3")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k1"))) & (Bool (Set (Var "k3")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool (Set (Var "k1")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k2"))) & (Bool (Set (Var "k2")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "k3")))) "holds" (Bool (Set (Set "(" ($#k3_finseq_6 :::"mid"::: ) "(" (Set (Var "f")) "," (Set (Var "k1")) "," (Set (Var "k2")) ")" ")" ) ($#k8_finseq_1 :::"^"::: ) (Set "(" ($#k3_finseq_6 :::"mid"::: ) "(" (Set (Var "f")) "," (Set "(" (Set (Var "k2")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "k3")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_6 :::"mid"::: ) "(" (Set (Var "f")) "," (Set (Var "k1")) "," (Set (Var "k3")) ")" ))))) ; begin definitionlet "A" be ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "x" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; :: original: :::"**"::: redefine func "x" :::"**"::: "A" -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ); end; theorem :: INTEGRA2:5 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "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"::: ) ) & (Bool (Set (Var "Y")) ($#r1_tarski :::"c="::: ) (Set (Var "X")))) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "Y")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set (Var "Y"))) "is" ($#v1_seq_2 :::"bounded_above"::: ) ))) ; theorem :: INTEGRA2:6 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "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"::: ) ) & (Bool (Set (Var "Y")) ($#r1_tarski :::"c="::: ) (Set (Var "X")))) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "Y")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set (Var "Y"))) "is" ($#v2_seq_2 :::"bounded_below"::: ) ))) ; theorem :: INTEGRA2:7 (Bool "for" (Set (Var "X")) "being" ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "iff" (Bool (Set (Set (Var "a")) ($#k1_integra2 :::"**"::: ) (Set (Var "X"))) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" ))) ; theorem :: INTEGRA2:8 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set (Var "r")) ($#k1_integra2 :::"**"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "r")) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) where x "is" ($#m1_subset_1 :::"Real":::) : (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) "}" ))) ; theorem :: INTEGRA2:9 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "X")) "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 ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r")))) "holds" (Bool (Set (Set (Var "r")) ($#k1_integra2 :::"**"::: ) (Set (Var "X"))) "is" ($#v4_xxreal_2 :::"bounded_above"::: ) ))) ; theorem :: INTEGRA2:10 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "X")) "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 "r")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set (Var "r")) ($#k1_integra2 :::"**"::: ) (Set (Var "X"))) "is" ($#v3_xxreal_2 :::"bounded_below"::: ) ))) ; theorem :: INTEGRA2:11 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "X")) "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" ($#v3_xxreal_2 :::"bounded_below"::: ) ) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r")))) "holds" (Bool (Set (Set (Var "r")) ($#k1_integra2 :::"**"::: ) (Set (Var "X"))) "is" ($#v3_xxreal_2 :::"bounded_below"::: ) ))) ; theorem :: INTEGRA2:12 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "X")) "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" ($#v3_xxreal_2 :::"bounded_below"::: ) ) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set (Var "r")) ($#k1_integra2 :::"**"::: ) (Set (Var "X"))) "is" ($#v4_xxreal_2 :::"bounded_above"::: ) ))) ; theorem :: INTEGRA2:13 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "X")) "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 ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r")))) "holds" (Bool (Set ($#k4_seq_4 :::"upper_bound"::: ) (Set "(" (Set (Var "r")) ($#k1_integra2 :::"**"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k4_seq_4 :::"upper_bound"::: ) (Set (Var "X")) ")" ))))) ; theorem :: INTEGRA2:14 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "X")) "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 "r")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k5_seq_4 :::"lower_bound"::: ) (Set "(" (Set (Var "r")) ($#k1_integra2 :::"**"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k4_seq_4 :::"upper_bound"::: ) (Set (Var "X")) ")" ))))) ; theorem :: INTEGRA2:15 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "X")) "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" ($#v3_xxreal_2 :::"bounded_below"::: ) ) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r")))) "holds" (Bool (Set ($#k5_seq_4 :::"lower_bound"::: ) (Set "(" (Set (Var "r")) ($#k1_integra2 :::"**"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k5_seq_4 :::"lower_bound"::: ) (Set (Var "X")) ")" ))))) ; theorem :: INTEGRA2:16 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "X")) "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" ($#v3_xxreal_2 :::"bounded_below"::: ) ) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k4_seq_4 :::"upper_bound"::: ) (Set "(" (Set (Var "r")) ($#k1_integra2 :::"**"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k5_seq_4 :::"lower_bound"::: ) (Set (Var "X")) ")" ))))) ; begin theorem :: INTEGRA2:17 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (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 :::"Function":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k1_rvsum_1 :::"rng"::: ) (Set "(" (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k1_integra2 :::"**"::: ) (Set "(" ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "f")) ")" )))))) ; theorem :: INTEGRA2:18 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "X")) "," (Set (Var "Z")) "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"::: ) ) "holds" (Bool (Set ($#k1_rvsum_1 :::"rng"::: ) (Set "(" (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "Z")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k1_integra2 :::"**"::: ) (Set "(" ($#k1_rvsum_1 :::"rng"::: ) (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "Z")) ")" ) ")" )))))) ; theorem :: INTEGRA2:19 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"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 "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "D")) "being" ($#m1_integra1 :::"Division"::: ) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A"))) "is" ($#v1_comseq_2 :::"bounded"::: ) ) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" ($#k8_integra1 :::"upper_sum_set"::: ) (Set "(" (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f")) ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "D"))) ($#r1_xxreal_0 :::">="::: ) (Set (Set "(" (Set (Var "r")) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k5_seq_4 :::"lower_bound"::: ) (Set "(" ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "f")) ")" ) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k3_integra1 :::"vol"::: ) (Set (Var "A")) ")" ))))))) ; theorem :: INTEGRA2:20 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"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 "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "D")) "being" ($#m1_integra1 :::"Division"::: ) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A"))) "is" ($#v1_comseq_2 :::"bounded"::: ) ) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" ($#k8_integra1 :::"upper_sum_set"::: ) (Set "(" (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f")) ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "D"))) ($#r1_xxreal_0 :::">="::: ) (Set (Set "(" (Set (Var "r")) ($#k8_real_1 :::"*"::: ) (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 :: INTEGRA2:21 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"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 "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "D")) "being" ($#m1_integra1 :::"Division"::: ) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A"))) "is" ($#v1_comseq_2 :::"bounded"::: ) ) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" ($#k9_integra1 :::"lower_sum_set"::: ) (Set "(" (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f")) ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "D"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set (Var "r")) ($#k8_real_1 :::"*"::: ) (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 :: INTEGRA2:22 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"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 "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "D")) "being" ($#m1_integra1 :::"Division"::: ) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A"))) "is" ($#v1_comseq_2 :::"bounded"::: ) ) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" ($#k9_integra1 :::"lower_sum_set"::: ) (Set "(" (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f")) ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "D"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set (Var "r")) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k5_seq_4 :::"lower_bound"::: ) (Set "(" ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "f")) ")" ) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k3_integra1 :::"vol"::: ) (Set (Var "A")) ")" ))))))) ; theorem :: INTEGRA2:23 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (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 "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (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 (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A"))) "is" ($#v1_seq_2 :::"bounded_above"::: ) ) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" ($#k4_integra1 :::"upper_volume"::: ) "(" (Set "(" (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f")) ")" ) "," (Set (Var "D")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" ($#k4_integra1 :::"upper_volume"::: ) "(" (Set (Var "f")) "," (Set (Var "D")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "i")) ")" )))))))) ; theorem :: INTEGRA2:24 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (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 "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (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 (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A"))) "is" ($#v1_seq_2 :::"bounded_above"::: ) ) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" ($#k5_integra1 :::"lower_volume"::: ) "(" (Set "(" (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f")) ")" ) "," (Set (Var "D")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" ($#k4_integra1 :::"upper_volume"::: ) "(" (Set (Var "f")) "," (Set (Var "D")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "i")) ")" )))))))) ; theorem :: INTEGRA2:25 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (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 "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (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 (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A"))) "is" ($#v2_seq_2 :::"bounded_below"::: ) ) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" ($#k5_integra1 :::"lower_volume"::: ) "(" (Set "(" (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f")) ")" ) "," (Set (Var "D")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" ($#k5_integra1 :::"lower_volume"::: ) "(" (Set (Var "f")) "," (Set (Var "D")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "i")) ")" )))))))) ; theorem :: INTEGRA2:26 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (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 "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (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 (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A"))) "is" ($#v2_seq_2 :::"bounded_below"::: ) ) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" ($#k4_integra1 :::"upper_volume"::: ) "(" (Set "(" (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f")) ")" ) "," (Set (Var "D")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" ($#k5_integra1 :::"lower_volume"::: ) "(" (Set (Var "f")) "," (Set (Var "D")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "i")) ")" )))))))) ; theorem :: INTEGRA2:27 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"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 "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "D")) "being" ($#m1_integra1 :::"Division"::: ) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A"))) "is" ($#v1_seq_2 :::"bounded_above"::: ) ) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k6_integra1 :::"upper_sum"::: ) "(" (Set "(" (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f")) ")" ) "," (Set (Var "D")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k6_integra1 :::"upper_sum"::: ) "(" (Set (Var "f")) "," (Set (Var "D")) ")" ")" ))))))) ; theorem :: INTEGRA2:28 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"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 "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "D")) "being" ($#m1_integra1 :::"Division"::: ) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A"))) "is" ($#v1_seq_2 :::"bounded_above"::: ) ) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k7_integra1 :::"lower_sum"::: ) "(" (Set "(" (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f")) ")" ) "," (Set (Var "D")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k6_integra1 :::"upper_sum"::: ) "(" (Set (Var "f")) "," (Set (Var "D")) ")" ")" ))))))) ; theorem :: INTEGRA2:29 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"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 "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "D")) "being" ($#m1_integra1 :::"Division"::: ) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A"))) "is" ($#v2_seq_2 :::"bounded_below"::: ) ) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k7_integra1 :::"lower_sum"::: ) "(" (Set "(" (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f")) ")" ) "," (Set (Var "D")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k7_integra1 :::"lower_sum"::: ) "(" (Set (Var "f")) "," (Set (Var "D")) ")" ")" ))))))) ; theorem :: INTEGRA2:30 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"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 "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "D")) "being" ($#m1_integra1 :::"Division"::: ) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A"))) "is" ($#v2_seq_2 :::"bounded_below"::: ) ) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k6_integra1 :::"upper_sum"::: ) "(" (Set "(" (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f")) ")" ) "," (Set (Var "D")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k7_integra1 :::"lower_sum"::: ) "(" (Set (Var "f")) "," (Set (Var "D")) ")" ")" ))))))) ; theorem :: INTEGRA2:31 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"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 "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"::: ) ) & (Bool (Set (Var "f")) "is" ($#v3_integra1 :::"integrable"::: ) )) "holds" (Bool "(" (Bool (Set (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f"))) "is" ($#v3_integra1 :::"integrable"::: ) ) & (Bool (Set ($#k12_integra1 :::"integral"::: ) (Set "(" (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k12_integra1 :::"integral"::: ) (Set (Var "f")) ")" ))) ")" )))) ; begin theorem :: INTEGRA2:32 (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"::: ) ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) "holds" (Bool (Set ($#k12_integra1 :::"integral"::: ) (Set (Var "f"))) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )))) ; theorem :: INTEGRA2:33 (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 (Var "f")) "is" ($#v3_integra1 :::"integrable"::: ) ) & (Bool (Set (Set (Var "g")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A"))) "is" ($#v1_comseq_2 :::"bounded"::: ) ) & (Bool (Set (Var "g")) "is" ($#v3_integra1 :::"integrable"::: ) )) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k47_valued_1 :::"-"::: ) (Set (Var "g"))) "is" ($#v3_integra1 :::"integrable"::: ) ) & (Bool (Set ($#k12_integra1 :::"integral"::: ) (Set "(" (Set (Var "f")) ($#k47_valued_1 :::"-"::: ) (Set (Var "g")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k12_integra1 :::"integral"::: ) (Set (Var "f")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k12_integra1 :::"integral"::: ) (Set (Var "g")) ")" ))) ")" ))) ; theorem :: INTEGRA2:34 (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 (Var "f")) "is" ($#v3_integra1 :::"integrable"::: ) ) & (Bool (Set (Set (Var "g")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A"))) "is" ($#v1_comseq_2 :::"bounded"::: ) ) & (Bool (Set (Var "g")) "is" ($#v3_integra1 :::"integrable"::: ) ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::">="::: ) (Set (Set (Var "g")) ($#k1_seq_1 :::"."::: ) (Set (Var "x")))) ")" )) "holds" (Bool (Set ($#k12_integra1 :::"integral"::: ) (Set (Var "f"))) ($#r1_xxreal_0 :::">="::: ) (Set ($#k12_integra1 :::"integral"::: ) (Set (Var "g")))))) ; begin theorem :: INTEGRA2:35 (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 ($#k1_rvsum_1 :::"rng"::: ) (Set "(" ($#k8_integra1 :::"upper_sum_set"::: ) (Set (Var "f")) ")" )) "is" ($#v3_xxreal_2 :::"bounded_below"::: ) ))) ; theorem :: INTEGRA2:36 (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 ($#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"::: ) ); mode DivSequence of "A" is ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k1_integra1 :::"divs"::: ) "A" ")" ); end; 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 "T" be ($#m1_subset_1 :::"DivSequence":::) "of" (Set (Const "A")); let "i" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); :: original: :::"."::: redefine func "T" :::"."::: "i" -> ($#m1_integra1 :::"Division"::: ) "of" "A"; end; 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 "T" be ($#m1_subset_1 :::"DivSequence":::) "of" (Set (Const "A")); func :::"upper_sum"::: "(" "f" "," "T" ")" -> ($#m1_subset_1 :::"Real_Sequence":::) means :: INTEGRA2:def 2 (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set it ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k6_integra1 :::"upper_sum"::: ) "(" "f" "," (Set "(" "T" ($#k2_integra2 :::"."::: ) (Set (Var "i")) ")" ) ")" ))); func :::"lower_sum"::: "(" "f" "," "T" ")" -> ($#m1_subset_1 :::"Real_Sequence":::) means :: INTEGRA2:def 3 (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set it ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k7_integra1 :::"lower_sum"::: ) "(" "f" "," (Set "(" "T" ($#k2_integra2 :::"."::: ) (Set (Var "i")) ")" ) ")" ))); end; :: deftheorem defines :::"upper_sum"::: INTEGRA2: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 (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"DivSequence":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k3_integra2 :::"upper_sum"::: ) "(" (Set (Var "f")) "," (Set (Var "T")) ")" )) "iff" (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "b4")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k6_integra1 :::"upper_sum"::: ) "(" (Set (Var "f")) "," (Set "(" (Set (Var "T")) ($#k2_integra2 :::"."::: ) (Set (Var "i")) ")" ) ")" ))) ")" ))))); :: deftheorem defines :::"lower_sum"::: INTEGRA2:def 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"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"DivSequence":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k4_integra2 :::"lower_sum"::: ) "(" (Set (Var "f")) "," (Set (Var "T")) ")" )) "iff" (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "b4")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k7_integra1 :::"lower_sum"::: ) "(" (Set (Var "f")) "," (Set "(" (Set (Var "T")) ($#k2_integra2 :::"."::: ) (Set (Var "i")) ")" ) ")" ))) ")" ))))); theorem :: INTEGRA2:37 (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 "for" (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"))))) "holds" (Bool "ex" (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 "D1")))) & (Bool (Set ($#k2_integra1 :::"divset"::: ) "(" (Set (Var "D2")) "," (Set (Var "j")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k2_integra1 :::"divset"::: ) "(" (Set (Var "D1")) "," (Set (Var "i")) ")" )) ")" ))))) ; theorem :: INTEGRA2:38 (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 (Var "B")))) "holds" (Bool (Set ($#k3_integra1 :::"vol"::: ) (Set (Var "A"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_integra1 :::"vol"::: ) (Set (Var "B"))))) ; theorem :: INTEGRA2:39 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "a")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "a")) ($#k1_integra2 :::"**"::: ) (Set (Var "A"))))) "holds" (Bool "ex" (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k8_real_1 :::"*"::: ) (Set (Var "b")))) ")" )))) ; begin theorem :: INTEGRA2:40 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set ($#k6_numbers :::"0"::: ) ) ($#k22_member_1 :::"**"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k1_seq_4 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k1_seq_4 :::"}"::: ) ))) ;