:: MESFUNC9 semantic presentation begin theorem :: MESFUNC9:1 (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 ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) "is" bbbadV4_MESFUNC5()) & (Bool (Set (Var "g")) "is" bbbadV4_MESFUNC5())) "holds" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k3_mesfunc1 :::"+"::: ) (Set (Var "g")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "g")) ")" ))))) ; theorem :: MESFUNC9:2 (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 ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) "is" bbbadV4_MESFUNC5()) & (Bool (Set (Var "g")) "is" bbbadV3_MESFUNC5())) "holds" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k4_mesfunc1 :::"-"::: ) (Set (Var "g")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "g")) ")" ))))) ; theorem :: MESFUNC9:3 (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 ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) "is" bbbadV3_MESFUNC5()) & (Bool (Set (Var "g")) "is" bbbadV3_MESFUNC5())) "holds" (Bool (Set (Set (Var "f")) ($#k3_mesfunc1 :::"+"::: ) (Set (Var "g"))) "is" bbbadV3_MESFUNC5()))) ; theorem :: MESFUNC9:4 (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 ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) "is" bbbadV4_MESFUNC5()) & (Bool (Set (Var "g")) "is" bbbadV4_MESFUNC5())) "holds" (Bool (Set (Set (Var "f")) ($#k3_mesfunc1 :::"+"::: ) (Set (Var "g"))) "is" bbbadV4_MESFUNC5()))) ; theorem :: MESFUNC9:5 (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 ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) "is" bbbadV3_MESFUNC5()) & (Bool (Set (Var "g")) "is" bbbadV4_MESFUNC5())) "holds" (Bool (Set (Set (Var "f")) ($#k4_mesfunc1 :::"-"::: ) (Set (Var "g"))) "is" bbbadV3_MESFUNC5()))) ; theorem :: MESFUNC9:6 (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 ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) "is" bbbadV4_MESFUNC5()) & (Bool (Set (Var "g")) "is" bbbadV3_MESFUNC5())) "holds" (Bool (Set (Set (Var "f")) ($#k4_mesfunc1 :::"-"::: ) (Set (Var "g"))) "is" bbbadV4_MESFUNC5()))) ; theorem :: MESFUNC9:7 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "seq")) "is" ($#v7_mesfunc5 :::"convergent_to_finite_number"::: ) )) "implies" (Bool "ex" (Set (Var "g")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool "(" (Bool (Set ($#k2_mesfunc5 :::"lim"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set (Var "g"))) & (Bool "(" "for" (Set (Var "p")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "p")))) "holds" (Bool "ex" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m")))) "holds" (Bool (Set ($#k3_extreal1 :::"|."::: ) (Set "(" (Set "(" (Set (Var "seq")) ($#k12_supinf_2 :::"."::: ) (Set (Var "m")) ")" ) ($#k4_supinf_2 :::"-"::: ) (Set "(" ($#k2_mesfunc5 :::"lim"::: ) (Set (Var "seq")) ")" ) ")" ) ($#k3_extreal1 :::".|"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "p"))))) ")" ) ")" )) ")" & "(" (Bool (Bool (Set (Var "seq")) "is" ($#v8_mesfunc5 :::"convergent_to_+infty"::: ) )) "implies" (Bool (Set ($#k2_mesfunc5 :::"lim"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set ($#k1_supinf_1 :::"+infty"::: ) )) ")" & "(" (Bool (Bool (Set (Var "seq")) "is" ($#v9_mesfunc5 :::"convergent_to_-infty"::: ) )) "implies" (Bool (Set ($#k2_mesfunc5 :::"lim"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set ($#k2_supinf_1 :::"-infty"::: ) )) ")" ")" )) ; theorem :: MESFUNC9:8 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) "st" (Bool (Bool (Set (Var "seq")) "is" bbbadV6_SUPINF_2())) "holds" (Bool "not" (Bool (Set (Var "seq")) "is" ($#v9_mesfunc5 :::"convergent_to_-infty"::: ) ))) ; theorem :: MESFUNC9:9 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) (Bool "for" (Set (Var "p")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v10_mesfunc5 :::"convergent"::: ) ) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "seq")) ($#k12_supinf_2 :::"."::: ) (Set (Var "k"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "p"))) ")" )) "holds" (Bool (Set ($#k2_mesfunc5 :::"lim"::: ) (Set (Var "seq"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "p"))))) ; theorem :: MESFUNC9:10 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) (Bool "for" (Set (Var "p")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v10_mesfunc5 :::"convergent"::: ) ) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Var "p")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "seq")) ($#k12_supinf_2 :::"."::: ) (Set (Var "k")))) ")" )) "holds" (Bool (Set (Var "p")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k2_mesfunc5 :::"lim"::: ) (Set (Var "seq")))))) ; theorem :: MESFUNC9:11 (Bool "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "," (Set (Var "seq")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) "st" (Bool (Bool (Set (Var "seq1")) "is" ($#v10_mesfunc5 :::"convergent"::: ) ) & (Bool (Set (Var "seq2")) "is" ($#v10_mesfunc5 :::"convergent"::: ) ) & (Bool (Set (Var "seq1")) "is" bbbadV6_SUPINF_2()) & (Bool (Set (Var "seq2")) "is" bbbadV6_SUPINF_2()) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "seq")) ($#k12_supinf_2 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "seq1")) ($#k12_supinf_2 :::"."::: ) (Set (Var "k")) ")" ) ($#k3_supinf_2 :::"+"::: ) (Set "(" (Set (Var "seq2")) ($#k12_supinf_2 :::"."::: ) (Set (Var "k")) ")" ))) ")" )) "holds" (Bool "(" (Bool (Set (Var "seq")) "is" bbbadV6_SUPINF_2()) & (Bool (Set (Var "seq")) "is" ($#v10_mesfunc5 :::"convergent"::: ) ) & (Bool (Set ($#k2_mesfunc5 :::"lim"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_mesfunc5 :::"lim"::: ) (Set (Var "seq1")) ")" ) ($#k3_supinf_2 :::"+"::: ) (Set "(" ($#k2_mesfunc5 :::"lim"::: ) (Set (Var "seq2")) ")" ))) ")" )) ; theorem :: MESFUNC9:12 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "," (Set (Var "F")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "G")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n"))) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set (Var "D")))) ")" ) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "D")))) "holds" (Bool "(" "(" (Bool (Bool (Set (Set (Var "F")) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x"))) "is" ($#v8_mesfunc5 :::"convergent_to_+infty"::: ) )) "implies" (Bool (Set (Set (Var "G")) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x"))) "is" ($#v8_mesfunc5 :::"convergent_to_+infty"::: ) ) ")" & "(" (Bool (Bool (Set (Set (Var "F")) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x"))) "is" ($#v9_mesfunc5 :::"convergent_to_-infty"::: ) )) "implies" (Bool (Set (Set (Var "G")) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x"))) "is" ($#v9_mesfunc5 :::"convergent_to_-infty"::: ) ) ")" & "(" (Bool (Bool (Set (Set (Var "F")) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x"))) "is" ($#v7_mesfunc5 :::"convergent_to_finite_number"::: ) )) "implies" (Bool (Set (Set (Var "G")) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x"))) "is" ($#v7_mesfunc5 :::"convergent_to_finite_number"::: ) ) ")" & "(" (Bool (Bool (Set (Set (Var "F")) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x"))) "is" ($#v10_mesfunc5 :::"convergent"::: ) )) "implies" (Bool (Set (Set (Var "G")) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x"))) "is" ($#v10_mesfunc5 :::"convergent"::: ) ) ")" ")" ))))) ; theorem :: MESFUNC9:13 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "E")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool (Set (Var "E")) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "f")) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "E"))) & (Bool (Set (Var "f")) "is" ($#v6_supinf_2 :::"nonnegative"::: ) ) & (Bool (Set (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set "(" (Set (Var "E")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k19_mesfunc1 :::"eq_dom"::: ) "(" (Set (Var "f")) "," (Set ($#k1_supinf_1 :::"+infty"::: ) ) ")" ")" ) ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k7_mesfunc5 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_supinf_1 :::"+infty"::: ) ))))))) ; theorem :: MESFUNC9:14 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "E")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set ($#k7_mesfunc5 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" ($#k3_mesfunc2 :::"chi"::: ) "(" (Set (Var "E")) "," (Set (Var "X")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set (Var "E")))) & (Bool (Set ($#k7_mesfunc5 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" (Set "(" ($#k3_mesfunc2 :::"chi"::: ) "(" (Set (Var "E")) "," (Set (Var "X")) ")" ")" ) ($#k2_partfun1 :::"|"::: ) (Set (Var "E")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set (Var "E")))) ")" ))))) ; theorem :: MESFUNC9:15 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "E")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool (Set (Var "E")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "E")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "g")))) & (Bool (Set (Var "f")) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "E"))) & (Bool (Set (Var "g")) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "E"))) & (Bool (Set (Var "f")) "is" ($#v6_supinf_2 :::"nonnegative"::: ) ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "E")))) "holds" (Bool (Set (Set (Var "f")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "g")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x")))) ")" )) "holds" (Bool (Set ($#k7_mesfunc5 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "E")) ")" ) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k7_mesfunc5 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "g")) ($#k2_partfun1 :::"|"::: ) (Set (Var "E")) ")" ) ")" ))))))) ; begin definitionlet "f" be ($#v2_valued_0 :::"ext-real-valued"::: ) ($#m1_hidden :::"Function":::); let "x" be ($#m1_hidden :::"set"::: ) ; :: original: :::"."::: redefine func "f" :::"."::: "x" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ); end; definitionlet "s" be ($#v2_valued_0 :::"ext-real-valued"::: ) ($#m1_hidden :::"Function":::); func :::"Partial_Sums"::: "s" -> ($#m1_subset_1 :::"ExtREAL_sequence":::) means :: MESFUNC9:def 1 (Bool "(" (Bool (Set it ($#k1_mesfunc9 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set "s" ($#k1_mesfunc9 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set it ($#k1_mesfunc9 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" it ($#k1_mesfunc9 :::"."::: ) (Set (Var "n")) ")" ) ($#k3_supinf_2 :::"+"::: ) (Set "(" "s" ($#k1_mesfunc9 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"Partial_Sums"::: MESFUNC9:def 1 : (Bool "for" (Set (Var "s")) "being" ($#v2_valued_0 :::"ext-real-valued"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k2_mesfunc9 :::"Partial_Sums"::: ) (Set (Var "s")))) "iff" (Bool "(" (Bool (Set (Set (Var "b2")) ($#k1_mesfunc9 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_mesfunc9 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "b2")) ($#k1_mesfunc9 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "b2")) ($#k1_mesfunc9 :::"."::: ) (Set (Var "n")) ")" ) ($#k3_supinf_2 :::"+"::: ) (Set "(" (Set (Var "s")) ($#k1_mesfunc9 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ))) ")" ) ")" ) ")" ))); definitionlet "s" be ($#v2_valued_0 :::"ext-real-valued"::: ) ($#m1_hidden :::"Function":::); attr "s" is :::"summable"::: means :: MESFUNC9:def 2 (Bool (Set ($#k2_mesfunc9 :::"Partial_Sums"::: ) "s") "is" ($#v10_mesfunc5 :::"convergent"::: ) ); end; :: deftheorem defines :::"summable"::: MESFUNC9:def 2 : (Bool "for" (Set (Var "s")) "being" ($#v2_valued_0 :::"ext-real-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "s")) "is" ($#v1_mesfunc9 :::"summable"::: ) ) "iff" (Bool (Set ($#k2_mesfunc9 :::"Partial_Sums"::: ) (Set (Var "s"))) "is" ($#v10_mesfunc5 :::"convergent"::: ) ) ")" )); definitionlet "s" be ($#v2_valued_0 :::"ext-real-valued"::: ) ($#m1_hidden :::"Function":::); func :::"Sum"::: "s" -> ($#m1_subset_1 :::"R_eal":::) equals :: MESFUNC9:def 3 (Set ($#k2_mesfunc5 :::"lim"::: ) (Set "(" ($#k2_mesfunc9 :::"Partial_Sums"::: ) "s" ")" )); end; :: deftheorem defines :::"Sum"::: MESFUNC9:def 3 : (Bool "for" (Set (Var "s")) "being" ($#v2_valued_0 :::"ext-real-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k3_mesfunc9 :::"Sum"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k2_mesfunc5 :::"lim"::: ) (Set "(" ($#k2_mesfunc9 :::"Partial_Sums"::: ) (Set (Var "s")) ")" )))); theorem :: MESFUNC9:16 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) "st" (Bool (Bool (Set (Var "seq")) "is" bbbadV6_SUPINF_2())) "holds" (Bool "(" (Bool (Set ($#k2_mesfunc9 :::"Partial_Sums"::: ) (Set (Var "seq"))) "is" bbbadV6_SUPINF_2()) & (Bool (Set ($#k2_mesfunc9 :::"Partial_Sums"::: ) (Set (Var "seq"))) "is" ($#v7_valued_0 :::"non-decreasing"::: ) ) ")" )) ; theorem :: MESFUNC9:17 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "seq")) ($#k1_mesfunc9 :::"."::: ) (Set (Var "n")))) ")" )) "holds" (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Set "(" ($#k2_mesfunc9 :::"Partial_Sums"::: ) (Set (Var "seq")) ")" ) ($#k1_mesfunc9 :::"."::: ) (Set (Var "m")))))) ; theorem :: MESFUNC9:18 (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 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "G")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n"))) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set (Var "D")))) ")" )) "holds" (Bool (Set (Var "G")) "is" ($#v1_mesfunc8 :::"with_the_same_dom"::: ) )))) ; theorem :: MESFUNC9:19 (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 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "D")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "G")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n"))) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set (Var "D")))) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "D")))) "holds" (Bool (Set (Set (Var "F")) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x"))) "is" ($#v10_mesfunc5 :::"convergent"::: ) ) ")" )) "holds" (Bool (Set (Set "(" ($#k7_mesfunc8 :::"lim"::: ) (Set (Var "F")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set (Var "D"))) ($#r2_relset_1 :::"="::: ) (Set ($#k7_mesfunc8 :::"lim"::: ) (Set (Var "G"))))))) ; theorem :: MESFUNC9:20 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "E")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ) & (Bool (Set (Var "E")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ))) & (Bool "(" "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "m"))) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "E"))) & (Bool (Set (Set (Var "G")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "m"))) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "m")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set (Var "E")))) ")" ) ")" )) "holds" (Bool (Set (Set (Var "G")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n"))) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "E")))))))) ; theorem :: MESFUNC9:21 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "E")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool (Set (Var "E")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ))) & (Bool (Set (Var "G")) "is" ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "E")))) "holds" (Bool (Set (Set (Var "F")) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x"))) "is" ($#v1_mesfunc9 :::"summable"::: ) ) ")" ) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "G")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n"))) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set (Var "E")))) ")" )) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "E")))) "holds" (Bool (Set (Set (Var "G")) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x"))) "is" ($#v1_mesfunc9 :::"summable"::: ) )))))) ; begin definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Const "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ); func :::"Partial_Sums"::: "F" -> ($#m1_subset_1 :::"Functional_Sequence":::) "of" "X" "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) means :: MESFUNC9:def 4 (Bool "(" (Bool (Set it ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r2_relset_1 :::"="::: ) (Set "F" ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set it ($#k4_mesfunc5 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set "(" it ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ($#k3_mesfunc1 :::"+"::: ) (Set "(" "F" ($#k4_mesfunc5 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"Partial_Sums"::: MESFUNC9:def 4 : (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "b3")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k4_mesfunc9 :::"Partial_Sums"::: ) (Set (Var "F")))) "iff" (Bool "(" (Bool (Set (Set (Var "b3")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "b3")) ($#k4_mesfunc5 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "b3")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ($#k3_mesfunc1 :::"+"::: ) (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ))) ")" ) ")" ) ")" ))); definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Const "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ); attr "F" is :::"additive"::: means :: MESFUNC9:def 5 (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_hidden :::"<>"::: ) (Set (Var "m")))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "not" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set "(" "F" ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set "(" "F" ($#k4_mesfunc5 :::"."::: ) (Set (Var "m")) ")" ) ")" ))) "or" (Bool (Set (Set "(" "F" ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ($#k1_mesfunc9 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_supinf_1 :::"+infty"::: ) )) "or" (Bool (Set (Set "(" "F" ($#k4_mesfunc5 :::"."::: ) (Set (Var "m")) ")" ) ($#k1_mesfunc9 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"<>"::: ) (Set ($#k2_supinf_1 :::"-infty"::: ) )) ")" ))); end; :: deftheorem defines :::"additive"::: MESFUNC9:def 5 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v2_mesfunc9 :::"additive"::: ) ) "iff" (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_hidden :::"<>"::: ) (Set (Var "m")))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "not" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "m")) ")" ) ")" ))) "or" (Bool (Set (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ($#k1_mesfunc9 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_supinf_1 :::"+infty"::: ) )) "or" (Bool (Set (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "m")) ")" ) ($#k1_mesfunc9 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"<>"::: ) (Set ($#k2_supinf_1 :::"-infty"::: ) )) ")" ))) ")" ))); theorem :: MESFUNC9:22 (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 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" ($#k4_mesfunc9 :::"Partial_Sums"::: ) (Set (Var "F")) ")" ) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ))) & (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool "(" (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" ($#k4_mesfunc9 :::"Partial_Sums"::: ) (Set (Var "F")) ")" ) ($#k4_mesfunc5 :::"."::: ) (Set (Var "m")) ")" ))) & (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "m")) ")" ))) ")" ))))) ; theorem :: MESFUNC9:23 (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 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" ($#k4_mesfunc9 :::"Partial_Sums"::: ) (Set (Var "F")) ")" ) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ))) & (Bool (Set (Set "(" (Set "(" ($#k4_mesfunc9 :::"Partial_Sums"::: ) (Set (Var "F")) ")" ) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ($#k1_mesfunc9 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k1_supinf_1 :::"+infty"::: ) ))) "holds" (Bool "ex" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "(" (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "m")) ")" ) ($#k1_mesfunc9 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k1_supinf_1 :::"+infty"::: ) )) ")" )))))) ; theorem :: MESFUNC9:24 (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 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "F")) "is" ($#v2_mesfunc9 :::"additive"::: ) ) & (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" ($#k4_mesfunc9 :::"Partial_Sums"::: ) (Set (Var "F")) ")" ) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ))) & (Bool (Set (Set "(" (Set "(" ($#k4_mesfunc9 :::"Partial_Sums"::: ) (Set (Var "F")) ")" ) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ($#k1_mesfunc9 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k1_supinf_1 :::"+infty"::: ) )) & (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "m")) ")" ) ($#k1_mesfunc9 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"<>"::: ) (Set ($#k2_supinf_1 :::"-infty"::: ) )))))) ; theorem :: MESFUNC9:25 (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 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" ($#k4_mesfunc9 :::"Partial_Sums"::: ) (Set (Var "F")) ")" ) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ))) & (Bool (Set (Set "(" (Set "(" ($#k4_mesfunc9 :::"Partial_Sums"::: ) (Set (Var "F")) ")" ) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ($#k1_mesfunc9 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k2_supinf_1 :::"-infty"::: ) ))) "holds" (Bool "ex" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "(" (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "m")) ")" ) ($#k1_mesfunc9 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k2_supinf_1 :::"-infty"::: ) )) ")" )))))) ; theorem :: MESFUNC9:26 (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 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "F")) "is" ($#v2_mesfunc9 :::"additive"::: ) ) & (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" ($#k4_mesfunc9 :::"Partial_Sums"::: ) (Set (Var "F")) ")" ) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ))) & (Bool (Set (Set "(" (Set "(" ($#k4_mesfunc9 :::"Partial_Sums"::: ) (Set (Var "F")) ")" ) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ($#k1_mesfunc9 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k2_supinf_1 :::"-infty"::: ) )) & (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "m")) ")" ) ($#k1_mesfunc9 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_supinf_1 :::"+infty"::: ) )))))) ; theorem :: MESFUNC9:27 (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 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "F")) "is" ($#v2_mesfunc9 :::"additive"::: ) )) "holds" (Bool "(" (Bool (Set (Set "(" (Set "(" (Set "(" ($#k4_mesfunc9 :::"Partial_Sums"::: ) (Set (Var "F")) ")" ) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ($#k8_relset_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k2_supinf_1 :::"-infty"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k8_relset_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_supinf_1 :::"+infty"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Set "(" (Set "(" (Set "(" ($#k4_mesfunc9 :::"Partial_Sums"::: ) (Set (Var "F")) ")" ) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ($#k8_relset_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_supinf_1 :::"+infty"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k8_relset_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k2_supinf_1 :::"-infty"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" )))) ; theorem :: MESFUNC9:28 (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 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "F")) "is" ($#v2_mesfunc9 :::"additive"::: ) )) "holds" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" ($#k4_mesfunc9 :::"Partial_Sums"::: ) (Set (Var "F")) ")" ) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_setfam_1 :::"meet"::: ) "{" (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "k")) ")" ) ")" ) where k "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) "}" ))))) ; theorem :: MESFUNC9:29 (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 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "F")) "is" ($#v2_mesfunc9 :::"additive"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_mesfunc8 :::"with_the_same_dom"::: ) )) "holds" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" ($#k4_mesfunc9 :::"Partial_Sums"::: ) (Set (Var "F")) ")" ) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )))))) ; theorem :: MESFUNC9:30 (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 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n"))) "is" ($#v6_supinf_2 :::"nonnegative"::: ) ) ")" )) "holds" (Bool (Set (Var "F")) "is" ($#v2_mesfunc9 :::"additive"::: ) ))) ; theorem :: MESFUNC9:31 (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 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "F")) "is" ($#v2_mesfunc9 :::"additive"::: ) ) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "G")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n"))) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set (Var "D")))) ")" )) "holds" (Bool (Set (Var "G")) "is" ($#v2_mesfunc9 :::"additive"::: ) )))) ; theorem :: MESFUNC9:32 (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 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "F")) "is" ($#v2_mesfunc9 :::"additive"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ) & (Bool (Set (Var "D")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "D")))) "holds" (Bool (Set (Set "(" ($#k2_mesfunc9 :::"Partial_Sums"::: ) (Set "(" (Set (Var "F")) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x")) ")" ) ")" ) ($#k1_mesfunc9 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k4_mesfunc9 :::"Partial_Sums"::: ) (Set (Var "F")) ")" ) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x")) ")" ) ($#k1_mesfunc9 :::"."::: ) (Set (Var "n"))))))))) ; theorem :: MESFUNC9:33 (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 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "F")) "is" ($#v2_mesfunc9 :::"additive"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ) & (Bool (Set (Var "D")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "D")))) "holds" (Bool "(" "(" (Bool (Bool (Set ($#k2_mesfunc9 :::"Partial_Sums"::: ) (Set "(" (Set (Var "F")) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x")) ")" )) "is" ($#v7_mesfunc5 :::"convergent_to_finite_number"::: ) )) "implies" (Bool (Set (Set "(" ($#k4_mesfunc9 :::"Partial_Sums"::: ) (Set (Var "F")) ")" ) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x"))) "is" ($#v7_mesfunc5 :::"convergent_to_finite_number"::: ) ) ")" & "(" (Bool (Bool (Set (Set "(" ($#k4_mesfunc9 :::"Partial_Sums"::: ) (Set (Var "F")) ")" ) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x"))) "is" ($#v7_mesfunc5 :::"convergent_to_finite_number"::: ) )) "implies" (Bool (Set ($#k2_mesfunc9 :::"Partial_Sums"::: ) (Set "(" (Set (Var "F")) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x")) ")" )) "is" ($#v7_mesfunc5 :::"convergent_to_finite_number"::: ) ) ")" & "(" (Bool (Bool (Set ($#k2_mesfunc9 :::"Partial_Sums"::: ) (Set "(" (Set (Var "F")) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x")) ")" )) "is" ($#v8_mesfunc5 :::"convergent_to_+infty"::: ) )) "implies" (Bool (Set (Set "(" ($#k4_mesfunc9 :::"Partial_Sums"::: ) (Set (Var "F")) ")" ) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x"))) "is" ($#v8_mesfunc5 :::"convergent_to_+infty"::: ) ) ")" & "(" (Bool (Bool (Set (Set "(" ($#k4_mesfunc9 :::"Partial_Sums"::: ) (Set (Var "F")) ")" ) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x"))) "is" ($#v8_mesfunc5 :::"convergent_to_+infty"::: ) )) "implies" (Bool (Set ($#k2_mesfunc9 :::"Partial_Sums"::: ) (Set "(" (Set (Var "F")) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x")) ")" )) "is" ($#v8_mesfunc5 :::"convergent_to_+infty"::: ) ) ")" & "(" (Bool (Bool (Set ($#k2_mesfunc9 :::"Partial_Sums"::: ) (Set "(" (Set (Var "F")) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x")) ")" )) "is" ($#v9_mesfunc5 :::"convergent_to_-infty"::: ) )) "implies" (Bool (Set (Set "(" ($#k4_mesfunc9 :::"Partial_Sums"::: ) (Set (Var "F")) ")" ) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x"))) "is" ($#v9_mesfunc5 :::"convergent_to_-infty"::: ) ) ")" & "(" (Bool (Bool (Set (Set "(" ($#k4_mesfunc9 :::"Partial_Sums"::: ) (Set (Var "F")) ")" ) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x"))) "is" ($#v9_mesfunc5 :::"convergent_to_-infty"::: ) )) "implies" (Bool (Set ($#k2_mesfunc9 :::"Partial_Sums"::: ) (Set "(" (Set (Var "F")) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x")) ")" )) "is" ($#v9_mesfunc5 :::"convergent_to_-infty"::: ) ) ")" & "(" (Bool (Bool (Set ($#k2_mesfunc9 :::"Partial_Sums"::: ) (Set "(" (Set (Var "F")) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x")) ")" )) "is" ($#v10_mesfunc5 :::"convergent"::: ) )) "implies" (Bool (Set (Set "(" ($#k4_mesfunc9 :::"Partial_Sums"::: ) (Set (Var "F")) ")" ) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x"))) "is" ($#v10_mesfunc5 :::"convergent"::: ) ) ")" & "(" (Bool (Bool (Set (Set "(" ($#k4_mesfunc9 :::"Partial_Sums"::: ) (Set (Var "F")) ")" ) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x"))) "is" ($#v10_mesfunc5 :::"convergent"::: ) )) "implies" (Bool (Set ($#k2_mesfunc9 :::"Partial_Sums"::: ) (Set "(" (Set (Var "F")) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x")) ")" )) "is" ($#v10_mesfunc5 :::"convergent"::: ) ) ")" ")" ))))) ; theorem :: MESFUNC9:34 (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 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v2_mesfunc9 :::"additive"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ) & (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Set (Var "F")) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x"))) "is" ($#v1_mesfunc9 :::"summable"::: ) ) & (Bool (Set (Set (Var "f")) ($#k1_mesfunc9 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k3_mesfunc9 :::"Sum"::: ) (Set "(" (Set (Var "F")) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x")) ")" )))) "holds" (Bool (Set (Set (Var "f")) ($#k1_mesfunc9 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k2_mesfunc5 :::"lim"::: ) (Set "(" (Set "(" ($#k4_mesfunc9 :::"Partial_Sums"::: ) (Set (Var "F")) ")" ) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x")) ")" ))))))) ; theorem :: MESFUNC9:35 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool "(" "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "m"))) ($#r1_mesfunc2 :::"is_simple_func_in"::: ) (Set (Var "S"))) ")" )) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v2_mesfunc9 :::"additive"::: ) ) & (Bool (Set (Set "(" ($#k4_mesfunc9 :::"Partial_Sums"::: ) (Set (Var "F")) ")" ) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n"))) ($#r1_mesfunc2 :::"is_simple_func_in"::: ) (Set (Var "S"))) ")" ))))) ; theorem :: MESFUNC9:36 (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 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool "(" "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "m"))) "is" ($#v6_supinf_2 :::"nonnegative"::: ) ) ")" )) "holds" (Bool (Set (Set "(" ($#k4_mesfunc9 :::"Partial_Sums"::: ) (Set (Var "F")) ")" ) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n"))) "is" ($#v6_supinf_2 :::"nonnegative"::: ) )))) ; theorem :: MESFUNC9:37 (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 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "k"))) "is" ($#v6_supinf_2 :::"nonnegative"::: ) ) ")" ) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m")))) "holds" (Bool (Set (Set "(" (Set "(" ($#k4_mesfunc9 :::"Partial_Sums"::: ) (Set (Var "F")) ")" ) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ($#k1_mesfunc9 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set "(" ($#k4_mesfunc9 :::"Partial_Sums"::: ) (Set (Var "F")) ")" ) ($#k4_mesfunc5 :::"."::: ) (Set (Var "m")) ")" ) ($#k1_mesfunc9 :::"."::: ) (Set (Var "x")))))))) ; theorem :: MESFUNC9:38 (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 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ))) & (Bool "(" "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "m"))) "is" ($#v6_supinf_2 :::"nonnegative"::: ) ) ")" )) "holds" (Bool "(" (Bool (Set (Set "(" ($#k4_mesfunc9 :::"Partial_Sums"::: ) (Set (Var "F")) ")" ) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x"))) "is" ($#v7_valued_0 :::"non-decreasing"::: ) ) & (Bool (Set (Set "(" ($#k4_mesfunc9 :::"Partial_Sums"::: ) (Set (Var "F")) ")" ) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x"))) "is" ($#v10_mesfunc5 :::"convergent"::: ) ) ")" )))) ; theorem :: MESFUNC9:39 (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 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool "(" "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "m"))) "is" bbbadV3_MESFUNC5()) ")" )) "holds" (Bool (Set (Set "(" ($#k4_mesfunc9 :::"Partial_Sums"::: ) (Set (Var "F")) ")" ) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n"))) "is" bbbadV3_MESFUNC5())))) ; theorem :: MESFUNC9:40 (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 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool "(" "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "m"))) "is" bbbadV4_MESFUNC5()) ")" )) "holds" (Bool (Set (Set "(" ($#k4_mesfunc9 :::"Partial_Sums"::: ) (Set (Var "F")) ")" ) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n"))) "is" bbbadV4_MESFUNC5())))) ; theorem :: MESFUNC9:41 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "E")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n"))) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "E"))) & (Bool (Set (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n"))) "is" bbbadV3_MESFUNC5()) ")" ) ")" )) "holds" (Bool (Set (Set "(" ($#k4_mesfunc9 :::"Partial_Sums"::: ) (Set (Var "F")) ")" ) ($#k4_mesfunc5 :::"."::: ) (Set (Var "m"))) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "E")))))))) ; theorem :: MESFUNC9:42 (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 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v2_mesfunc9 :::"additive"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ) & (Bool (Set (Var "G")) "is" ($#v2_mesfunc9 :::"additive"::: ) ) & (Bool (Set (Var "G")) "is" ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "G")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "G")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" )))) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "k")) ")" ) ($#k1_mesfunc9 :::"."::: ) (Set (Var "y"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set (Var "G")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "k")) ")" ) ($#k1_mesfunc9 :::"."::: ) (Set (Var "y"))))) ")" )) "holds" (Bool (Set (Set "(" (Set "(" ($#k4_mesfunc9 :::"Partial_Sums"::: ) (Set (Var "F")) ")" ) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ($#k1_mesfunc9 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set "(" ($#k4_mesfunc9 :::"Partial_Sums"::: ) (Set (Var "G")) ")" ) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ($#k1_mesfunc9 :::"."::: ) (Set (Var "x")))))))) ; theorem :: MESFUNC9:43 (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 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool (Set (Var "F")) "is" ($#v2_mesfunc9 :::"additive"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_mesfunc8 :::"with_the_same_dom"::: ) )) "holds" (Bool (Set ($#k4_mesfunc9 :::"Partial_Sums"::: ) (Set (Var "F"))) "is" ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ))) ; theorem :: MESFUNC9:44 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "E")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "E"))) & (Bool (Set (Var "F")) "is" ($#v2_mesfunc9 :::"additive"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" ($#k4_mesfunc9 :::"Partial_Sums"::: ) (Set (Var "F")) ")" ) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n"))) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "E"))) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "E")))) "holds" (Bool (Set (Set (Var "F")) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x"))) "is" ($#v1_mesfunc9 :::"summable"::: ) ) ")" )) "holds" (Bool (Set ($#k7_mesfunc8 :::"lim"::: ) (Set "(" ($#k4_mesfunc9 :::"Partial_Sums"::: ) (Set (Var "F")) ")" )) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "E"))))))) ; theorem :: MESFUNC9:45 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n"))) ($#r1_mesfunc5 :::"is_integrable_on"::: ) (Set (Var "M"))) ")" )) "holds" (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" ($#k4_mesfunc9 :::"Partial_Sums"::: ) (Set (Var "F")) ")" ) ($#k4_mesfunc5 :::"."::: ) (Set (Var "m"))) ($#r1_mesfunc5 :::"is_integrable_on"::: ) (Set (Var "M")))))))) ; theorem :: MESFUNC9:46 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "E")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "E")) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ))) & (Bool (Set (Var "F")) "is" ($#v2_mesfunc9 :::"additive"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n"))) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "E"))) & (Bool (Set (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n"))) "is" ($#v6_supinf_2 :::"nonnegative"::: ) ) & (Bool (Set (Set (Var "I")) ($#k1_mesfunc9 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k7_mesfunc5 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ")" )) ")" ) ")" )) "holds" (Bool (Set ($#k7_mesfunc5 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" (Set "(" ($#k4_mesfunc9 :::"Partial_Sums"::: ) (Set (Var "F")) ")" ) ($#k4_mesfunc5 :::"."::: ) (Set (Var "m")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_mesfunc9 :::"Partial_Sums"::: ) (Set (Var "I")) ")" ) ($#k1_mesfunc9 :::"."::: ) (Set (Var "m"))))))))))) ; begin theorem :: MESFUNC9:47 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "E")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool (Set (Var "E")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "f")) "is" ($#v6_supinf_2 :::"nonnegative"::: ) ) & (Bool (Set (Var "f")) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "E"))) & (Bool (Set (Var "F")) "is" ($#v2_mesfunc9 :::"additive"::: ) ) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n"))) ($#r1_mesfunc2 :::"is_simple_func_in"::: ) (Set (Var "S"))) & (Bool (Set (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n"))) "is" ($#v6_supinf_2 :::"nonnegative"::: ) ) & (Bool (Set (Var "E")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ))) ")" ) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "E")))) "holds" (Bool "(" (Bool (Set (Set (Var "F")) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x"))) "is" ($#v1_mesfunc9 :::"summable"::: ) ) & (Bool (Set (Set (Var "f")) ($#k1_mesfunc9 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k3_mesfunc9 :::"Sum"::: ) (Set "(" (Set (Var "F")) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x")) ")" ))) ")" ) ")" )) "holds" (Bool "ex" (Set (Var "I")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) "st" (Bool "(" (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "I")) ($#k1_mesfunc9 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k7_mesfunc5 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set (Var "E")) ")" ) ")" )) ")" ) & (Bool (Set (Var "I")) "is" ($#v1_mesfunc9 :::"summable"::: ) ) & (Bool (Set ($#k7_mesfunc5 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "E")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_mesfunc9 :::"Sum"::: ) (Set (Var "I")))) ")" )))))))) ; theorem :: MESFUNC9:48 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "E")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool (Set (Var "E")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "f")) "is" ($#v6_supinf_2 :::"nonnegative"::: ) ) & (Bool (Set (Var "f")) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "E")))) "holds" (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool "(" (Bool (Set (Var "g")) "is" ($#v2_mesfunc9 :::"additive"::: ) ) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set (Set (Var "g")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n"))) ($#r1_mesfunc2 :::"is_simple_func_in"::: ) (Set (Var "S"))) & (Bool (Set (Set (Var "g")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n"))) "is" ($#v6_supinf_2 :::"nonnegative"::: ) ) & (Bool (Set (Set (Var "g")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n"))) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "E"))) ")" ) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "E")))) "holds" (Bool "(" (Bool (Set (Set (Var "g")) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x"))) "is" ($#v1_mesfunc9 :::"summable"::: ) ) & (Bool (Set (Set (Var "f")) ($#k1_mesfunc9 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k3_mesfunc9 :::"Sum"::: ) (Set "(" (Set (Var "g")) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x")) ")" ))) ")" ) ")" ) & (Bool "ex" (Set (Var "I")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) "st" (Bool "(" (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "I")) ($#k1_mesfunc9 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k7_mesfunc5 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" (Set "(" (Set (Var "g")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set (Var "E")) ")" ) ")" )) ")" ) & (Bool (Set (Var "I")) "is" ($#v1_mesfunc9 :::"summable"::: ) ) & (Bool (Set ($#k7_mesfunc5 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "E")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_mesfunc9 :::"Sum"::: ) (Set (Var "I")))) ")" )) ")" ))))))) ; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set ($#k4_partfun1 :::"PFuncs"::: ) "(" "X" "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) ")" ) ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_partfun1 :::"total"::: ) ($#v1_funct_2 :::"quasi_total"::: ) ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ($#v2_mesfunc9 :::"additive"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k4_partfun1 :::"PFuncs"::: ) "(" "X" "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) ")" ")" ) ($#k2_zfmisc_1 :::":]"::: ) )); end; definitionlet "C", "D", "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Const "C")) "," (Set (Const "D")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "(" ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set (Const "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) ")" ")" ); let "c" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "C")); let "d" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "D")); :: original: :::"."::: redefine func "F" :::"."::: "(" "c" "," "d" ")" -> ($#m1_subset_1 :::"PartFunc":::) "of" "X" "," (Set ($#k7_numbers :::"ExtREAL"::: ) ); end; definitionlet "C", "D", "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Const "C")) "," (Set (Const "D")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Const "X")); let "c" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "C")); func :::"ProjMap1"::: "(" "F" "," "c" ")" -> ($#m1_subset_1 :::"Function":::) "of" "D" "," "X" means :: MESFUNC9:def 6 (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "D" "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "d"))) ($#r1_hidden :::"="::: ) (Set "F" ($#k2_binop_1 :::"."::: ) "(" "c" "," (Set (Var "d")) ")" ))); end; :: deftheorem defines :::"ProjMap1"::: MESFUNC9:def 6 : (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "," (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 ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "C")) "," (Set (Var "D")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "X")) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C")) (Bool "for" (Set (Var "b6")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "D")) "," (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b6")) ($#r1_hidden :::"="::: ) (Set ($#k6_mesfunc9 :::"ProjMap1"::: ) "(" (Set (Var "F")) "," (Set (Var "c")) ")" )) "iff" (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "holds" (Bool (Set (Set (Var "b6")) ($#k3_funct_2 :::"."::: ) (Set (Var "d"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "c")) "," (Set (Var "d")) ")" ))) ")" ))))); definitionlet "C", "D", "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Const "C")) "," (Set (Const "D")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Const "X")); let "d" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "D")); func :::"ProjMap2"::: "(" "F" "," "d" ")" -> ($#m1_subset_1 :::"Function":::) "of" "C" "," "X" means :: MESFUNC9:def 7 (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "C" "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set "F" ($#k2_binop_1 :::"."::: ) "(" (Set (Var "c")) "," "d" ")" ))); end; :: deftheorem defines :::"ProjMap2"::: MESFUNC9:def 7 : (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "," (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 ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "C")) "," (Set (Var "D")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "X")) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "b6")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C")) "," (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b6")) ($#r1_hidden :::"="::: ) (Set ($#k7_mesfunc9 :::"ProjMap2"::: ) "(" (Set (Var "F")) "," (Set (Var "d")) ")" )) "iff" (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C")) "holds" (Bool (Set (Set (Var "b6")) ($#k3_funct_2 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "c")) "," (Set (Var "d")) ")" ))) ")" ))))); definitionlet "X", "Y" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k5_numbers :::"NAT"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "(" ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set (Const "X")) "," (Set (Const "Y")) ")" ")" ); let "n" be ($#m1_hidden :::"Nat":::); func :::"ProjMap1"::: "(" "F" "," "n" ")" -> ($#m1_subset_1 :::"Functional_Sequence":::) "of" "X" "," "Y" means :: MESFUNC9:def 8 (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set it ($#k4_mesfunc5 :::"."::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set "F" ($#k1_binop_1 :::"."::: ) "(" "n" "," (Set (Var "m")) ")" ))); func :::"ProjMap2"::: "(" "F" "," "n" ")" -> ($#m1_subset_1 :::"Functional_Sequence":::) "of" "X" "," "Y" means :: MESFUNC9:def 9 (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set it ($#k4_mesfunc5 :::"."::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set "F" ($#k1_binop_1 :::"."::: ) "(" (Set (Var "m")) "," "n" ")" ))); end; :: deftheorem defines :::"ProjMap1"::: MESFUNC9:def 8 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k5_numbers :::"NAT"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "(" ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ")" ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k8_mesfunc9 :::"ProjMap1"::: ) "(" (Set (Var "F")) "," (Set (Var "n")) ")" )) "iff" (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "b5")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "n")) "," (Set (Var "m")) ")" ))) ")" ))))); :: deftheorem defines :::"ProjMap2"::: MESFUNC9:def 9 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k5_numbers :::"NAT"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "(" ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ")" ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k9_mesfunc9 :::"ProjMap2"::: ) "(" (Set (Var "F")) "," (Set (Var "n")) ")" )) "iff" (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "b5")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "m")) "," (Set (Var "n")) ")" ))) ")" ))))); definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set (Const "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) ")" ")" ) ")" ")" ); let "n" be ($#m1_hidden :::"Nat":::); :: original: :::"."::: redefine func "F" :::"."::: "n" -> ($#m1_subset_1 :::"Functional_Sequence":::) "of" "X" "," (Set ($#k7_numbers :::"ExtREAL"::: ) ); end; theorem :: MESFUNC9:49 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "E")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool (Set (Var "E")) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ))) & (Bool (Set (Var "F")) "is" ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n"))) "is" ($#v6_supinf_2 :::"nonnegative"::: ) ) & (Bool (Set (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n"))) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "E"))) ")" ) ")" )) "holds" (Bool "ex" (Set (Var "FF")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) ")" ")" ) ")" ")" ) "st" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool "(" "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "FF")) ($#k10_mesfunc9 :::"."::: ) (Set (Var "n")) ")" ) ($#k4_mesfunc5 :::"."::: ) (Set (Var "m"))) ($#r1_mesfunc2 :::"is_simple_func_in"::: ) (Set (Var "S"))) & (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" (Set (Var "FF")) ($#k10_mesfunc9 :::"."::: ) (Set (Var "n")) ")" ) ($#k4_mesfunc5 :::"."::: ) (Set (Var "m")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ))) ")" ) ")" ) & (Bool "(" "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" (Set (Var "FF")) ($#k10_mesfunc9 :::"."::: ) (Set (Var "n")) ")" ) ($#k4_mesfunc5 :::"."::: ) (Set (Var "m"))) "is" ($#v6_supinf_2 :::"nonnegative"::: ) ) ")" ) & (Bool "(" "for" (Set (Var "j")) "," (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k")))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" )))) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "FF")) ($#k10_mesfunc9 :::"."::: ) (Set (Var "n")) ")" ) ($#k4_mesfunc5 :::"."::: ) (Set (Var "j")) ")" ) ($#k1_mesfunc9 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set "(" (Set (Var "FF")) ($#k10_mesfunc9 :::"."::: ) (Set (Var "n")) ")" ) ($#k4_mesfunc5 :::"."::: ) (Set (Var "k")) ")" ) ($#k1_mesfunc9 :::"."::: ) (Set (Var "x"))))) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" )))) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "FF")) ($#k10_mesfunc9 :::"."::: ) (Set (Var "n")) ")" ) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x"))) "is" ($#v10_mesfunc5 :::"convergent"::: ) ) & (Bool (Set ($#k2_mesfunc5 :::"lim"::: ) (Set "(" (Set "(" (Set (Var "FF")) ($#k10_mesfunc9 :::"."::: ) (Set (Var "n")) ")" ) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ($#k1_mesfunc9 :::"."::: ) (Set (Var "x")))) ")" ) ")" ) ")" ))))))) ; theorem :: MESFUNC9:50 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "E")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool (Set (Var "E")) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ))) & (Bool (Set (Var "F")) "is" ($#v2_mesfunc9 :::"additive"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n"))) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "E"))) & (Bool (Set (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n"))) "is" ($#v6_supinf_2 :::"nonnegative"::: ) ) ")" ) ")" )) "holds" (Bool "ex" (Set (Var "I")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) "st" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set (Set (Var "I")) ($#k1_mesfunc9 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k7_mesfunc5 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ")" )) & (Bool (Set ($#k7_mesfunc5 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" (Set "(" ($#k4_mesfunc9 :::"Partial_Sums"::: ) (Set (Var "F")) ")" ) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_mesfunc9 :::"Partial_Sums"::: ) (Set (Var "I")) ")" ) ($#k1_mesfunc9 :::"."::: ) (Set (Var "n")))) ")" )))))))) ; theorem :: MESFUNC9:51 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "E")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool (Set (Var "E")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ))) & (Bool (Set (Var "F")) "is" ($#v2_mesfunc9 :::"additive"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n"))) "is" ($#v6_supinf_2 :::"nonnegative"::: ) ) & (Bool (Set (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n"))) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "E"))) ")" ) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "E")))) "holds" (Bool (Set (Set (Var "F")) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x"))) "is" ($#v1_mesfunc9 :::"summable"::: ) ) ")" )) "holds" (Bool "ex" (Set (Var "I")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) "st" (Bool "(" (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "I")) ($#k1_mesfunc9 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k7_mesfunc5 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set (Var "E")) ")" ) ")" )) ")" ) & (Bool (Set (Var "I")) "is" ($#v1_mesfunc9 :::"summable"::: ) ) & (Bool (Set ($#k7_mesfunc5 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" (Set "(" ($#k7_mesfunc8 :::"lim"::: ) (Set "(" ($#k4_mesfunc9 :::"Partial_Sums"::: ) (Set (Var "F")) ")" ) ")" ) ($#k2_partfun1 :::"|"::: ) (Set (Var "E")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_mesfunc9 :::"Sum"::: ) (Set (Var "I")))) ")" ))))))) ; theorem :: MESFUNC9:52 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "E")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool (Set (Var "E")) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ))) & (Bool (Set (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) "is" ($#v6_supinf_2 :::"nonnegative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n"))) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "E"))) ")" ) & (Bool "(" "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m")))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "E")))) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ($#k1_mesfunc9 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "m")) ")" ) ($#k1_mesfunc9 :::"."::: ) (Set (Var "x"))))) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "E")))) "holds" (Bool (Set (Set (Var "F")) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x"))) "is" ($#v10_mesfunc5 :::"convergent"::: ) ) ")" )) "holds" (Bool "ex" (Set (Var "I")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) "st" (Bool "(" (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "I")) ($#k1_mesfunc9 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k7_mesfunc5 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ")" )) ")" ) & (Bool (Set (Var "I")) "is" ($#v10_mesfunc5 :::"convergent"::: ) ) & (Bool (Set ($#k7_mesfunc5 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" ($#k7_mesfunc8 :::"lim"::: ) (Set (Var "F")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_mesfunc5 :::"lim"::: ) (Set (Var "I")))) ")" ))))))) ;