:: INTEGRA4 semantic presentation begin theorem :: INTEGRA4: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 "D")) "being" ($#m1_integra1 :::"Division"::: ) "of" (Set (Var "A")) "st" (Bool (Bool (Set ($#k3_integra1 :::"vol"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "D"))) ($#r1_hidden :::"="::: ) (Num 1)))) ; theorem :: INTEGRA4: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"::: ) ) "holds" (Bool "(" (Bool (Set ($#k7_rfunct_1 :::"chi"::: ) "(" (Set (Var "A")) "," (Set (Var "A")) ")" ) "is" ($#v3_integra1 :::"integrable"::: ) ) & (Bool (Set ($#k12_integra1 :::"integral"::: ) (Set "(" ($#k7_rfunct_1 :::"chi"::: ) "(" (Set (Var "A")) "," (Set (Var "A")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_integra1 :::"vol"::: ) (Set (Var "A")))) ")" )) ; theorem :: INTEGRA4: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 "r")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "f")) "is" ($#v1_partfun1 :::"total"::: ) ) & (Bool (Set ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k1_seq_4 :::"{"::: ) (Set (Var "r")) ($#k1_seq_4 :::"}"::: ) )) ")" ) "iff" (Bool (Set (Var "f")) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set "(" ($#k7_rfunct_1 :::"chi"::: ) "(" (Set (Var "A")) "," (Set (Var "A")) ")" ")" ))) ")" )))) ; theorem :: INTEGRA4: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 "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k1_seq_4 :::"{"::: ) (Set (Var "r")) ($#k1_seq_4 :::"}"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v3_integra1 :::"integrable"::: ) ) & (Bool (Set ($#k12_integra1 :::"integral"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k3_integra1 :::"vol"::: ) (Set (Var "A")) ")" ))) ")" )))) ; theorem :: INTEGRA4: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 "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool (Set ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k1_seq_4 :::"{"::: ) (Set (Var "r")) ($#k1_seq_4 :::"}"::: ) )) & (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A"))) "is" ($#v1_comseq_2 :::"bounded"::: ) ) ")" )))) ; theorem :: INTEGRA4: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_subset_1 :::"Element"::: ) "of" (Set ($#k1_integra1 :::"divs"::: ) (Set (Var "A"))) "st" (Bool (Bool (Set ($#k3_integra1 :::"vol"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v3_integra1 :::"integrable"::: ) ) & (Bool (Set ($#k12_integra1 :::"integral"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )))) ; theorem :: INTEGRA4: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 :::"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 "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set ($#k5_seq_4 :::"lower_bound"::: ) (Set "(" ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "f")) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "a"))) & (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k4_seq_4 :::"upper_bound"::: ) (Set "(" ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "f")) ")" ))) & (Bool (Set ($#k12_integra1 :::"integral"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k3_integra1 :::"vol"::: ) (Set (Var "A")) ")" ))) ")" )))) ; begin theorem :: INTEGRA4: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 :::"Function":::) "of" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"DivSequence":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A"))) "is" ($#v1_comseq_2 :::"bounded"::: ) ) & (Bool (Set ($#k2_integra3 :::"delta"::: ) (Set (Var "T"))) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set "(" ($#k2_integra3 :::"delta"::: ) (Set (Var "T")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k4_integra2 :::"lower_sum"::: ) "(" (Set (Var "f")) "," (Set (Var "T")) ")" ) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set "(" ($#k4_integra2 :::"lower_sum"::: ) "(" (Set (Var "f")) "," (Set (Var "T")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k11_integra1 :::"lower_integral"::: ) (Set (Var "f")))) ")" )))) ; theorem :: INTEGRA4: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 :::"Function":::) "of" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"DivSequence":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A"))) "is" ($#v1_comseq_2 :::"bounded"::: ) ) & (Bool (Set ($#k2_integra3 :::"delta"::: ) (Set (Var "T"))) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set "(" ($#k2_integra3 :::"delta"::: ) (Set (Var "T")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k3_integra2 :::"upper_sum"::: ) "(" (Set (Var "f")) "," (Set (Var "T")) ")" ) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set "(" ($#k3_integra2 :::"upper_sum"::: ) "(" (Set (Var "f")) "," (Set (Var "T")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k10_integra1 :::"upper_integral"::: ) (Set (Var "f")))) ")" )))) ; theorem :: INTEGRA4: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 :::"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 "(" (Bool (Set (Var "f")) "is" ($#v1_integra1 :::"upper_integrable"::: ) ) & (Bool (Set (Var "f")) "is" ($#v2_integra1 :::"lower_integrable"::: ) ) ")" ))) ; definitionlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_measure5 :::"closed_interval"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ); let "IT" be ($#m1_integra1 :::"Division"::: ) "of" (Set (Const "A")); let "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); pred "IT" :::"divide_into_equal"::: "n" means :: INTEGRA4:def 1 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) "IT") ($#r1_hidden :::"="::: ) "n") & (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "IT"))) "holds" (Bool (Set "IT" ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_seq_4 :::"lower_bound"::: ) "A" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Set "(" ($#k3_integra1 :::"vol"::: ) "A" ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) "IT" ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set (Var "i")) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"divide_into_equal"::: INTEGRA4:def 1 : (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_measure5 :::"closed_interval"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "IT")) "being" ($#m1_integra1 :::"Division"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "IT")) ($#r1_integra4 :::"divide_into_equal"::: ) (Set (Var "n"))) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "IT"))) ($#r1_hidden :::"="::: ) (Set (Var "n"))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "IT"))))) "holds" (Bool (Set (Set (Var "IT")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_seq_4 :::"lower_bound"::: ) (Set (Var "A")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Set "(" ($#k3_integra1 :::"vol"::: ) (Set (Var "A")) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "IT")) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set (Var "i")) ")" ))) ")" ) ")" ) ")" )))); theorem :: INTEGRA4: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 "ex" (Set (Var "T")) "being" ($#m1_subset_1 :::"DivSequence":::) "of" (Set (Var "A")) "st" (Bool "(" (Bool (Set ($#k2_integra3 :::"delta"::: ) (Set (Var "T"))) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set "(" ($#k2_integra3 :::"delta"::: ) (Set (Var "T")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ))) ; theorem :: INTEGRA4: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 :::"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 "(" (Bool (Set (Var "f")) "is" ($#v3_integra1 :::"integrable"::: ) ) "iff" (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"DivSequence":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set ($#k2_integra3 :::"delta"::: ) (Set (Var "T"))) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set "(" ($#k2_integra3 :::"delta"::: ) (Set (Var "T")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" ($#k2_seq_2 :::"lim"::: ) (Set "(" ($#k3_integra2 :::"upper_sum"::: ) "(" (Set (Var "f")) "," (Set (Var "T")) ")" ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k2_seq_2 :::"lim"::: ) (Set "(" ($#k4_integra2 :::"lower_sum"::: ) "(" (Set (Var "f")) "," (Set (Var "T")) ")" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ")" ))) ; theorem :: INTEGRA4:13 (Bool "for" (Set (Var "C")) "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 "C")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set ($#k18_rfunct_3 :::"max+"::: ) (Set (Var "f"))) "is" ($#v1_partfun1 :::"total"::: ) ) & (Bool (Set ($#k19_rfunct_3 :::"max-"::: ) (Set (Var "f"))) "is" ($#v1_partfun1 :::"total"::: ) ) ")" ))) ; theorem :: INTEGRA4:14 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (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 (Set "(" ($#k18_rfunct_3 :::"max+"::: ) (Set (Var "f")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) "is" ($#v1_seq_2 :::"bounded_above"::: ) )))) ; theorem :: INTEGRA4:15 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set "(" ($#k18_rfunct_3 :::"max+"::: ) (Set (Var "f")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) "is" ($#v2_seq_2 :::"bounded_below"::: ) )))) ; theorem :: INTEGRA4:16 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (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 (Set "(" ($#k19_rfunct_3 :::"max-"::: ) (Set (Var "f")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) "is" ($#v1_seq_2 :::"bounded_above"::: ) )))) ; theorem :: INTEGRA4:17 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set "(" ($#k19_rfunct_3 :::"max-"::: ) (Set (Var "f")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) "is" ($#v2_seq_2 :::"bounded_below"::: ) )))) ; theorem :: INTEGRA4:18 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_measure5 :::"closed_interval"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (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 ($#k1_rvsum_1 :::"rng"::: ) (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X")) ")" )) "is" ($#v4_xxreal_2 :::"bounded_above"::: ) )))) ; theorem :: INTEGRA4: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 "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "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 ($#k1_rvsum_1 :::"rng"::: ) (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X")) ")" )) "is" ($#v3_xxreal_2 :::"bounded_below"::: ) )))) ; theorem :: INTEGRA4:20 (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 (Set ($#k18_rfunct_3 :::"max+"::: ) (Set (Var "f"))) "is" ($#v3_integra1 :::"integrable"::: ) ))) ; theorem :: INTEGRA4:21 (Bool "for" (Set (Var "C")) "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 "C")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k19_rfunct_3 :::"max-"::: ) (Set (Var "f"))) ($#r2_relset_1 :::"="::: ) (Set ($#k18_rfunct_3 :::"max+"::: ) (Set "(" ($#k32_valued_1 :::"-"::: ) (Set (Var "f")) ")" ))))) ; theorem :: INTEGRA4:22 (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 (Set ($#k19_rfunct_3 :::"max-"::: ) (Set (Var "f"))) "is" ($#v3_integra1 :::"integrable"::: ) ))) ; theorem :: INTEGRA4: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 "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 ($#k56_valued_1 :::"abs"::: ) (Set (Var "f"))) "is" ($#v3_integra1 :::"integrable"::: ) ) & (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set "(" ($#k12_integra1 :::"integral"::: ) (Set (Var "f")) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k12_integra1 :::"integral"::: ) (Set "(" ($#k56_valued_1 :::"abs"::: ) (Set (Var "f")) ")" ))) ")" ))) ; theorem :: INTEGRA4:24 (Bool "for" (Set (Var "a")) "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 "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set "(" (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "y")) ")" ) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "a"))) ")" )) "holds" (Bool (Set (Set "(" ($#k4_seq_4 :::"upper_bound"::: ) (Set "(" ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "f")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k5_seq_4 :::"lower_bound"::: ) (Set "(" ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "f")) ")" ) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "a")))))) ; theorem :: INTEGRA4:25 (Bool "for" (Set (Var "a")) "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")) "," (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 "a")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set "(" (Set (Var "g")) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "g")) ($#k1_seq_1 :::"."::: ) (Set (Var "y")) ")" ) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "a")) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_complex1 :::"abs"::: ) (Set "(" (Set "(" (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "y")) ")" ) ")" ) ")" ))) ")" )) "holds" (Bool (Set (Set "(" ($#k4_seq_4 :::"upper_bound"::: ) (Set "(" ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "g")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k5_seq_4 :::"lower_bound"::: ) (Set "(" ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "g")) ")" ) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "a")) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" ($#k4_seq_4 :::"upper_bound"::: ) (Set "(" ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "f")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k5_seq_4 :::"lower_bound"::: ) (Set "(" ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "f")) ")" ) ")" ) ")" )))))) ; theorem :: INTEGRA4:26 (Bool "for" (Set (Var "a")) "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")) "," (Set (Var "g")) "," (Set (Var "h")) "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 "a")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set "(" (Set (Var "h")) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "h")) ($#k1_seq_1 :::"."::: ) (Set (Var "y")) ")" ) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "a")) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" ($#k18_complex1 :::"abs"::: ) (Set "(" (Set "(" (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "y")) ")" ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k18_complex1 :::"abs"::: ) (Set "(" (Set "(" (Set (Var "g")) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "g")) ($#k1_seq_1 :::"."::: ) (Set (Var "y")) ")" ) ")" ) ")" ) ")" ))) ")" )) "holds" (Bool (Set (Set "(" ($#k4_seq_4 :::"upper_bound"::: ) (Set "(" ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "h")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k5_seq_4 :::"lower_bound"::: ) (Set "(" ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "h")) ")" ) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "a")) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" ($#k4_seq_4 :::"upper_bound"::: ) (Set "(" ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "f")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k5_seq_4 :::"lower_bound"::: ) (Set "(" ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "f")) ")" ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k4_seq_4 :::"upper_bound"::: ) (Set "(" ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "g")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k5_seq_4 :::"lower_bound"::: ) (Set "(" ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "g")) ")" ) ")" ) ")" ) ")" )))))) ; theorem :: INTEGRA4:27 (Bool "for" (Set (Var "a")) "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")) "," (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 "a")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set "(" (Set (Var "g")) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "g")) ($#k1_seq_1 :::"."::: ) (Set (Var "y")) ")" ) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "a")) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_complex1 :::"abs"::: ) (Set "(" (Set "(" (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "y")) ")" ) ")" ) ")" ))) ")" )) "holds" (Bool (Set (Var "g")) "is" ($#v3_integra1 :::"integrable"::: ) )))) ; theorem :: INTEGRA4:28 (Bool "for" (Set (Var "a")) "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")) "," (Set (Var "g")) "," (Set (Var "h")) "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 (Set (Set (Var "h")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A"))) "is" ($#v1_comseq_2 :::"bounded"::: ) ) & (Bool (Set (Var "a")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set "(" (Set (Var "h")) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "h")) ($#k1_seq_1 :::"."::: ) (Set (Var "y")) ")" ) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "a")) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" ($#k18_complex1 :::"abs"::: ) (Set "(" (Set "(" (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "y")) ")" ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k18_complex1 :::"abs"::: ) (Set "(" (Set "(" (Set (Var "g")) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "g")) ($#k1_seq_1 :::"."::: ) (Set (Var "y")) ")" ) ")" ) ")" ) ")" ))) ")" )) "holds" (Bool (Set (Var "h")) "is" ($#v3_integra1 :::"integrable"::: ) )))) ; theorem :: INTEGRA4: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 "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 (Set (Set (Var "f")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "g"))) "is" ($#v3_integra1 :::"integrable"::: ) ))) ; theorem :: INTEGRA4: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 "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"::: ) ) & (Bool (Bool "not" (Set ($#k6_numbers :::"0"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_rvsum_1 :::"rng"::: ) (Set (Var "f"))))) & (Bool (Set (Set "(" (Set (Var "f")) ($#k6_rfunct_1 :::"^"::: ) ")" ) ($#k2_partfun1 :::"|"::: ) (Set (Var "A"))) "is" ($#v1_comseq_2 :::"bounded"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k6_rfunct_1 :::"^"::: ) ) "is" ($#v3_integra1 :::"integrable"::: ) ))) ;