:: MESFUNC5 semantic presentation begin theorem :: MESFUNC5:1 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"R_eal":::) "holds" (Bool (Set ($#k3_extreal1 :::"|."::: ) (Set "(" (Set (Var "x")) ($#k4_supinf_2 :::"-"::: ) (Set (Var "y")) ")" ) ($#k3_extreal1 :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k3_extreal1 :::"|."::: ) (Set "(" (Set (Var "y")) ($#k4_supinf_2 :::"-"::: ) (Set (Var "x")) ")" ) ($#k3_extreal1 :::".|"::: ) ))) ; theorem :: MESFUNC5:2 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"R_eal":::) "holds" (Bool (Set (Set (Var "y")) ($#k4_supinf_2 :::"-"::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_extreal1 :::"|."::: ) (Set "(" (Set (Var "x")) ($#k4_supinf_2 :::"-"::: ) (Set (Var "y")) ")" ) ($#k3_extreal1 :::".|"::: ) ))) ; theorem :: MESFUNC5:3 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"R_eal":::) (Bool "for" (Set (Var "e")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" "not" (Bool (Set ($#k3_extreal1 :::"|."::: ) (Set "(" (Set (Var "x")) ($#k4_supinf_2 :::"-"::: ) (Set (Var "y")) ")" ) ($#k3_extreal1 :::".|"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "e"))) "or" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_supinf_1 :::"+infty"::: ) )) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k1_supinf_1 :::"+infty"::: ) )) ")" ) "or" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k2_supinf_1 :::"-infty"::: ) )) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k2_supinf_1 :::"-infty"::: ) )) ")" ) "or" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_supinf_1 :::"+infty"::: ) )) & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k2_supinf_1 :::"-infty"::: ) )) & (Bool (Set (Var "y")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_supinf_1 :::"+infty"::: ) )) & (Bool (Set (Var "y")) ($#r1_hidden :::"<>"::: ) (Set ($#k2_supinf_1 :::"-infty"::: ) )) ")" ) ")" ))) ; theorem :: MESFUNC5:4 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"R_eal":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "p"))) & (Bool (Set (Var "p")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n")))) "holds" (Bool "ex" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Num 2) ($#k2_newton :::"|^"::: ) (Set (Var "n")) ")" ) ($#k8_real_1 :::"*"::: ) (Set (Var "n")))) & (Bool (Set (Set "(" (Set (Var "k")) ($#k5_real_1 :::"-"::: ) (Num 1) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Num 2) ($#k2_newton :::"|^"::: ) (Set (Var "n")) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "p"))) & (Bool (Set (Var "p")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "k")) ($#k6_real_1 :::"/"::: ) (Set "(" (Num 2) ($#k2_newton :::"|^"::: ) (Set (Var "n")) ")" ))) ")" )))) ; theorem :: MESFUNC5:5 (Bool "for" (Set (Var "n")) "," (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"R_eal":::) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Num 2) ($#k2_newton :::"|^"::: ) (Set (Var "n")) ")" ) ($#k8_real_1 :::"*"::: ) (Set (Var "n")))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "p")))) "holds" (Bool (Set (Set (Var "k")) ($#k6_real_1 :::"/"::: ) (Set "(" (Num 2) ($#k2_newton :::"|^"::: ) (Set (Var "n")) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "p"))))) ; theorem :: MESFUNC5:6 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "k")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k")))) "holds" (Bool "(" (Bool (Set (Set (Var "k")) ($#k4_xxreal_3 :::"*"::: ) (Set "(" ($#k4_xxreal_0 :::"max"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_xxreal_0 :::"max"::: ) "(" (Set "(" (Set (Var "k")) ($#k4_xxreal_3 :::"*"::: ) (Set (Var "x")) ")" ) "," (Set "(" (Set (Var "k")) ($#k4_xxreal_3 :::"*"::: ) (Set (Var "y")) ")" ) ")" )) & (Bool (Set (Set (Var "k")) ($#k4_xxreal_3 :::"*"::: ) (Set "(" ($#k3_xxreal_0 :::"min"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_xxreal_0 :::"min"::: ) "(" (Set "(" (Set (Var "k")) ($#k4_xxreal_3 :::"*"::: ) (Set (Var "x")) ")" ) "," (Set "(" (Set (Var "k")) ($#k4_xxreal_3 :::"*"::: ) (Set (Var "y")) ")" ) ")" )) ")" )) ; theorem :: MESFUNC5:7 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "k")) "being" ($#m1_subset_1 :::"R_eal":::) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set (Set (Var "k")) ($#k4_xxreal_3 :::"*"::: ) (Set "(" ($#k3_xxreal_0 :::"min"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_xxreal_0 :::"max"::: ) "(" (Set "(" (Set (Var "k")) ($#k1_extreal1 :::"*"::: ) (Set (Var "x")) ")" ) "," (Set "(" (Set (Var "k")) ($#k1_extreal1 :::"*"::: ) (Set (Var "y")) ")" ) ")" )) & (Bool (Set (Set (Var "k")) ($#k4_xxreal_3 :::"*"::: ) (Set "(" ($#k4_xxreal_0 :::"max"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_xxreal_0 :::"min"::: ) "(" (Set "(" (Set (Var "k")) ($#k1_extreal1 :::"*"::: ) (Set (Var "x")) ")" ) "," (Set "(" (Set (Var "k")) ($#k1_extreal1 :::"*"::: ) (Set (Var "y")) ")" ) ")" )) ")" )) ; begin definitionlet "IT" be ($#m1_hidden :::"set"::: ) ; attr "IT" is :::"nonpositive"::: means :: MESFUNC5:def 1 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"R_eal":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "IT")) "holds" (Bool (Set (Var "x")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) ))); end; :: deftheorem defines :::"nonpositive"::: MESFUNC5:def 1 : (Bool "for" (Set (Var "IT")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v1_mesfunc5 :::"nonpositive"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"R_eal":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "IT")))) "holds" (Bool (Set (Var "x")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ")" )); definitionlet "R" be ($#m1_hidden :::"Relation":::); attr "R" is :::"nonpositive"::: means :: MESFUNC5:def 2 (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) "R") "is" ($#v1_mesfunc5 :::"nonpositive"::: ) ); end; :: deftheorem defines :::"nonpositive"::: MESFUNC5:def 2 : (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v2_mesfunc5 :::"nonpositive"::: ) ) "iff" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R"))) "is" ($#v1_mesfunc5 :::"nonpositive"::: ) ) ")" )); theorem :: MESFUNC5:8 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v2_mesfunc5 :::"nonpositive"::: ) ) "iff" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "F")) ($#k12_supinf_2 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_supinf_2 :::"0."::: ) ))) ")" ))) ; theorem :: MESFUNC5:9 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool (Set (Set (Var "F")) ($#k12_supinf_2 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_supinf_2 :::"0."::: ) )) ")" )) "holds" (Bool (Set (Var "F")) "is" ($#v2_mesfunc5 :::"nonpositive"::: ) ))) ; definitionlet "R" be ($#m1_hidden :::"Relation":::); attr "R" is :::"without-infty"::: means :: MESFUNC5:def 3 (Bool (Bool "not" (Set ($#k2_supinf_1 :::"-infty"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) "R"))); attr "R" is :::"without+infty"::: means :: MESFUNC5:def 4 (Bool (Bool "not" (Set ($#k1_supinf_1 :::"+infty"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) "R"))); end; :: deftheorem defines :::"without-infty"::: MESFUNC5:def 3 : (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v3_mesfunc5 :::"without-infty"::: ) ) "iff" (Bool (Bool "not" (Set ($#k2_supinf_1 :::"-infty"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R"))))) ")" )); :: deftheorem defines :::"without+infty"::: MESFUNC5:def 4 : (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v4_mesfunc5 :::"without+infty"::: ) ) "iff" (Bool (Bool "not" (Set ($#k1_supinf_1 :::"+infty"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R"))))) ")" )); definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ); :: original: :::"without-infty"::: redefine attr "f" is :::"without-infty"::: means :: MESFUNC5:def 5 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k2_supinf_1 :::"-infty"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set "f" ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))))); :: original: :::"without+infty"::: redefine attr "f" is :::"without+infty"::: means :: MESFUNC5:def 6 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set "f" ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_supinf_1 :::"+infty"::: ) ))); end; :: deftheorem defines :::"without-infty"::: MESFUNC5:def 5 : (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v3_mesfunc5 :::"without-infty"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k2_supinf_1 :::"-infty"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "f")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))))) ")" ))); :: deftheorem defines :::"without+infty"::: MESFUNC5:def 6 : (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v4_mesfunc5 :::"without+infty"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "f")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_supinf_1 :::"+infty"::: ) ))) ")" ))); theorem :: MESFUNC5:10 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "holds" (Bool "(" (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set ($#k2_supinf_1 :::"-infty"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "f")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x")))) ")" ) "iff" (Bool (Set (Var "f")) "is" ()) ")" ))) ; theorem :: MESFUNC5:11 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "holds" (Bool "(" (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_supinf_1 :::"+infty"::: ) )) ")" ) "iff" (Bool (Set (Var "f")) "is" ()) ")" ))) ; theorem :: MESFUNC5:12 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) "is" ($#v6_supinf_2 :::"nonnegative"::: ) )) "holds" (Bool (Set (Var "f")) "is" ()))) ; theorem :: MESFUNC5:13 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) "is" ($#v2_mesfunc5 :::"nonpositive"::: ) )) "holds" (Bool (Set (Var "f")) "is" ()))) ; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster ($#v1_funct_1 :::"Function-like"::: ) ($#v6_supinf_2 :::"nonnegative"::: ) -> () for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) "X" "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )); cluster ($#v1_funct_1 :::"Function-like"::: ) ($#v2_mesfunc5 :::"nonpositive"::: ) -> () for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) "X" "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )); end; theorem :: MESFUNC5: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 "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r1_mesfunc2 :::"is_simple_func_in"::: ) (Set (Var "S")))) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ()) & (Bool (Set (Var "f")) "is" ()) ")" )))) ; theorem :: MESFUNC5:15 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) "is" ($#v6_supinf_2 :::"nonnegative"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "Y"))) "is" ($#v6_supinf_2 :::"nonnegative"::: ) )))) ; theorem :: MESFUNC5:16 (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" ()) & (Bool (Set (Var "g")) "is" ())) "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 :: MESFUNC5:17 (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" ()) & (Bool (Set (Var "g")) "is" ())) "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 :: MESFUNC5:18 (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")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k3_numbers :::"RAT"::: ) ) "," (Set (Var "S")) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "A")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "f")) "is" ()) & (Bool (Set (Var "g")) "is" ()) & (Bool "(" "for" (Set (Var "p")) "being" ($#m1_hidden :::"Rational":::) "holds" (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k15_mesfunc1 :::"less_dom"::: ) "(" (Set (Var "f")) "," (Set "(" ($#k1_measure6 :::"R_EAL"::: ) (Set (Var "p")) ")" ) ")" ")" ) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k15_mesfunc1 :::"less_dom"::: ) "(" (Set (Var "g")) "," (Set "(" ($#k1_measure6 :::"R_EAL"::: ) (Set "(" (Set (Var "r")) ($#k9_real_1 :::"-"::: ) (Set (Var "p")) ")" ) ")" ) ")" ")" ) ")" ))) ")" )) "holds" (Bool (Set (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k15_mesfunc1 :::"less_dom"::: ) "(" (Set "(" (Set (Var "f")) ($#k3_mesfunc1 :::"+"::: ) (Set (Var "g")) ")" ) "," (Set "(" ($#k1_measure6 :::"R_EAL"::: ) (Set (Var "r")) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "F")) ")" ))))))))) ; definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); func :::"R_EAL"::: "f" -> ($#m1_subset_1 :::"PartFunc":::) "of" "X" "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) equals :: MESFUNC5:def 7 "f"; end; :: deftheorem defines :::"R_EAL"::: MESFUNC5:def 7 : (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k1_mesfunc5 :::"R_EAL"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "f"))))); theorem :: MESFUNC5:19 (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")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) "is" ($#v6_supinf_2 :::"nonnegative"::: ) ) & (Bool (Set (Var "g")) "is" ($#v6_supinf_2 :::"nonnegative"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k3_mesfunc1 :::"+"::: ) (Set (Var "g"))) "is" ($#v6_supinf_2 :::"nonnegative"::: ) ))))) ; theorem :: MESFUNC5:20 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "f")) "is" ($#v6_supinf_2 :::"nonnegative"::: ) )) "holds" (Bool "(" "(" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "c")))) "implies" (Bool (Set (Set (Var "c")) ($#k6_mesfunc1 :::"(#)"::: ) (Set (Var "f"))) "is" ($#v6_supinf_2 :::"nonnegative"::: ) ) ")" & "(" (Bool (Bool (Set (Var "c")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set (Set (Var "c")) ($#k6_mesfunc1 :::"(#)"::: ) (Set (Var "f"))) "is" ($#v2_mesfunc5 :::"nonpositive"::: ) ) ")" ")" )))) ; theorem :: MESFUNC5:21 (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 "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "g")) ")" )))) "holds" (Bool "(" (Bool (Set (Set (Var "g")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "f")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x")))) & (Bool (Set ($#k2_supinf_1 :::"-infty"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "g")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x")))) & (Bool (Set (Set (Var "f")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_supinf_1 :::"+infty"::: ) )) ")" ) ")" )) "holds" (Bool (Set (Set (Var "f")) ($#k4_mesfunc1 :::"-"::: ) (Set (Var "g"))) "is" ($#v6_supinf_2 :::"nonnegative"::: ) ))) ; theorem :: MESFUNC5:22 (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" ($#v6_supinf_2 :::"nonnegative"::: ) ) & (Bool (Set (Var "g")) "is" ($#v6_supinf_2 :::"nonnegative"::: ) )) "holds" (Bool "(" (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")) ")" ))) & (Bool (Set (Set (Var "f")) ($#k3_mesfunc1 :::"+"::: ) (Set (Var "g"))) "is" ($#v6_supinf_2 :::"nonnegative"::: ) ) ")" ))) ; theorem :: MESFUNC5:23 (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")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) "is" ($#v6_supinf_2 :::"nonnegative"::: ) ) & (Bool (Set (Var "g")) "is" ($#v6_supinf_2 :::"nonnegative"::: ) ) & (Bool (Set (Var "h")) "is" ($#v6_supinf_2 :::"nonnegative"::: ) )) "holds" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" (Set (Var "f")) ($#k3_mesfunc1 :::"+"::: ) (Set (Var "g")) ")" ) ($#k3_mesfunc1 :::"+"::: ) (Set (Var "h")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "g")) ")" ) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "h")) ")" ))) & (Bool (Set (Set "(" (Set (Var "f")) ($#k3_mesfunc1 :::"+"::: ) (Set (Var "g")) ")" ) ($#k3_mesfunc1 :::"+"::: ) (Set (Var "h"))) "is" ($#v6_supinf_2 :::"nonnegative"::: ) ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set "(" (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "g")) ")" ) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "h")) ")" )))) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "f")) ($#k3_mesfunc1 :::"+"::: ) (Set (Var "g")) ")" ) ($#k3_mesfunc1 :::"+"::: ) (Set (Var "h")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "f")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k3_supinf_2 :::"+"::: ) (Set "(" (Set (Var "g")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x")) ")" ) ")" ) ($#k3_supinf_2 :::"+"::: ) (Set "(" (Set (Var "h")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x")) ")" ))) ")" ) ")" ))) ; theorem :: MESFUNC5:24 (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" ()) & (Bool (Set (Var "g")) "is" ())) "holds" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" ($#k1_mesfunc2 :::"max+"::: ) (Set "(" (Set (Var "f")) ($#k3_mesfunc1 :::"+"::: ) (Set (Var "g")) ")" ) ")" ) ($#k3_mesfunc1 :::"+"::: ) (Set "(" ($#k2_mesfunc2 :::"max-"::: ) (Set (Var "f")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "g")) ")" ))) & (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" ($#k2_mesfunc2 :::"max-"::: ) (Set "(" (Set (Var "f")) ($#k3_mesfunc1 :::"+"::: ) (Set (Var "g")) ")" ) ")" ) ($#k3_mesfunc1 :::"+"::: ) (Set "(" ($#k1_mesfunc2 :::"max+"::: ) (Set (Var "f")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "g")) ")" ))) & (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" (Set "(" ($#k1_mesfunc2 :::"max+"::: ) (Set "(" (Set (Var "f")) ($#k3_mesfunc1 :::"+"::: ) (Set (Var "g")) ")" ) ")" ) ($#k3_mesfunc1 :::"+"::: ) (Set "(" ($#k2_mesfunc2 :::"max-"::: ) (Set (Var "f")) ")" ) ")" ) ($#k3_mesfunc1 :::"+"::: ) (Set "(" ($#k2_mesfunc2 :::"max-"::: ) (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")) ")" ))) & (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" (Set "(" ($#k2_mesfunc2 :::"max-"::: ) (Set "(" (Set (Var "f")) ($#k3_mesfunc1 :::"+"::: ) (Set (Var "g")) ")" ) ")" ) ($#k3_mesfunc1 :::"+"::: ) (Set "(" ($#k1_mesfunc2 :::"max+"::: ) (Set (Var "f")) ")" ) ")" ) ($#k3_mesfunc1 :::"+"::: ) (Set "(" ($#k1_mesfunc2 :::"max+"::: ) (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")) ")" ))) & (Bool (Set (Set "(" ($#k1_mesfunc2 :::"max+"::: ) (Set "(" (Set (Var "f")) ($#k3_mesfunc1 :::"+"::: ) (Set (Var "g")) ")" ) ")" ) ($#k3_mesfunc1 :::"+"::: ) (Set "(" ($#k2_mesfunc2 :::"max-"::: ) (Set (Var "f")) ")" )) "is" ($#v6_supinf_2 :::"nonnegative"::: ) ) & (Bool (Set (Set "(" ($#k2_mesfunc2 :::"max-"::: ) (Set "(" (Set (Var "f")) ($#k3_mesfunc1 :::"+"::: ) (Set (Var "g")) ")" ) ")" ) ($#k3_mesfunc1 :::"+"::: ) (Set "(" ($#k1_mesfunc2 :::"max+"::: ) (Set (Var "f")) ")" )) "is" ($#v6_supinf_2 :::"nonnegative"::: ) ) ")" ))) ; theorem :: MESFUNC5:25 (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" ()) & (Bool (Set (Var "f")) "is" ()) & (Bool (Set (Var "g")) "is" ()) & (Bool (Set (Var "g")) "is" ())) "holds" (Bool (Set (Set "(" (Set "(" ($#k1_mesfunc2 :::"max+"::: ) (Set "(" (Set (Var "f")) ($#k3_mesfunc1 :::"+"::: ) (Set (Var "g")) ")" ) ")" ) ($#k3_mesfunc1 :::"+"::: ) (Set "(" ($#k2_mesfunc2 :::"max-"::: ) (Set (Var "f")) ")" ) ")" ) ($#k3_mesfunc1 :::"+"::: ) (Set "(" ($#k2_mesfunc2 :::"max-"::: ) (Set (Var "g")) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set "(" ($#k2_mesfunc2 :::"max-"::: ) (Set "(" (Set (Var "f")) ($#k3_mesfunc1 :::"+"::: ) (Set (Var "g")) ")" ) ")" ) ($#k3_mesfunc1 :::"+"::: ) (Set "(" ($#k1_mesfunc2 :::"max+"::: ) (Set (Var "f")) ")" ) ")" ) ($#k3_mesfunc1 :::"+"::: ) (Set "(" ($#k1_mesfunc2 :::"max+"::: ) (Set (Var "g")) ")" ))))) ; theorem :: MESFUNC5:26 (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 ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "c")))) "holds" (Bool "(" (Bool (Set ($#k1_mesfunc2 :::"max+"::: ) (Set "(" (Set (Var "c")) ($#k6_mesfunc1 :::"(#)"::: ) (Set (Var "f")) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "c")) ($#k6_mesfunc1 :::"(#)"::: ) (Set "(" ($#k1_mesfunc2 :::"max+"::: ) (Set (Var "f")) ")" ))) & (Bool (Set ($#k2_mesfunc2 :::"max-"::: ) (Set "(" (Set (Var "c")) ($#k6_mesfunc1 :::"(#)"::: ) (Set (Var "f")) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "c")) ($#k6_mesfunc1 :::"(#)"::: ) (Set "(" ($#k2_mesfunc2 :::"max-"::: ) (Set (Var "f")) ")" ))) ")" )))) ; theorem :: MESFUNC5:27 (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 ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "c")))) "holds" (Bool "(" (Bool (Set ($#k1_mesfunc2 :::"max+"::: ) (Set "(" (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "c")) ")" ) ($#k6_mesfunc1 :::"(#)"::: ) (Set (Var "f")) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "c")) ($#k6_mesfunc1 :::"(#)"::: ) (Set "(" ($#k2_mesfunc2 :::"max-"::: ) (Set (Var "f")) ")" ))) & (Bool (Set ($#k2_mesfunc2 :::"max-"::: ) (Set "(" (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "c")) ")" ) ($#k6_mesfunc1 :::"(#)"::: ) (Set (Var "f")) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "c")) ($#k6_mesfunc1 :::"(#)"::: ) (Set "(" ($#k1_mesfunc2 :::"max+"::: ) (Set (Var "f")) ")" ))) ")" )))) ; theorem :: MESFUNC5: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 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k1_mesfunc2 :::"max+"::: ) (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A")) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set "(" ($#k1_mesfunc2 :::"max+"::: ) (Set (Var "f")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set (Var "A")))) & (Bool (Set ($#k2_mesfunc2 :::"max-"::: ) (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A")) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set "(" ($#k2_mesfunc2 :::"max-"::: ) (Set (Var "f")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set (Var "A")))) ")" )))) ; theorem :: MESFUNC5:29 (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"::: ) ) (Bool "for" (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k3_mesfunc1 :::"+"::: ) (Set (Var "g")) ")" )))) "holds" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" (Set (Var "f")) ($#k3_mesfunc1 :::"+"::: ) (Set (Var "g")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "B"))) & (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "B")) ")" ) ($#k3_mesfunc1 :::"+"::: ) (Set "(" (Set (Var "g")) ($#k2_partfun1 :::"|"::: ) (Set (Var "B")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "B"))) & (Bool (Set (Set "(" (Set (Var "f")) ($#k3_mesfunc1 :::"+"::: ) (Set (Var "g")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set (Var "B"))) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "B")) ")" ) ($#k3_mesfunc1 :::"+"::: ) (Set "(" (Set (Var "g")) ($#k2_partfun1 :::"|"::: ) (Set (Var "B")) ")" ))) ")" )))) ; theorem :: MESFUNC5: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 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"R_eal":::) "holds" (Bool (Set ($#k19_mesfunc1 :::"eq_dom"::: ) "(" (Set (Var "f")) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "a")) ($#k1_tarski :::"}"::: ) )))))) ; begin theorem :: MESFUNC5:31 (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")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "f")) "is" ()) & (Bool (Set (Var "g")) "is" ()) & (Bool (Set (Var "f")) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "A"))) & (Bool (Set (Var "g")) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "A")))) "holds" (Bool (Set (Set (Var "f")) ($#k3_mesfunc1 :::"+"::: ) (Set (Var "g"))) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "A"))))))) ; theorem :: MESFUNC5:32 (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 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r1_mesfunc2 :::"is_simple_func_in"::: ) (Set (Var "S"))) & (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "ex" (Set (Var "F")) "being" ($#m2_finseq_1 :::"Finite_Sep_Sequence":::) "of" (Set (Var "S"))(Bool "ex" (Set (Var "a")) "," (Set (Var "x")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool "(" (Bool (Set (Var "F")) "," (Set (Var "a")) ($#r1_mesfunc3 :::"are_Re-presentation_of"::: ) (Set (Var "f"))) & (Bool (Set (Set (Var "a")) ($#k12_supinf_2 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 2) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "a"))))) "holds" (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "a")) ($#k12_supinf_2 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Set (Var "a")) ($#k12_supinf_2 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_supinf_1 :::"+infty"::: ) )) ")" ) ")" ) & (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "F")))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "x"))))) "holds" (Bool (Set (Set (Var "x")) ($#k12_supinf_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k12_supinf_2 :::"."::: ) (Set (Var "n")) ")" ) ($#k1_extreal1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "M")) ($#k4_finseqop :::"*"::: ) (Set (Var "F")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "n")) ")" ))) ")" ) & (Bool (Set ($#k4_extreal1 :::"Sum"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ))))))) ; theorem :: MESFUNC5:33 (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 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) (Bool "for" (Set (Var "r")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "f")) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "A"))) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k18_mesfunc1 :::"great_eq_dom"::: ) "(" (Set (Var "f")) "," (Set "(" ($#k1_measure6 :::"R_EAL"::: ) (Set (Var "r")) ")" ) ")" ")" ) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k15_mesfunc1 :::"less_dom"::: ) "(" (Set (Var "f")) "," (Set "(" ($#k1_measure6 :::"R_EAL"::: ) (Set (Var "s")) ")" ) ")" ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "S")))))))) ; theorem :: MESFUNC5:34 (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 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "f")) ($#r1_mesfunc2 :::"is_simple_func_in"::: ) (Set (Var "S")))) "holds" (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A"))) ($#r1_mesfunc2 :::"is_simple_func_in"::: ) (Set (Var "S")))))))) ; theorem :: MESFUNC5: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 "A")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"Finite_Sep_Sequence":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "G")))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool (Set (Set (Var "G")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set (Var "A")))) ")" )) "holds" (Bool (Set (Var "G")) "is" ($#m2_finseq_1 :::"Finite_Sep_Sequence":::) "of" (Set (Var "S")))))))) ; theorem :: MESFUNC5:36 (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 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m2_finseq_1 :::"Finite_Sep_Sequence":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "a")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "G")))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool (Set (Set (Var "G")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set (Var "A")))) ")" ) & (Bool (Set (Var "F")) "," (Set (Var "a")) ($#r1_mesfunc3 :::"are_Re-presentation_of"::: ) (Set (Var "f")))) "holds" (Bool (Set (Var "G")) "," (Set (Var "a")) ($#r1_mesfunc3 :::"are_Re-presentation_of"::: ) (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A")))))))))) ; theorem :: MESFUNC5:37 (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 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r1_mesfunc2 :::"is_simple_func_in"::: ) (Set (Var "S")))) "holds" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))) "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S"))))))) ; theorem :: MESFUNC5:38 (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")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r1_mesfunc2 :::"is_simple_func_in"::: ) (Set (Var "S"))) & (Bool (Set (Var "g")) ($#r1_mesfunc2 :::"is_simple_func_in"::: ) (Set (Var "S")))) "holds" (Bool (Set (Set (Var "f")) ($#k3_mesfunc1 :::"+"::: ) (Set (Var "g"))) ($#r1_mesfunc2 :::"is_simple_func_in"::: ) (Set (Var "S")))))) ; theorem :: MESFUNC5:39 (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 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "f")) ($#r1_mesfunc2 :::"is_simple_func_in"::: ) (Set (Var "S")))) "holds" (Bool (Set (Set (Var "c")) ($#k6_mesfunc1 :::"(#)"::: ) (Set (Var "f"))) ($#r1_mesfunc2 :::"is_simple_func_in"::: ) (Set (Var "S")))))))) ; theorem :: MESFUNC5:40 (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")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r1_mesfunc2 :::"is_simple_func_in"::: ) (Set (Var "S"))) & (Bool (Set (Var "g")) ($#r1_mesfunc2 :::"is_simple_func_in"::: ) (Set (Var "S"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k4_mesfunc1 :::"-"::: ) (Set (Var "g")) ")" )))) "holds" (Bool (Set (Set (Var "g")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "f")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x")))) ")" )) "holds" (Bool (Set (Set (Var "f")) ($#k4_mesfunc1 :::"-"::: ) (Set (Var "g"))) "is" ($#v6_supinf_2 :::"nonnegative"::: ) ))))) ; theorem :: MESFUNC5: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 "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "A")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"R_eal":::) "st" (Bool (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_supinf_1 :::"+infty"::: ) )) & (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set ($#k2_supinf_1 :::"-infty"::: ) ))) "holds" (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool "(" (Bool (Set (Var "f")) ($#r1_mesfunc2 :::"is_simple_func_in"::: ) (Set (Var "S"))) & (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "A"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set (Set (Var "f")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "c"))) ")" ) ")" ))))))) ; theorem :: MESFUNC5:42 (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 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "B")) "," (Set (Var "BF")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "f")) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "B"))) & (Bool (Set (Var "BF")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set (Var "B"))))) "holds" (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "B"))) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "BF")))))))) ; theorem :: MESFUNC5:43 (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 "A")) "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 "A")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "f")) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "A"))) & (Bool (Set (Var "g")) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "A"))) & (Bool (Set (Var "f")) "is" ()) & (Bool (Set (Var "g")) "is" ())) "holds" (Bool (Set (Set "(" ($#k1_mesfunc2 :::"max+"::: ) (Set "(" (Set (Var "f")) ($#k3_mesfunc1 :::"+"::: ) (Set (Var "g")) ")" ) ")" ) ($#k3_mesfunc1 :::"+"::: ) (Set "(" ($#k2_mesfunc2 :::"max-"::: ) (Set (Var "f")) ")" )) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "A")))))))) ; theorem :: MESFUNC5: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 "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "A")) "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 "A")) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "g")) ")" ))) & (Bool (Set (Var "f")) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "A"))) & (Bool (Set (Var "g")) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "A"))) & (Bool (Set (Var "f")) "is" ()) & (Bool (Set (Var "g")) "is" ())) "holds" (Bool (Set (Set "(" ($#k2_mesfunc2 :::"max-"::: ) (Set "(" (Set (Var "f")) ($#k3_mesfunc1 :::"+"::: ) (Set (Var "g")) ")" ) ")" ) ($#k3_mesfunc1 :::"+"::: ) (Set "(" ($#k1_mesfunc2 :::"max+"::: ) (Set (Var "f")) ")" )) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "A")))))))) ; theorem :: MESFUNC5: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 "A")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "S")))) "holds" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set (Var "A")))))))) ; theorem :: MESFUNC5: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 "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool "ex" (Set (Var "E1")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool "(" (Bool (Set (Var "E1")) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "f")) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "E1"))) ")" )) & (Bool "ex" (Set (Var "E2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool "(" (Bool (Set (Var "E2")) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "g")))) & (Bool (Set (Var "g")) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "E2"))) ")" )) & (Bool (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_supinf_1 :::"+infty"::: ) ) ($#k1_tarski :::"}"::: ) )) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) & (Bool (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k2_supinf_1 :::"-infty"::: ) ) ($#k1_tarski :::"}"::: ) )) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) & (Bool (Set (Set (Var "g")) ($#k8_relset_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_supinf_1 :::"+infty"::: ) ) ($#k1_tarski :::"}"::: ) )) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) & (Bool (Set (Set (Var "g")) ($#k8_relset_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k2_supinf_1 :::"-infty"::: ) ) ($#k1_tarski :::"}"::: ) )) ($#r2_hidden :::"in"::: ) (Set (Var "S")))) "holds" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k3_mesfunc1 :::"+"::: ) (Set (Var "g")) ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "S"))))))) ; theorem :: MESFUNC5: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 "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool "ex" (Set (Var "E1")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool "(" (Bool (Set (Var "E1")) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "f")) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "E1"))) ")" )) & (Bool "ex" (Set (Var "E2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool "(" (Bool (Set (Var "E2")) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "g")))) & (Bool (Set (Var "g")) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "E2"))) ")" ))) "holds" (Bool "ex" (Set (Var "E")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool "(" (Bool (Set (Var "E")) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k3_mesfunc1 :::"+"::: ) (Set (Var "g")) ")" ))) & (Bool (Set (Set (Var "f")) ($#k3_mesfunc1 :::"+"::: ) (Set (Var "g"))) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "E"))) ")" )))))) ; theorem :: MESFUNC5: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 "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "A")))) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "B"))) "iff" (Bool (Set (Var "f")) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Set (Var "A")) ($#k5_prob_1 :::"/\"::: ) (Set (Var "B")))) ")" )))))) ; theorem :: MESFUNC5: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 "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "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 "ex" (Set (Var "A")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "A"))))) "holds" (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "B")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "f")) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "B")))) "holds" (Bool (Set (Set (Var "c")) ($#k6_mesfunc1 :::"(#)"::: ) (Set (Var "f"))) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "B"))))))))) ; begin definitionmode ExtREAL_sequence is ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ); end; definitionlet "seq" be ($#m1_subset_1 :::"ExtREAL_sequence":::); attr "seq" is :::"convergent_to_finite_number"::: means :: MESFUNC5:def 8 (Bool "ex" (Set (Var "g")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (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 "(" "seq" ($#k8_nat_1 :::"."::: ) (Set (Var "m")) ")" ) ($#k4_supinf_2 :::"-"::: ) (Set "(" ($#k1_measure6 :::"R_EAL"::: ) (Set (Var "g")) ")" ) ")" ) ($#k3_extreal1 :::".|"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "p"))))))); end; :: deftheorem defines :::"convergent_to_finite_number"::: MESFUNC5:def 8 : (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) "holds" (Bool "(" (Bool (Set (Var "seq")) "is" ($#v7_mesfunc5 :::"convergent_to_finite_number"::: ) ) "iff" (Bool "ex" (Set (Var "g")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (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")) ($#k8_nat_1 :::"."::: ) (Set (Var "m")) ")" ) ($#k4_supinf_2 :::"-"::: ) (Set "(" ($#k1_measure6 :::"R_EAL"::: ) (Set (Var "g")) ")" ) ")" ) ($#k3_extreal1 :::".|"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "p"))))))) ")" )); definitionlet "seq" be ($#m1_subset_1 :::"ExtREAL_sequence":::); attr "seq" is :::"convergent_to_+infty"::: means :: MESFUNC5:def 9 (Bool "for" (Set (Var "g")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "g")))) "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 (Var "g")) ($#r1_xxreal_0 :::"<="::: ) (Set "seq" ($#k8_nat_1 :::"."::: ) (Set (Var "m"))))))); end; :: deftheorem defines :::"convergent_to_+infty"::: MESFUNC5:def 9 : (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) "holds" (Bool "(" (Bool (Set (Var "seq")) "is" ($#v8_mesfunc5 :::"convergent_to_+infty"::: ) ) "iff" (Bool "for" (Set (Var "g")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "g")))) "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 (Var "g")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "seq")) ($#k8_nat_1 :::"."::: ) (Set (Var "m"))))))) ")" )); definitionlet "seq" be ($#m1_subset_1 :::"ExtREAL_sequence":::); attr "seq" is :::"convergent_to_-infty"::: means :: MESFUNC5:def 10 (Bool "for" (Set (Var "g")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "g")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "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 "seq" ($#k8_nat_1 :::"."::: ) (Set (Var "m"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "g")))))); end; :: deftheorem defines :::"convergent_to_-infty"::: MESFUNC5:def 10 : (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) "holds" (Bool "(" (Bool (Set (Var "seq")) "is" ($#v9_mesfunc5 :::"convergent_to_-infty"::: ) ) "iff" (Bool "for" (Set (Var "g")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "g")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "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 (Set (Var "seq")) ($#k8_nat_1 :::"."::: ) (Set (Var "m"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "g")))))) ")" )); theorem :: MESFUNC5:50 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v8_mesfunc5 :::"convergent_to_+infty"::: ) )) "holds" (Bool "(" (Bool (Bool "not" (Set (Var "seq")) "is" ($#v9_mesfunc5 :::"convergent_to_-infty"::: ) )) & (Bool (Bool "not" (Set (Var "seq")) "is" ($#v7_mesfunc5 :::"convergent_to_finite_number"::: ) )) ")" )) ; theorem :: MESFUNC5:51 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v9_mesfunc5 :::"convergent_to_-infty"::: ) )) "holds" (Bool "(" (Bool (Bool "not" (Set (Var "seq")) "is" ($#v8_mesfunc5 :::"convergent_to_+infty"::: ) )) & (Bool (Bool "not" (Set (Var "seq")) "is" ($#v7_mesfunc5 :::"convergent_to_finite_number"::: ) )) ")" )) ; definitionlet "seq" be ($#m1_subset_1 :::"ExtREAL_sequence":::); attr "seq" is :::"convergent"::: means :: MESFUNC5:def 11 (Bool "(" (Bool "seq" "is" ($#v7_mesfunc5 :::"convergent_to_finite_number"::: ) ) "or" (Bool "seq" "is" ($#v8_mesfunc5 :::"convergent_to_+infty"::: ) ) "or" (Bool "seq" "is" ($#v9_mesfunc5 :::"convergent_to_-infty"::: ) ) ")" ); end; :: deftheorem defines :::"convergent"::: MESFUNC5:def 11 : (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) "holds" (Bool "(" (Bool (Set (Var "seq")) "is" ($#v10_mesfunc5 :::"convergent"::: ) ) "iff" (Bool "(" (Bool (Set (Var "seq")) "is" ($#v7_mesfunc5 :::"convergent_to_finite_number"::: ) ) "or" (Bool (Set (Var "seq")) "is" ($#v8_mesfunc5 :::"convergent_to_+infty"::: ) ) "or" (Bool (Set (Var "seq")) "is" ($#v9_mesfunc5 :::"convergent_to_-infty"::: ) ) ")" ) ")" )); definitionlet "seq" be ($#m1_subset_1 :::"ExtREAL_sequence":::); assume (Bool (Set (Const "seq")) "is" ($#v10_mesfunc5 :::"convergent"::: ) ) ; func :::"lim"::: "seq" -> ($#m1_subset_1 :::"R_eal":::) means :: MESFUNC5:def 12 (Bool "(" (Bool "ex" (Set (Var "g")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool "(" (Bool it ($#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 "(" "seq" ($#k8_nat_1 :::"."::: ) (Set (Var "m")) ")" ) ($#k4_supinf_2 :::"-"::: ) it ")" ) ($#k3_extreal1 :::".|"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "p"))))) ")" ) & (Bool "seq" "is" ($#v7_mesfunc5 :::"convergent_to_finite_number"::: ) ) ")" )) "or" (Bool "(" (Bool it ($#r1_hidden :::"="::: ) (Set ($#k1_supinf_1 :::"+infty"::: ) )) & (Bool "seq" "is" ($#v8_mesfunc5 :::"convergent_to_+infty"::: ) ) ")" ) "or" (Bool "(" (Bool it ($#r1_hidden :::"="::: ) (Set ($#k2_supinf_1 :::"-infty"::: ) )) & (Bool "seq" "is" ($#v9_mesfunc5 :::"convergent_to_-infty"::: ) ) ")" ) ")" ); end; :: deftheorem defines :::"lim"::: MESFUNC5:def 12 : (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v10_mesfunc5 :::"convergent"::: ) )) "holds" (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"R_eal":::) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k2_mesfunc5 :::"lim"::: ) (Set (Var "seq")))) "iff" (Bool "(" (Bool "ex" (Set (Var "g")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool "(" (Bool (Set (Var "b2")) ($#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")) ($#k8_nat_1 :::"."::: ) (Set (Var "m")) ")" ) ($#k4_supinf_2 :::"-"::: ) (Set (Var "b2")) ")" ) ($#k3_extreal1 :::".|"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "p"))))) ")" ) & (Bool (Set (Var "seq")) "is" ($#v7_mesfunc5 :::"convergent_to_finite_number"::: ) ) ")" )) "or" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k1_supinf_1 :::"+infty"::: ) )) & (Bool (Set (Var "seq")) "is" ($#v8_mesfunc5 :::"convergent_to_+infty"::: ) ) ")" ) "or" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k2_supinf_1 :::"-infty"::: ) )) & (Bool (Set (Var "seq")) "is" ($#v9_mesfunc5 :::"convergent_to_-infty"::: ) ) ")" ) ")" ) ")" ))); theorem :: MESFUNC5:52 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "seq")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Var "r"))) ")" )) "holds" (Bool "(" (Bool (Set (Var "seq")) "is" ($#v7_mesfunc5 :::"convergent_to_finite_number"::: ) ) & (Bool (Set ($#k2_mesfunc5 :::"lim"::: ) (Set (Var "seq"))) ($#r1_hidden :::"="::: ) (Set (Var "r"))) ")" ))) ; theorem :: MESFUNC5:53 (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "F")) ($#k12_supinf_2 :::"."::: ) (Set (Var "n")))) ")" )) "holds" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k4_extreal1 :::"Sum"::: ) (Set (Var "F"))))) ; theorem :: MESFUNC5:54 (Bool "for" (Set (Var "L")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) "st" (Bool (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 (Set (Set (Var "L")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "L")) ($#k8_nat_1 :::"."::: ) (Set (Var "m")))) ")" )) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v10_mesfunc5 :::"convergent"::: ) ) & (Bool (Set ($#k2_mesfunc5 :::"lim"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set ($#k8_supinf_2 :::"sup"::: ) (Set "(" ($#k17_supinf_2 :::"rng"::: ) (Set (Var "L")) ")" ))) ")" )) ; theorem :: MESFUNC5:55 (Bool "for" (Set (Var "L")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "L")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "G")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")))) ")" )) "holds" (Bool (Set ($#k8_supinf_2 :::"sup"::: ) (Set "(" ($#k17_supinf_2 :::"rng"::: ) (Set (Var "L")) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k8_supinf_2 :::"sup"::: ) (Set "(" ($#k17_supinf_2 :::"rng"::: ) (Set (Var "G")) ")" )))) ; theorem :: MESFUNC5:56 (Bool "for" (Set (Var "L")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "L")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k8_supinf_2 :::"sup"::: ) (Set "(" ($#k17_supinf_2 :::"rng"::: ) (Set (Var "L")) ")" ))))) ; theorem :: MESFUNC5:57 (Bool "for" (Set (Var "L")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) (Bool "for" (Set (Var "K")) "being" ($#m1_subset_1 :::"R_eal":::) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "L")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "K"))) ")" )) "holds" (Bool (Set ($#k8_supinf_2 :::"sup"::: ) (Set "(" ($#k17_supinf_2 :::"rng"::: ) (Set (Var "L")) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "K"))))) ; theorem :: MESFUNC5:58 (Bool "for" (Set (Var "L")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) (Bool "for" (Set (Var "K")) "being" ($#m1_subset_1 :::"R_eal":::) "st" (Bool (Bool (Set (Var "K")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_supinf_1 :::"+infty"::: ) )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "L")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "K"))) ")" )) "holds" (Bool (Set ($#k8_supinf_2 :::"sup"::: ) (Set "(" ($#k17_supinf_2 :::"rng"::: ) (Set (Var "L")) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_supinf_1 :::"+infty"::: ) )))) ; theorem :: MESFUNC5:59 (Bool "for" (Set (Var "L")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) "st" (Bool (Bool (Set (Var "L")) "is" ())) "holds" (Bool "(" (Bool (Set ($#k8_supinf_2 :::"sup"::: ) (Set "(" ($#k17_supinf_2 :::"rng"::: ) (Set (Var "L")) ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k1_supinf_1 :::"+infty"::: ) )) "iff" (Bool "ex" (Set (Var "K")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "K"))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "L")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "K"))) ")" ) ")" )) ")" )) ; theorem :: MESFUNC5:60 (Bool "for" (Set (Var "L")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) (Bool "for" (Set (Var "c")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "L")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Var "c"))) ")" )) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v10_mesfunc5 :::"convergent"::: ) ) & (Bool (Set ($#k2_mesfunc5 :::"lim"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set (Var "c"))) & (Bool (Set ($#k2_mesfunc5 :::"lim"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set ($#k8_supinf_2 :::"sup"::: ) (Set "(" ($#k17_supinf_2 :::"rng"::: ) (Set (Var "L")) ")" ))) ")" ))) ; theorem :: MESFUNC5:61 (Bool "for" (Set (Var "J")) "," (Set (Var "K")) "," (Set (Var "L")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) "st" (Bool (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 (Set (Set (Var "J")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "J")) ($#k8_nat_1 :::"."::: ) (Set (Var "m")))) ")" ) & (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 (Set (Set (Var "K")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "K")) ($#k8_nat_1 :::"."::: ) (Set (Var "m")))) ")" ) & (Bool (Set (Var "J")) "is" ()) & (Bool (Set (Var "K")) "is" ()) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" (Set (Var "J")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k3_supinf_2 :::"+"::: ) (Set "(" (Set (Var "K")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "L")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")))) ")" )) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v10_mesfunc5 :::"convergent"::: ) ) & (Bool (Set ($#k2_mesfunc5 :::"lim"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set ($#k8_supinf_2 :::"sup"::: ) (Set "(" ($#k17_supinf_2 :::"rng"::: ) (Set (Var "L")) ")" ))) & (Bool (Set ($#k2_mesfunc5 :::"lim"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_mesfunc5 :::"lim"::: ) (Set (Var "J")) ")" ) ($#k3_supinf_2 :::"+"::: ) (Set "(" ($#k2_mesfunc5 :::"lim"::: ) (Set (Var "K")) ")" ))) & (Bool (Set ($#k8_supinf_2 :::"sup"::: ) (Set "(" ($#k17_supinf_2 :::"rng"::: ) (Set (Var "L")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k8_supinf_2 :::"sup"::: ) (Set "(" ($#k17_supinf_2 :::"rng"::: ) (Set (Var "K")) ")" ) ")" ) ($#k3_supinf_2 :::"+"::: ) (Set "(" ($#k8_supinf_2 :::"sup"::: ) (Set "(" ($#k17_supinf_2 :::"rng"::: ) (Set (Var "J")) ")" ) ")" ))) ")" )) ; theorem :: MESFUNC5:62 (Bool "for" (Set (Var "L")) "," (Set (Var "K")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "c"))) & (Bool (Set (Var "L")) "is" ()) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "K")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_measure6 :::"R_EAL"::: ) (Set (Var "c")) ")" ) ($#k1_extreal1 :::"*"::: ) (Set "(" (Set (Var "L")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ))) ")" )) "holds" (Bool "(" (Bool (Set ($#k8_supinf_2 :::"sup"::: ) (Set "(" ($#k17_supinf_2 :::"rng"::: ) (Set (Var "K")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_measure6 :::"R_EAL"::: ) (Set (Var "c")) ")" ) ($#k1_extreal1 :::"*"::: ) (Set "(" ($#k8_supinf_2 :::"sup"::: ) (Set "(" ($#k17_supinf_2 :::"rng"::: ) (Set (Var "L")) ")" ) ")" ))) & (Bool (Set (Var "K")) "is" ()) ")" ))) ; theorem :: MESFUNC5:63 (Bool "for" (Set (Var "L")) "," (Set (Var "K")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "c"))) & (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 (Set (Set (Var "L")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "L")) ($#k8_nat_1 :::"."::: ) (Set (Var "m")))) ")" ) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "K")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_measure6 :::"R_EAL"::: ) (Set (Var "c")) ")" ) ($#k1_extreal1 :::"*"::: ) (Set "(" (Set (Var "L")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ))) ")" ) & (Bool (Set (Var "L")) "is" ())) "holds" (Bool "(" (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 (Set (Set (Var "K")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "K")) ($#k8_nat_1 :::"."::: ) (Set (Var "m")))) ")" ) & (Bool (Set (Var "K")) "is" ()) & (Bool (Set (Var "K")) "is" ($#v10_mesfunc5 :::"convergent"::: ) ) & (Bool (Set ($#k2_mesfunc5 :::"lim"::: ) (Set (Var "K"))) ($#r1_hidden :::"="::: ) (Set ($#k8_supinf_2 :::"sup"::: ) (Set "(" ($#k17_supinf_2 :::"rng"::: ) (Set (Var "K")) ")" ))) & (Bool (Set ($#k2_mesfunc5 :::"lim"::: ) (Set (Var "K"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_measure6 :::"R_EAL"::: ) (Set (Var "c")) ")" ) ($#k1_extreal1 :::"*"::: ) (Set "(" ($#k2_mesfunc5 :::"lim"::: ) (Set (Var "L")) ")" ))) ")" ))) ; begin definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "H" be ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Const "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ); let "x" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "X")); func "H" :::"#"::: "x" -> ($#m1_subset_1 :::"ExtREAL_sequence":::) means :: MESFUNC5:def 13 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set it ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "H" ($#k1_seqfunc :::"."::: ) (Set (Var "n")) ")" ) ($#k12_supinf_2 :::"."::: ) "x"))); end; :: deftheorem defines :::"#"::: MESFUNC5:def 13 : (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "H")) "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 "b4")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "H")) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x")))) "iff" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "b4")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "H")) ($#k1_seqfunc :::"."::: ) (Set (Var "n")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))))) ")" ))))); definitionlet "D1", "D2" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k3_rfunct_3 :::"PFuncs"::: ) "(" (Set (Const "D1")) "," (Set (Const "D2")) ")" ")" ); let "n" be ($#m1_hidden :::"Nat":::); :: original: :::"."::: redefine func "F" :::"."::: "n" -> ($#m1_subset_1 :::"PartFunc":::) "of" "D1" "," "D2"; end; theorem :: MESFUNC5:64 (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 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool "ex" (Set (Var "A")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool "(" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "f")) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "A"))) ")" )) & (Bool (Set (Var "f")) "is" ($#v6_supinf_2 :::"nonnegative"::: ) )) "holds" (Bool "ex" (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 "(" (Bool (Set (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n"))) ($#r1_mesfunc2 :::"is_simple_func_in"::: ) (Set (Var "S"))) & (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) ")" ) ")" ) & (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"::: ) ) ")" ) & (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 ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "m")) ")" ) ($#k12_supinf_2 :::"."::: ) (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 (Var "f"))))) "holds" (Bool "(" (Bool (Set (Set (Var "F")) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x"))) "is" ($#v10_mesfunc5 :::"convergent"::: ) ) & (Bool (Set ($#k2_mesfunc5 :::"lim"::: ) (Set "(" (Set (Var "F")) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x")))) ")" ) ")" ) ")" ))))) ; begin definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "X")); let "M" be ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Const "S")); let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ); func :::"integral'"::: "(" "M" "," "f" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) equals :: MESFUNC5:def 14 (Set ($#k1_mesfunc3 :::"integral"::: ) "(" "X" "," "S" "," "M" "," "f" ")" ) if (Bool (Set ($#k1_relset_1 :::"dom"::: ) "f") ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) otherwise (Set ($#k1_supinf_2 :::"0."::: ) ); end; :: deftheorem defines :::"integral'"::: MESFUNC5:def 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 "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set ($#k5_mesfunc5 :::"integral'"::: ) "(" (Set (Var "M")) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_mesfunc3 :::"integral"::: ) "(" (Set (Var "X")) "," (Set (Var "S")) "," (Set (Var "M")) "," (Set (Var "f")) ")" )) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) "implies" (Bool (Set ($#k5_mesfunc5 :::"integral'"::: ) "(" (Set (Var "M")) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_supinf_2 :::"0."::: ) )) ")" ")" ))))); theorem :: MESFUNC5:65 (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")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r1_mesfunc2 :::"is_simple_func_in"::: ) (Set (Var "S"))) & (Bool (Set (Var "g")) ($#r1_mesfunc2 :::"is_simple_func_in"::: ) (Set (Var "S"))) & (Bool (Set (Var "f")) "is" ($#v6_supinf_2 :::"nonnegative"::: ) ) & (Bool (Set (Var "g")) "is" ($#v6_supinf_2 :::"nonnegative"::: ) )) "holds" (Bool "(" (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")) ")" ))) & (Bool (Set ($#k5_mesfunc5 :::"integral'"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "f")) ($#k3_mesfunc1 :::"+"::: ) (Set (Var "g")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_mesfunc5 :::"integral'"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k3_mesfunc1 :::"+"::: ) (Set (Var "g")) ")" ) ")" ) ")" ) ")" ")" ) ($#k3_supinf_2 :::"+"::: ) (Set "(" ($#k5_mesfunc5 :::"integral'"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "g")) ($#k2_partfun1 :::"|"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k3_mesfunc1 :::"+"::: ) (Set (Var "g")) ")" ) ")" ) ")" ) ")" ")" ))) ")" ))))) ; theorem :: MESFUNC5:66 (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 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "f")) ($#r1_mesfunc2 :::"is_simple_func_in"::: ) (Set (Var "S"))) & (Bool (Set (Var "f")) "is" ($#v6_supinf_2 :::"nonnegative"::: ) ) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "c")))) "holds" (Bool (Set ($#k5_mesfunc5 :::"integral'"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "c")) ($#k6_mesfunc1 :::"(#)"::: ) (Set (Var "f")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_measure6 :::"R_EAL"::: ) (Set (Var "c")) ")" ) ($#k1_extreal1 :::"*"::: ) (Set "(" ($#k5_mesfunc5 :::"integral'"::: ) "(" (Set (Var "M")) "," (Set (Var "f")) ")" ")" )))))))) ; theorem :: MESFUNC5:67 (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 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "f")) ($#r1_mesfunc2 :::"is_simple_func_in"::: ) (Set (Var "S"))) & (Bool (Set (Var "f")) "is" ($#v6_supinf_2 :::"nonnegative"::: ) ) & (Bool (Set (Var "A")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "B")))) "holds" (Bool (Set ($#k5_mesfunc5 :::"integral'"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set "(" (Set (Var "A")) ($#k6_prob_1 :::"\/"::: ) (Set (Var "B")) ")" ) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_mesfunc5 :::"integral'"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A")) ")" ) ")" ")" ) ($#k3_supinf_2 :::"+"::: ) (Set "(" ($#k5_mesfunc5 :::"integral'"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "B")) ")" ) ")" ")" )))))))) ; theorem :: MESFUNC5:68 (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 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r1_mesfunc2 :::"is_simple_func_in"::: ) (Set (Var "S"))) & (Bool (Set (Var "f")) "is" ($#v6_supinf_2 :::"nonnegative"::: ) )) "holds" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k5_mesfunc5 :::"integral'"::: ) "(" (Set (Var "M")) "," (Set (Var "f")) ")" )))))) ; theorem :: MESFUNC5:69 (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")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r1_mesfunc2 :::"is_simple_func_in"::: ) (Set (Var "S"))) & (Bool (Set (Var "f")) "is" ($#v6_supinf_2 :::"nonnegative"::: ) ) & (Bool (Set (Var "g")) ($#r1_mesfunc2 :::"is_simple_func_in"::: ) (Set (Var "S"))) & (Bool (Set (Var "g")) "is" ($#v6_supinf_2 :::"nonnegative"::: ) ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k4_mesfunc1 :::"-"::: ) (Set (Var "g")) ")" )))) "holds" (Bool (Set (Set (Var "g")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "f")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x")))) ")" )) "holds" (Bool "(" (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")) ")" ))) & (Bool (Set ($#k5_mesfunc5 :::"integral'"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k4_mesfunc1 :::"-"::: ) (Set (Var "g")) ")" ) ")" ) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_mesfunc5 :::"integral'"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "f")) ($#k4_mesfunc1 :::"-"::: ) (Set (Var "g")) ")" ) ")" ")" ) ($#k3_supinf_2 :::"+"::: ) (Set "(" ($#k5_mesfunc5 :::"integral'"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "g")) ($#k2_partfun1 :::"|"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k4_mesfunc1 :::"-"::: ) (Set (Var "g")) ")" ) ")" ) ")" ) ")" ")" ))) ")" ))))) ; theorem :: MESFUNC5:70 (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")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r1_mesfunc2 :::"is_simple_func_in"::: ) (Set (Var "S"))) & (Bool (Set (Var "g")) ($#r1_mesfunc2 :::"is_simple_func_in"::: ) (Set (Var "S"))) & (Bool (Set (Var "f")) "is" ($#v6_supinf_2 :::"nonnegative"::: ) ) & (Bool (Set (Var "g")) "is" ($#v6_supinf_2 :::"nonnegative"::: ) ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k4_mesfunc1 :::"-"::: ) (Set (Var "g")) ")" )))) "holds" (Bool (Set (Set (Var "g")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "f")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x")))) ")" )) "holds" (Bool (Set ($#k5_mesfunc5 :::"integral'"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "g")) ($#k2_partfun1 :::"|"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k4_mesfunc1 :::"-"::: ) (Set (Var "g")) ")" ) ")" ) ")" ) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k5_mesfunc5 :::"integral'"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k4_mesfunc1 :::"-"::: ) (Set (Var "g")) ")" ) ")" ) ")" ) ")" )))))) ; theorem :: MESFUNC5:71 (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 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"R_eal":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "c"))) & (Bool (Set (Var "f")) ($#r1_mesfunc2 :::"is_simple_func_in"::: ) (Set (Var "S"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "c"))) ")" )) "holds" (Bool (Set ($#k5_mesfunc5 :::"integral'"::: ) "(" (Set (Var "M")) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "c")) ($#k1_extreal1 :::"*"::: ) (Set "(" (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")) ")" ) ")" )))))))) ; theorem :: MESFUNC5:72 (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 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r1_mesfunc2 :::"is_simple_func_in"::: ) (Set (Var "S"))) & (Bool (Set (Var "f")) "is" ($#v6_supinf_2 :::"nonnegative"::: ) )) "holds" (Bool (Set ($#k5_mesfunc5 :::"integral'"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set "(" ($#k19_mesfunc1 :::"eq_dom"::: ) "(" (Set (Var "f")) "," (Set "(" ($#k1_measure6 :::"R_EAL"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ")" ) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )))))) ; theorem :: MESFUNC5:73 (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 "B")) "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 "f")) ($#r1_mesfunc2 :::"is_simple_func_in"::: ) (Set (Var "S"))) & (Bool (Set (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "f")) "is" ($#v6_supinf_2 :::"nonnegative"::: ) )) "holds" (Bool (Set ($#k5_mesfunc5 :::"integral'"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "B")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))))))) ; theorem :: MESFUNC5:74 (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 "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "L")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) "st" (Bool (Bool (Set (Var "g")) ($#r1_mesfunc2 :::"is_simple_func_in"::: ) (Set (Var "S"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "g"))))) "holds" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "g")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x")))) ")" ) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n"))) ($#r1_mesfunc2 :::"is_simple_func_in"::: ) (Set (Var "S"))) ")" ) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "g")))) ")" ) & (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"::: ) ) ")" ) & (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 ($#k1_relset_1 :::"dom"::: ) (Set (Var "g"))))) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "m")) ")" ) ($#k12_supinf_2 :::"."::: ) (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 (Var "g"))))) "holds" (Bool "(" (Bool (Set (Set (Var "F")) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x"))) "is" ($#v10_mesfunc5 :::"convergent"::: ) ) & (Bool (Set (Set (Var "g")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k2_mesfunc5 :::"lim"::: ) (Set "(" (Set (Var "F")) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x")) ")" ))) ")" ) ")" ) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "L")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k5_mesfunc5 :::"integral'"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ")" )) ")" )) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v10_mesfunc5 :::"convergent"::: ) ) & (Bool (Set ($#k5_mesfunc5 :::"integral'"::: ) "(" (Set (Var "M")) "," (Set (Var "g")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k2_mesfunc5 :::"lim"::: ) (Set (Var "L")))) ")" ))))))) ; theorem :: MESFUNC5:75 (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 "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool (Set (Var "g")) ($#r1_mesfunc2 :::"is_simple_func_in"::: ) (Set (Var "S"))) & (Bool (Set (Var "g")) "is" ($#v6_supinf_2 :::"nonnegative"::: ) ) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n"))) ($#r1_mesfunc2 :::"is_simple_func_in"::: ) (Set (Var "S"))) ")" ) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "g")))) ")" ) & (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"::: ) ) ")" ) & (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 ($#k1_relset_1 :::"dom"::: ) (Set (Var "g"))))) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "m")) ")" ) ($#k12_supinf_2 :::"."::: ) (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 (Var "g"))))) "holds" (Bool "(" (Bool (Set (Set (Var "F")) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x"))) "is" ($#v10_mesfunc5 :::"convergent"::: ) ) & (Bool (Set (Set (Var "g")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k2_mesfunc5 :::"lim"::: ) (Set "(" (Set (Var "F")) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x")) ")" ))) ")" ) ")" )) "holds" (Bool "ex" (Set (Var "G")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) "st" (Bool "(" (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "G")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k5_mesfunc5 :::"integral'"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ")" )) ")" ) & (Bool (Set (Var "G")) "is" ($#v10_mesfunc5 :::"convergent"::: ) ) & (Bool (Set ($#k8_supinf_2 :::"sup"::: ) (Set "(" ($#k17_supinf_2 :::"rng"::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_mesfunc5 :::"lim"::: ) (Set (Var "G")))) & (Bool (Set ($#k5_mesfunc5 :::"integral'"::: ) "(" (Set (Var "M")) "," (Set (Var "g")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k2_mesfunc5 :::"lim"::: ) (Set (Var "G")))) ")" ))))))) ; theorem :: MESFUNC5:76 (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 "A")) "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 "K")) "," (Set (Var "L")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) "st" (Bool (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 ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "A"))) ")" ) ")" ) & (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"::: ) ) ")" ) & (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 "A")))) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "m")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))))) ")" ) & (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 ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "G")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "A"))) ")" ) ")" ) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "G")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n"))) "is" ($#v6_supinf_2 :::"nonnegative"::: ) ) ")" ) & (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 "A")))) "holds" (Bool (Set (Set "(" (Set (Var "G")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set (Var "G")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "m")) ")" ) ($#k12_supinf_2 :::"."::: ) (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 "A")))) "holds" (Bool "(" (Bool (Set (Set (Var "F")) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x"))) "is" ($#v10_mesfunc5 :::"convergent"::: ) ) & (Bool (Set (Set (Var "G")) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x"))) "is" ($#v10_mesfunc5 :::"convergent"::: ) ) & (Bool (Set ($#k2_mesfunc5 :::"lim"::: ) (Set "(" (Set (Var "F")) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_mesfunc5 :::"lim"::: ) (Set "(" (Set (Var "G")) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x")) ")" ))) ")" ) ")" ) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set (Set (Var "K")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k5_mesfunc5 :::"integral'"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ")" )) & (Bool (Set (Set (Var "L")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k5_mesfunc5 :::"integral'"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "G")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ")" )) ")" ) ")" )) "holds" (Bool "(" (Bool (Set (Var "K")) "is" ($#v10_mesfunc5 :::"convergent"::: ) ) & (Bool (Set (Var "L")) "is" ($#v10_mesfunc5 :::"convergent"::: ) ) & (Bool (Set ($#k2_mesfunc5 :::"lim"::: ) (Set (Var "K"))) ($#r1_hidden :::"="::: ) (Set ($#k2_mesfunc5 :::"lim"::: ) (Set (Var "L")))) ")" ))))))) ; definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "X")); let "M" be ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Const "S")); let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ); assume that (Bool "ex" (Set (Var "A")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Const "S")) "st" (Bool "(" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Const "f")))) & (Bool (Set (Const "f")) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "A"))) ")" )) and (Bool (Set (Const "f")) "is" ($#v6_supinf_2 :::"nonnegative"::: ) ) ; func :::"integral+"::: "(" "M" "," "f" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) means :: MESFUNC5:def 15 (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" "X" "," (Set ($#k7_numbers :::"ExtREAL"::: ) )(Bool "ex" (Set (Var "K")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) "st" (Bool "(" (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"::: ) "S") & (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) "f")) ")" ) ")" ) & (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"::: ) ) ")" ) & (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" "X" "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) "f"))) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "m")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))))) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "X" "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) "f"))) "holds" (Bool "(" (Bool (Set (Set (Var "F")) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x"))) "is" ($#v10_mesfunc5 :::"convergent"::: ) ) & (Bool (Set ($#k2_mesfunc5 :::"lim"::: ) (Set "(" (Set (Var "F")) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set "f" ($#k12_supinf_2 :::"."::: ) (Set (Var "x")))) ")" ) ")" ) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "K")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k5_mesfunc5 :::"integral'"::: ) "(" "M" "," (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ")" )) ")" ) & (Bool (Set (Var "K")) "is" ($#v10_mesfunc5 :::"convergent"::: ) ) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k2_mesfunc5 :::"lim"::: ) (Set (Var "K")))) ")" ))); end; :: deftheorem defines :::"integral+"::: MESFUNC5:def 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 "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool "ex" (Set (Var "A")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool "(" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "f")) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "A"))) ")" )) & (Bool (Set (Var "f")) "is" ($#v6_supinf_2 :::"nonnegative"::: ) )) "holds" (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k6_mesfunc5 :::"integral+"::: ) "(" (Set (Var "M")) "," (Set (Var "f")) ")" )) "iff" (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) )(Bool "ex" (Set (Var "K")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) "st" (Bool "(" (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 ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) ")" ) ")" ) & (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"::: ) ) ")" ) & (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 ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "m")) ")" ) ($#k12_supinf_2 :::"."::: ) (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 (Var "f"))))) "holds" (Bool "(" (Bool (Set (Set (Var "F")) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x"))) "is" ($#v10_mesfunc5 :::"convergent"::: ) ) & (Bool (Set ($#k2_mesfunc5 :::"lim"::: ) (Set "(" (Set (Var "F")) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x")))) ")" ) ")" ) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "K")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k5_mesfunc5 :::"integral'"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ")" )) ")" ) & (Bool (Set (Var "K")) "is" ($#v10_mesfunc5 :::"convergent"::: ) ) & (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k2_mesfunc5 :::"lim"::: ) (Set (Var "K")))) ")" ))) ")" )))))); theorem :: MESFUNC5:77 (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 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r1_mesfunc2 :::"is_simple_func_in"::: ) (Set (Var "S"))) & (Bool (Set (Var "f")) "is" ($#v6_supinf_2 :::"nonnegative"::: ) )) "holds" (Bool (Set ($#k6_mesfunc5 :::"integral+"::: ) "(" (Set (Var "M")) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_mesfunc5 :::"integral'"::: ) "(" (Set (Var "M")) "," (Set (Var "f")) ")" )))))) ; theorem :: MESFUNC5:78 (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")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool "ex" (Set (Var "A")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool "(" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "f")) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "A"))) ")" )) & (Bool "ex" (Set (Var "B")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool "(" (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "g")))) & (Bool (Set (Var "g")) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "B"))) ")" )) & (Bool (Set (Var "f")) "is" ($#v6_supinf_2 :::"nonnegative"::: ) ) & (Bool (Set (Var "g")) "is" ($#v6_supinf_2 :::"nonnegative"::: ) )) "holds" (Bool "ex" (Set (Var "C")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool "(" (Bool (Set (Var "C")) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k3_mesfunc1 :::"+"::: ) (Set (Var "g")) ")" ))) & (Bool (Set ($#k6_mesfunc5 :::"integral+"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "f")) ($#k3_mesfunc1 :::"+"::: ) (Set (Var "g")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_mesfunc5 :::"integral+"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "C")) ")" ) ")" ")" ) ($#k3_supinf_2 :::"+"::: ) (Set "(" ($#k6_mesfunc5 :::"integral+"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "g")) ($#k2_partfun1 :::"|"::: ) (Set (Var "C")) ")" ) ")" ")" ))) ")" )))))) ; theorem :: MESFUNC5:79 (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 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool "ex" (Set (Var "A")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool "(" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "f")) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "A"))) ")" )) & (Bool (Set (Var "f")) "is" ($#v6_supinf_2 :::"nonnegative"::: ) )) "holds" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_mesfunc5 :::"integral+"::: ) "(" (Set (Var "M")) "," (Set (Var "f")) ")" )))))) ; theorem :: MESFUNC5:80 (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 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool (Bool "ex" (Set (Var "E")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "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"::: ) )) "holds" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_mesfunc5 :::"integral+"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A")) ")" ) ")" ))))))) ; theorem :: MESFUNC5:81 (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 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool (Bool "ex" (Set (Var "E")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "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 (Var "A")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "B")))) "holds" (Bool (Set ($#k6_mesfunc5 :::"integral+"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set "(" (Set (Var "A")) ($#k6_prob_1 :::"\/"::: ) (Set (Var "B")) ")" ) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_mesfunc5 :::"integral+"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A")) ")" ) ")" ")" ) ($#k3_supinf_2 :::"+"::: ) (Set "(" ($#k6_mesfunc5 :::"integral+"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "B")) ")" ) ")" ")" )))))))) ; theorem :: MESFUNC5:82 (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 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool (Bool "ex" (Set (Var "E")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "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 (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k6_mesfunc5 :::"integral+"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))))))) ; theorem :: MESFUNC5:83 (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 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool (Bool "ex" (Set (Var "E")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "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 (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B")))) "holds" (Bool (Set ($#k6_mesfunc5 :::"integral+"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A")) ")" ) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_mesfunc5 :::"integral+"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "B")) ")" ) ")" ))))))) ; theorem :: MESFUNC5:84 (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 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "E")) "," (Set (Var "A")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v6_supinf_2 :::"nonnegative"::: ) ) & (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 (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k6_mesfunc5 :::"integral+"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set "(" (Set (Var "E")) ($#k7_prob_1 :::"\"::: ) (Set (Var "A")) ")" ) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_mesfunc5 :::"integral+"::: ) "(" (Set (Var "M")) "," (Set (Var "f")) ")" ))))))) ; theorem :: MESFUNC5:85 (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")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool "ex" (Set (Var "E")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool "(" (Bool (Set (Var "E")) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "E")) ($#r1_hidden :::"="::: ) (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 (Set (Var "g")) "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 ($#k1_relset_1 :::"dom"::: ) (Set (Var "g"))))) "holds" (Bool (Set (Set (Var "g")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "f")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x")))) ")" )) "holds" (Bool (Set ($#k6_mesfunc5 :::"integral+"::: ) "(" (Set (Var "M")) "," (Set (Var "g")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_mesfunc5 :::"integral+"::: ) "(" (Set (Var "M")) "," (Set (Var "f")) ")" )))))) ; theorem :: MESFUNC5:86 (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 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "c"))) & (Bool "ex" (Set (Var "A")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool "(" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "f")) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "A"))) ")" )) & (Bool (Set (Var "f")) "is" ($#v6_supinf_2 :::"nonnegative"::: ) )) "holds" (Bool (Set ($#k6_mesfunc5 :::"integral+"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "c")) ($#k6_mesfunc1 :::"(#)"::: ) (Set (Var "f")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_measure6 :::"R_EAL"::: ) (Set (Var "c")) ")" ) ($#k1_extreal1 :::"*"::: ) (Set "(" ($#k6_mesfunc5 :::"integral+"::: ) "(" (Set (Var "M")) "," (Set (Var "f")) ")" ")" )))))))) ; theorem :: MESFUNC5:87 (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 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool "ex" (Set (Var "A")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool "(" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "f")) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "A"))) ")" )) & (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 (Var "f"))))) "holds" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x")))) ")" )) "holds" (Bool (Set ($#k6_mesfunc5 :::"integral+"::: ) "(" (Set (Var "M")) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )))))) ; begin definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "X")); let "M" be ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Const "S")); let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ); func :::"Integral"::: "(" "M" "," "f" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) equals :: MESFUNC5:def 16 (Set (Set "(" ($#k6_mesfunc5 :::"integral+"::: ) "(" "M" "," (Set "(" ($#k1_mesfunc2 :::"max+"::: ) "f" ")" ) ")" ")" ) ($#k4_supinf_2 :::"-"::: ) (Set "(" ($#k6_mesfunc5 :::"integral+"::: ) "(" "M" "," (Set "(" ($#k2_mesfunc2 :::"max-"::: ) "f" ")" ) ")" ")" )); end; :: deftheorem defines :::"Integral"::: MESFUNC5:def 16 : (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 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "holds" (Bool (Set ($#k7_mesfunc5 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_mesfunc5 :::"integral+"::: ) "(" (Set (Var "M")) "," (Set "(" ($#k1_mesfunc2 :::"max+"::: ) (Set (Var "f")) ")" ) ")" ")" ) ($#k4_supinf_2 :::"-"::: ) (Set "(" ($#k6_mesfunc5 :::"integral+"::: ) "(" (Set (Var "M")) "," (Set "(" ($#k2_mesfunc2 :::"max-"::: ) (Set (Var "f")) ")" ) ")" ")" ))))))); theorem :: MESFUNC5:88 (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 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool "ex" (Set (Var "A")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool "(" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "f")) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "A"))) ")" )) & (Bool (Set (Var "f")) "is" ($#v6_supinf_2 :::"nonnegative"::: ) )) "holds" (Bool (Set ($#k7_mesfunc5 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_mesfunc5 :::"integral+"::: ) "(" (Set (Var "M")) "," (Set (Var "f")) ")" )))))) ; theorem :: MESFUNC5:89 (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 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r1_mesfunc2 :::"is_simple_func_in"::: ) (Set (Var "S"))) & (Bool (Set (Var "f")) "is" ($#v6_supinf_2 :::"nonnegative"::: ) )) "holds" (Bool "(" (Bool (Set ($#k7_mesfunc5 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_mesfunc5 :::"integral+"::: ) "(" (Set (Var "M")) "," (Set (Var "f")) ")" )) & (Bool (Set ($#k7_mesfunc5 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_mesfunc5 :::"integral'"::: ) "(" (Set (Var "M")) "," (Set (Var "f")) ")" )) ")" ))))) ; theorem :: MESFUNC5:90 (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 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool "ex" (Set (Var "A")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool "(" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "f")) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "A"))) ")" )) & (Bool (Set (Var "f")) "is" ($#v6_supinf_2 :::"nonnegative"::: ) )) "holds" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k7_mesfunc5 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set (Var "f")) ")" )))))) ; theorem :: MESFUNC5:91 (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 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool (Bool "ex" (Set (Var "E")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "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 (Var "A")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "B")))) "holds" (Bool (Set ($#k7_mesfunc5 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set "(" (Set (Var "A")) ($#k6_prob_1 :::"\/"::: ) (Set (Var "B")) ")" ) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_mesfunc5 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A")) ")" ) ")" ")" ) ($#k3_supinf_2 :::"+"::: ) (Set "(" ($#k7_mesfunc5 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "B")) ")" ) ")" ")" )))))))) ; theorem :: MESFUNC5:92 (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 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool (Bool "ex" (Set (Var "E")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "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"::: ) )) "holds" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k7_mesfunc5 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A")) ")" ) ")" ))))))) ; theorem :: MESFUNC5:93 (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 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool (Bool "ex" (Set (Var "E")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "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 (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B")))) "holds" (Bool (Set ($#k7_mesfunc5 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A")) ")" ) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k7_mesfunc5 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "B")) ")" ) ")" ))))))) ; theorem :: MESFUNC5:94 (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 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool (Bool "ex" (Set (Var "E")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "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 (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k7_mesfunc5 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))))))) ; theorem :: MESFUNC5:95 (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 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "E")) "," (Set (Var "A")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "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 (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k7_mesfunc5 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set "(" (Set (Var "E")) ($#k7_prob_1 :::"\"::: ) (Set (Var "A")) ")" ) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k7_mesfunc5 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set (Var "f")) ")" ))))))) ; definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "X")); let "M" be ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Const "S")); let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ); pred "f" :::"is_integrable_on"::: "M" means :: MESFUNC5:def 17 (Bool "(" (Bool "ex" (Set (Var "A")) "being" ($#m2_subset_1 :::"Element"::: ) "of" "S" "st" (Bool "(" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) "f")) & (Bool "f" ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "A"))) ")" )) & (Bool (Set ($#k6_mesfunc5 :::"integral+"::: ) "(" "M" "," (Set "(" ($#k1_mesfunc2 :::"max+"::: ) "f" ")" ) ")" ) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_supinf_1 :::"+infty"::: ) )) & (Bool (Set ($#k6_mesfunc5 :::"integral+"::: ) "(" "M" "," (Set "(" ($#k2_mesfunc2 :::"max-"::: ) "f" ")" ) ")" ) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_supinf_1 :::"+infty"::: ) )) ")" ); end; :: deftheorem defines :::"is_integrable_on"::: MESFUNC5:def 17 : (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 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_mesfunc5 :::"is_integrable_on"::: ) (Set (Var "M"))) "iff" (Bool "(" (Bool "ex" (Set (Var "A")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool "(" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "f")) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "A"))) ")" )) & (Bool (Set ($#k6_mesfunc5 :::"integral+"::: ) "(" (Set (Var "M")) "," (Set "(" ($#k1_mesfunc2 :::"max+"::: ) (Set (Var "f")) ")" ) ")" ) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_supinf_1 :::"+infty"::: ) )) & (Bool (Set ($#k6_mesfunc5 :::"integral+"::: ) "(" (Set (Var "M")) "," (Set "(" ($#k2_mesfunc2 :::"max-"::: ) (Set (Var "f")) ")" ) ")" ) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_supinf_1 :::"+infty"::: ) )) ")" ) ")" ))))); theorem :: MESFUNC5:96 (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 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r1_mesfunc5 :::"is_integrable_on"::: ) (Set (Var "M")))) "holds" (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_mesfunc5 :::"integral+"::: ) "(" (Set (Var "M")) "," (Set "(" ($#k1_mesfunc2 :::"max+"::: ) (Set (Var "f")) ")" ) ")" )) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_mesfunc5 :::"integral+"::: ) "(" (Set (Var "M")) "," (Set "(" ($#k2_mesfunc2 :::"max-"::: ) (Set (Var "f")) ")" ) ")" )) & (Bool (Set ($#k2_supinf_1 :::"-infty"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k7_mesfunc5 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set (Var "f")) ")" )) & (Bool (Set ($#k7_mesfunc5 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set (Var "f")) ")" ) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_supinf_1 :::"+infty"::: ) )) ")" ))))) ; theorem :: MESFUNC5:97 (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 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "f")) ($#r1_mesfunc5 :::"is_integrable_on"::: ) (Set (Var "M")))) "holds" (Bool "(" (Bool (Set ($#k6_mesfunc5 :::"integral+"::: ) "(" (Set (Var "M")) "," (Set "(" ($#k1_mesfunc2 :::"max+"::: ) (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A")) ")" ) ")" ) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_mesfunc5 :::"integral+"::: ) "(" (Set (Var "M")) "," (Set "(" ($#k1_mesfunc2 :::"max+"::: ) (Set (Var "f")) ")" ) ")" )) & (Bool (Set ($#k6_mesfunc5 :::"integral+"::: ) "(" (Set (Var "M")) "," (Set "(" ($#k2_mesfunc2 :::"max-"::: ) (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A")) ")" ) ")" ) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_mesfunc5 :::"integral+"::: ) "(" (Set (Var "M")) "," (Set "(" ($#k2_mesfunc2 :::"max-"::: ) (Set (Var "f")) ")" ) ")" )) & (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A"))) ($#r1_mesfunc5 :::"is_integrable_on"::: ) (Set (Var "M"))) ")" )))))) ; theorem :: MESFUNC5:98 (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 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "f")) ($#r1_mesfunc5 :::"is_integrable_on"::: ) (Set (Var "M"))) & (Bool (Set (Var "A")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "B")))) "holds" (Bool (Set ($#k7_mesfunc5 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set "(" (Set (Var "A")) ($#k6_prob_1 :::"\/"::: ) (Set (Var "B")) ")" ) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_mesfunc5 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A")) ")" ) ")" ")" ) ($#k3_supinf_2 :::"+"::: ) (Set "(" ($#k7_mesfunc5 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "B")) ")" ) ")" ")" )))))))) ; theorem :: MESFUNC5:99 (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 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "f")) ($#r1_mesfunc5 :::"is_integrable_on"::: ) (Set (Var "M"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set (Var "A"))))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A"))) ($#r1_mesfunc5 :::"is_integrable_on"::: ) (Set (Var "M"))) & (Bool (Set ($#k7_mesfunc5 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_mesfunc5 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A")) ")" ) ")" ")" ) ($#k3_supinf_2 :::"+"::: ) (Set "(" ($#k7_mesfunc5 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "B")) ")" ) ")" ")" ))) ")" )))))) ; theorem :: MESFUNC5:100 (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 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool "ex" (Set (Var "A")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool "(" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "f")) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "A"))) ")" ))) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_mesfunc5 :::"is_integrable_on"::: ) (Set (Var "M"))) "iff" (Bool (Set ($#k10_mesfunc1 :::"|."::: ) (Set (Var "f")) ($#k10_mesfunc1 :::".|"::: ) ) ($#r1_mesfunc5 :::"is_integrable_on"::: ) (Set (Var "M"))) ")" ))))) ; theorem :: MESFUNC5:101 (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 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r1_mesfunc5 :::"is_integrable_on"::: ) (Set (Var "M")))) "holds" (Bool (Set ($#k3_extreal1 :::"|."::: ) (Set "(" ($#k7_mesfunc5 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set (Var "f")) ")" ")" ) ($#k3_extreal1 :::".|"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k7_mesfunc5 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set ($#k10_mesfunc1 :::"|."::: ) (Set (Var "f")) ($#k10_mesfunc1 :::".|"::: ) ) ")" )))))) ; theorem :: MESFUNC5:102 (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")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool "ex" (Set (Var "A")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool "(" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "f")) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "A"))) ")" )) & (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "g")))) & (Bool (Set (Var "g")) ($#r1_mesfunc5 :::"is_integrable_on"::: ) (Set (Var "M"))) & (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 (Var "f"))))) "holds" (Bool (Set ($#k3_extreal1 :::"|."::: ) (Set "(" (Set (Var "f")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k3_extreal1 :::".|"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "g")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x")))) ")" )) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_mesfunc5 :::"is_integrable_on"::: ) (Set (Var "M"))) & (Bool (Set ($#k7_mesfunc5 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set ($#k10_mesfunc1 :::"|."::: ) (Set (Var "f")) ($#k10_mesfunc1 :::".|"::: ) ) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k7_mesfunc5 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set (Var "g")) ")" )) ")" ))))) ; theorem :: MESFUNC5:103 (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 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) & (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "r"))) ")" )) "holds" (Bool (Set ($#k1_mesfunc3 :::"integral"::: ) "(" (Set (Var "X")) "," (Set (Var "S")) "," (Set (Var "M")) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k4_xxreal_3 :::"*"::: ) (Set "(" (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")) ")" ) ")" )))))))) ; theorem :: MESFUNC5:104 (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 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "r"))) ")" )) "holds" (Bool (Set ($#k5_mesfunc5 :::"integral'"::: ) "(" (Set (Var "M")) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_measure6 :::"R_EAL"::: ) (Set (Var "r")) ")" ) ($#k1_extreal1 :::"*"::: ) (Set "(" (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")) ")" ) ")" )))))))) ; theorem :: MESFUNC5:105 (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 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r1_mesfunc5 :::"is_integrable_on"::: ) (Set (Var "M")))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_supinf_1 :::"+infty"::: ) ) ($#k1_tarski :::"}"::: ) )) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) & (Bool (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k2_supinf_1 :::"-infty"::: ) ) ($#k1_tarski :::"}"::: ) )) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) & (Bool (Set (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set "(" (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_supinf_1 :::"+infty"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set "(" (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k2_supinf_1 :::"-infty"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set "(" (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_supinf_1 :::"+infty"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k2_supinf_1 :::"-infty"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) & (Bool (Set (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set "(" (Set "(" (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_supinf_1 :::"+infty"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k2_supinf_1 :::"-infty"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ))))) ; theorem :: MESFUNC5:106 (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")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r1_mesfunc5 :::"is_integrable_on"::: ) (Set (Var "M"))) & (Bool (Set (Var "g")) ($#r1_mesfunc5 :::"is_integrable_on"::: ) (Set (Var "M"))) & (Bool (Set (Var "f")) "is" ($#v6_supinf_2 :::"nonnegative"::: ) ) & (Bool (Set (Var "g")) "is" ($#v6_supinf_2 :::"nonnegative"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k3_mesfunc1 :::"+"::: ) (Set (Var "g"))) ($#r1_mesfunc5 :::"is_integrable_on"::: ) (Set (Var "M"))))))) ; theorem :: MESFUNC5:107 (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")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r1_mesfunc5 :::"is_integrable_on"::: ) (Set (Var "M"))) & (Bool (Set (Var "g")) ($#r1_mesfunc5 :::"is_integrable_on"::: ) (Set (Var "M")))) "holds" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k3_mesfunc1 :::"+"::: ) (Set (Var "g")) ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "S"))))))) ; theorem :: MESFUNC5:108 (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")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r1_mesfunc5 :::"is_integrable_on"::: ) (Set (Var "M"))) & (Bool (Set (Var "g")) ($#r1_mesfunc5 :::"is_integrable_on"::: ) (Set (Var "M")))) "holds" (Bool (Set (Set (Var "f")) ($#k3_mesfunc1 :::"+"::: ) (Set (Var "g"))) ($#r1_mesfunc5 :::"is_integrable_on"::: ) (Set (Var "M"))))))) ; theorem :: MESFUNC5:109 (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")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r1_mesfunc5 :::"is_integrable_on"::: ) (Set (Var "M"))) & (Bool (Set (Var "g")) ($#r1_mesfunc5 :::"is_integrable_on"::: ) (Set (Var "M")))) "holds" (Bool "ex" (Set (Var "E")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool "(" (Bool (Set (Var "E")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "g")) ")" ))) & (Bool (Set ($#k7_mesfunc5 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "f")) ($#k3_mesfunc1 :::"+"::: ) (Set (Var "g")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_mesfunc5 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "E")) ")" ) ")" ")" ) ($#k3_supinf_2 :::"+"::: ) (Set "(" ($#k7_mesfunc5 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "g")) ($#k2_partfun1 :::"|"::: ) (Set (Var "E")) ")" ) ")" ")" ))) ")" )))))) ; theorem :: MESFUNC5:110 (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 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "f")) ($#r1_mesfunc5 :::"is_integrable_on"::: ) (Set (Var "M")))) "holds" (Bool "(" (Bool (Set (Set (Var "c")) ($#k6_mesfunc1 :::"(#)"::: ) (Set (Var "f"))) ($#r1_mesfunc5 :::"is_integrable_on"::: ) (Set (Var "M"))) & (Bool (Set ($#k7_mesfunc5 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "c")) ($#k6_mesfunc1 :::"(#)"::: ) (Set (Var "f")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_measure6 :::"R_EAL"::: ) (Set (Var "c")) ")" ) ($#k1_extreal1 :::"*"::: ) (Set "(" ($#k7_mesfunc5 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set (Var "f")) ")" ")" ))) ")" )))))) ; definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "X")); let "M" be ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Const "S")); let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ); let "B" be ($#m2_subset_1 :::"Element"::: ) "of" (Set (Const "S")); func :::"Integral_on"::: "(" "M" "," "B" "," "f" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) equals :: MESFUNC5:def 18 (Set ($#k7_mesfunc5 :::"Integral"::: ) "(" "M" "," (Set "(" "f" ($#k2_partfun1 :::"|"::: ) "B" ")" ) ")" ); end; :: deftheorem defines :::"Integral_on"::: MESFUNC5:def 18 : (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 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "B")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "holds" (Bool (Set ($#k8_mesfunc5 :::"Integral_on"::: ) "(" (Set (Var "M")) "," (Set (Var "B")) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k7_mesfunc5 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "B")) ")" ) ")" ))))))); theorem :: MESFUNC5:111 (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")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "B")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "f")) ($#r1_mesfunc5 :::"is_integrable_on"::: ) (Set (Var "M"))) & (Bool (Set (Var "g")) ($#r1_mesfunc5 :::"is_integrable_on"::: ) (Set (Var "M"))) & (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k3_mesfunc1 :::"+"::: ) (Set (Var "g")) ")" )))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k3_mesfunc1 :::"+"::: ) (Set (Var "g"))) ($#r1_mesfunc5 :::"is_integrable_on"::: ) (Set (Var "M"))) & (Bool (Set ($#k8_mesfunc5 :::"Integral_on"::: ) "(" (Set (Var "M")) "," (Set (Var "B")) "," (Set "(" (Set (Var "f")) ($#k3_mesfunc1 :::"+"::: ) (Set (Var "g")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k8_mesfunc5 :::"Integral_on"::: ) "(" (Set (Var "M")) "," (Set (Var "B")) "," (Set (Var "f")) ")" ")" ) ($#k3_supinf_2 :::"+"::: ) (Set "(" ($#k8_mesfunc5 :::"Integral_on"::: ) "(" (Set (Var "M")) "," (Set (Var "B")) "," (Set (Var "g")) ")" ")" ))) ")" )))))) ; theorem :: MESFUNC5:112 (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 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "B")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "f")) ($#r1_mesfunc5 :::"is_integrable_on"::: ) (Set (Var "M")))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "B"))) ($#r1_mesfunc5 :::"is_integrable_on"::: ) (Set (Var "M"))) & (Bool (Set ($#k8_mesfunc5 :::"Integral_on"::: ) "(" (Set (Var "M")) "," (Set (Var "B")) "," (Set "(" (Set (Var "c")) ($#k6_mesfunc1 :::"(#)"::: ) (Set (Var "f")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_measure6 :::"R_EAL"::: ) (Set (Var "c")) ")" ) ($#k1_extreal1 :::"*"::: ) (Set "(" ($#k8_mesfunc5 :::"Integral_on"::: ) "(" (Set (Var "M")) "," (Set (Var "B")) "," (Set (Var "f")) ")" ")" ))) ")" ))))))) ;