:: MESFUNC7  semantic presentation begin  
















theorem :: MESFUNC7:1 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set  ($#k7_numbers :::"ExtREAL"::: ) )  "st" (Bool (Bool  "("   "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 (Var "f"))  ($#k12_supinf_2 :::"."::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "g"))  ($#k12_supinf_2 :::"."::: )  (Set (Var "x"))))  ")" )) "holds"  (Bool (Set (Set (Var "g"))  ($#k4_mesfunc1 :::"-"::: )  (Set (Var "f"))) "is"   ($#v6_supinf_2 :::"nonnegative"::: )  ))) ; 
 
theorem :: MESFUNC7:2 (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"::: ) )  (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set (Set  "(" (Set (Var "r"))  ($#k6_mesfunc1 :::"(#)"::: )  (Set (Var "f")) ")" )  ($#k2_partfun1 :::"|"::: )  (Set (Var "Y")))  ($#r2_relset_1 :::"="::: )  (Set (Set (Var "r"))  ($#k6_mesfunc1 :::"(#)"::: )  (Set  "(" (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "Y")) ")" ))))))) ; 
 
theorem :: MESFUNC7:3 (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 (Set (Var "g"))  ($#k4_mesfunc1 :::"-"::: )  (Set (Var "f"))) "is"   ($#v6_supinf_2 :::"nonnegative"::: )  )) "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"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "E")) ")" ) ")" )  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k7_mesfunc5 :::"Integral"::: )   "(" (Set (Var "M")) "," (Set  "(" (Set (Var "g"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "E")) ")" ) ")" ))  ")" )))))) ; 
 begin  registrationlet "X" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; 
cluster   ($#v1_relat_1 :::"Relation-like"::: )   "X"  ($#v4_relat_1 :::"-defined"::: )   (Set   ($#k7_numbers :::"ExtREAL"::: )  )  ($#v5_relat_1 :::"-valued"::: )   bbbadV1_FUNCT_1()   ($#v2_valued_0 :::"extreal-yielding"::: )     ($#v6_supinf_2 :::"nonnegative"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1("X" "," (Set  ($#k7_numbers :::"ExtREAL"::: ) ))))); 
end; registrationlet "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"::: ) ); 
cluster (Set  ($#k10_mesfunc1 :::"|."::: ) "f" ($#k10_mesfunc1 :::".|"::: ) ) ->   ($#v6_supinf_2 :::"nonnegative"::: )    for  ($#m1_subset_1 :::"PartFunc":::) "of" "X" "," (Set  ($#k7_numbers :::"ExtREAL"::: ) ); 
end; 
theorem :: MESFUNC7:4 (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  "ex" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set (Var "S")) "st"  (Bool  "("  (Bool  "("   "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "F"))  ($#k3_funct_2 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")) ")" )  ($#k9_subset_1 :::"/\"::: )  (Set  "("  ($#k18_mesfunc1 :::"great_eq_dom"::: )   "(" (Set  ($#k10_mesfunc1 :::"|."::: ) (Set (Var "f")) ($#k10_mesfunc1 :::".|"::: ) ) "," (Set  "("  ($#k1_measure6 :::"R_EAL"::: )  (Set  "(" (Num 1)  ($#k10_real_1 :::"/"::: )  (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" ) ")" ) ")"  ")" )))  ")" ) & (Bool (Set (Set  "("  ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")) ")" )  ($#k7_subset_1 :::"\"::: )  (Set  "("  ($#k19_mesfunc1 :::"eq_dom"::: )   "(" (Set (Var "f")) "," (Set  ($#k1_supinf_2 :::"0."::: ) ) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k3_tarski :::"union"::: )  (Set  "("  ($#k2_relset_1 :::"rng"::: )  (Set (Var "F")) ")" ))) & (Bool  "("   "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"   (Bool  "("  (Bool (Set (Set (Var "F"))  ($#k3_funct_2 :::"."::: )  (Set (Var "n")))  ($#r2_hidden :::"in"::: )  (Set (Var "S"))) & (Bool (Set (Set (Var "M"))  ($#k12_supinf_2 :::"."::: )  (Set  "(" (Set (Var "F"))  ($#k3_funct_2 :::"."::: )  (Set (Var "n")) ")" ))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k1_supinf_1 :::"+infty"::: )  ))  ")" )  ")" )  ")" )))))) ; 
 begin  notationlet "F" be   ($#m1_hidden :::"Relation":::); synonym  :::"extreal-yielding"::: "F" for  :::"ext-real-valued"::: ; end; registration
cluster   ($#v1_relat_1 :::"Relation-like"::: )   (Set   ($#k5_numbers :::"NAT"::: )  )  ($#v4_relat_1 :::"-defined"::: )   bbbadV1_FUNCT_1() bbbadV1_FINSET_1()   ($#v1_finseq_1 :::"FinSequence-like"::: )     ($#v2_finseq_1 :::"FinSubsequence-like"::: )     ($#v2_valued_0 :::"extreal-yielding"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; definitionfunc  :::"multextreal":::  ->   ($#m1_subset_1 :::"BinOp":::) "of" (Set  ($#k7_numbers :::"ExtREAL"::: ) ) means :: MESFUNC7:def 1 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k7_numbers :::"ExtREAL"::: )  ) "holds"  (Bool (Set it  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k1_extreal1 :::"*"::: )  (Set (Var "y"))))); end; 




:: deftheorem    defines :::"multextreal"::: MESFUNC7:def 1 :  (Bool  "for" (Set (Var "b1")) "being"   ($#m1_subset_1 :::"BinOp":::) "of" (Set  ($#k7_numbers :::"ExtREAL"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_mesfunc7 :::"multextreal"::: )  )) "iff" (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k7_numbers :::"ExtREAL"::: )  ) "holds"  (Bool (Set (Set (Var "b1"))  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k1_extreal1 :::"*"::: )  (Set (Var "y")))))  ")" )); 
 registration
cluster (Set   ($#k1_mesfunc7 :::"multextreal"::: )  ) ->   ($#v1_binop_1 :::"commutative"::: )     ($#v2_binop_1 :::"associative"::: )   ; 
end; 
theorem :: MESFUNC7:5 (Bool (Set   ($#k4_binop_1 :::"the_unity_wrt"::: )  (Set  ($#k1_mesfunc7 :::"multextreal"::: ) ))  ($#r1_hidden :::"="::: )  (Num 1)) ; 
 registration
cluster (Set   ($#k1_mesfunc7 :::"multextreal"::: )  ) ->   ($#v1_setwiseo :::"having_a_unity"::: )   ; 
end; definitionlet "F" be   ($#v2_valued_0 :::"extreal-yielding"::: )    ($#m1_hidden :::"FinSequence":::); func  :::"Product"::: "F" ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k7_numbers :::"ExtREAL"::: )  ) means :: MESFUNC7:def 2 (Bool  "ex" (Set (Var "f")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k7_numbers :::"ExtREAL"::: )  ) "st"  (Bool  "("  (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  "F") & (Bool it  ($#r1_hidden :::"="::: )  (Set (Set  ($#k1_mesfunc7 :::"multextreal"::: ) )  ($#k1_finsop_1 :::"$$"::: )  (Set (Var "f"))))  ")" )); end; 





:: deftheorem    defines :::"Product"::: MESFUNC7:def 2 :  (Bool  "for" (Set (Var "F")) "being"   ($#v2_valued_0 :::"extreal-yielding"::: )    ($#m1_hidden :::"FinSequence":::)  (Bool  "for" (Set (Var "b2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k7_numbers :::"ExtREAL"::: )  ) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_mesfunc7 :::"Product"::: )  (Set (Var "F")))) "iff" (Bool  "ex" (Set (Var "f")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k7_numbers :::"ExtREAL"::: )  ) "st"  (Bool  "("  (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set (Var "F"))) & (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k1_mesfunc7 :::"multextreal"::: ) )  ($#k1_finsop_1 :::"$$"::: )  (Set (Var "f"))))  ")" ))  ")" ))); 
 registrationlet "x" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k7_numbers :::"ExtREAL"::: )  ); let "n" be   ($#m1_hidden :::"Nat":::); 
cluster (Set "n"  ($#k2_finseq_2 :::"|->"::: )  "x") ->   ($#v2_valued_0 :::"extreal-yielding"::: )   ; 
end; definitionlet "x" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k7_numbers :::"ExtREAL"::: )  ); let "k" be   ($#m1_hidden :::"Nat":::); func "x" :::"|^"::: "k" ->    ($#m1_hidden :::"set"::: )   equals :: MESFUNC7:def 3 (Set   ($#k2_mesfunc7 :::"Product"::: )  (Set  "(" "k"  ($#k5_finseq_2 :::"|->"::: )  "x" ")" )); end; 






:: deftheorem    defines :::"|^"::: MESFUNC7:def 3 :  (Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k7_numbers :::"ExtREAL"::: )  )  (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set (Var "x"))  ($#k3_mesfunc7 :::"|^"::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_mesfunc7 :::"Product"::: )  (Set  "(" (Set (Var "k"))  ($#k5_finseq_2 :::"|->"::: )  (Set (Var "x")) ")" ))))); 
 definitionlet "x" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k7_numbers :::"ExtREAL"::: )  ); let "k" be   ($#m1_hidden :::"Nat":::); :: original: :::"|^"::: redefine func "x" :::"|^"::: "k" ->   ($#m1_subset_1 :::"R_eal":::); end; registration
cluster (Set   ($#k6_finseq_1 :::"<*>"::: )  (Set  ($#k7_numbers :::"ExtREAL"::: ) )) ->   ($#v2_valued_0 :::"extreal-yielding"::: )   ; 
end; registrationlet "r" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k7_numbers :::"ExtREAL"::: )  ); 
cluster (Set  ($#k5_finseq_1 :::"<*"::: ) "r" ($#k5_finseq_1 :::"*>"::: ) ) ->   ($#v2_valued_0 :::"extreal-yielding"::: )   ; 
end; 
theorem :: MESFUNC7:6 (Bool (Set   ($#k2_mesfunc7 :::"Product"::: )  (Set  "("  ($#k6_finseq_1 :::"<*>"::: )  (Set  ($#k7_numbers :::"ExtREAL"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Num 1)) ; 
 
theorem :: MESFUNC7:7 (Bool  "for" (Set (Var "r")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k7_numbers :::"ExtREAL"::: )  ) "holds"  (Bool (Set   ($#k2_mesfunc7 :::"Product"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "r")) ($#k12_finseq_1 :::"*>"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "r")))) ; 
 registrationlet "f", "g" be   ($#v2_valued_0 :::"extreal-yielding"::: )    ($#m1_hidden :::"FinSequence":::); 
cluster (Set "f"  ($#k7_finseq_1 :::"^"::: )  "g") ->   ($#v2_valued_0 :::"extreal-yielding"::: )   ; 
end; 
theorem :: MESFUNC7:8 (Bool  "for" (Set (Var "F")) "being"   ($#v2_valued_0 :::"extreal-yielding"::: )    ($#m1_hidden :::"FinSequence":::)  (Bool  "for" (Set (Var "r")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k7_numbers :::"ExtREAL"::: )  ) "holds"  (Bool (Set   ($#k2_mesfunc7 :::"Product"::: )  (Set  "(" (Set (Var "F"))  ($#k7_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "r")) ($#k12_finseq_1 :::"*>"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_mesfunc7 :::"Product"::: )  (Set (Var "F")) ")" )  ($#k1_extreal1 :::"*"::: )  (Set (Var "r")))))) ; 
 
theorem :: MESFUNC7:9 (Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k7_numbers :::"ExtREAL"::: )  ) "holds"  (Bool (Set (Set (Var "x"))  ($#k4_mesfunc7 :::"|^"::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Var "x")))) ; 
 
theorem :: MESFUNC7:10 (Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k7_numbers :::"ExtREAL"::: )  )  (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set (Var "x"))  ($#k4_mesfunc7 :::"|^"::: )  (Set  "(" (Set (Var "k"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k4_mesfunc7 :::"|^"::: )  (Set (Var "k")) ")" )  ($#k1_extreal1 :::"*"::: )  (Set (Var "x")))))) ; 
 definitionlet "k" be   ($#m1_hidden :::"Nat":::); let "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"::: ) ); func "f" :::"|^"::: "k" ->   ($#m1_subset_1 :::"PartFunc":::) "of" "X" "," (Set  ($#k7_numbers :::"ExtREAL"::: ) ) means :: MESFUNC7:def 4 (Bool  "("  (Bool (Set   ($#k1_relset_1 :::"dom"::: )  it)  ($#r1_hidden :::"="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  "f")) & (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"::: )  it))) "holds"  (Bool (Set it  ($#k12_supinf_2 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" "f"  ($#k12_supinf_2 :::"."::: )  (Set (Var "x")) ")" )  ($#k4_mesfunc7 :::"|^"::: )  "k"))  ")" )  ")" ); end; 







:: deftheorem    defines :::"|^"::: MESFUNC7:def 4 :  (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "," (Set (Var "b4")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set  ($#k7_numbers :::"ExtREAL"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k5_mesfunc7 :::"|^"::: )  (Set (Var "k")))) "iff" (Bool  "("  (Bool (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "b4")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))) & (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 "b4"))))) "holds"  (Bool (Set (Set (Var "b4"))  ($#k12_supinf_2 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "f"))  ($#k12_supinf_2 :::"."::: )  (Set (Var "x")) ")" )  ($#k4_mesfunc7 :::"|^"::: )  (Set (Var "k"))))  ")" )  ")" )  ")" )))); 
 
theorem :: MESFUNC7:11 (Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k7_numbers :::"ExtREAL"::: )  )  (Bool  "for" (Set (Var "y")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "y")))) "holds"  (Bool (Set (Set (Var "x"))  ($#k4_mesfunc7 :::"|^"::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "y"))  ($#k1_newton :::"|^"::: )  (Set (Var "k"))))))) ; 
 
theorem :: MESFUNC7:12 (Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k7_numbers :::"ExtREAL"::: )  )  (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "x")))) "holds"  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "x"))  ($#k4_mesfunc7 :::"|^"::: )  (Set (Var "k")))))) ; 
 
theorem :: MESFUNC7:13 (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k")))) "holds"  (Bool (Set (Set  ($#k1_supinf_1 :::"+infty"::: ) )  ($#k4_mesfunc7 :::"|^"::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_supinf_1 :::"+infty"::: )  ))) ; 
 
theorem :: MESFUNC7:14 (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  (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 "E")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set (Var "S"))  "st" (Bool (Bool (Set (Var "E"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Var "f"))  ($#r1_mesfunc1 :::"is_measurable_on"::: )  (Set (Var "E")))) "holds"  (Bool (Set (Set  ($#k10_mesfunc1 :::"|."::: ) (Set (Var "f")) ($#k10_mesfunc1 :::".|"::: ) )  ($#k5_mesfunc7 :::"|^"::: )  (Set (Var "k")))  ($#r1_mesfunc1 :::"is_measurable_on"::: )  (Set (Var "E")))))))) ; 
 
theorem :: MESFUNC7: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 "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set  ($#k7_numbers :::"ExtREAL"::: ) )  (Bool  "for" (Set (Var "E")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set (Var "S"))  "st" (Bool (Bool (Set (Set  "("  ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")) ")" )  ($#k9_subset_1 :::"/\"::: )  (Set  "("  ($#k1_relset_1 :::"dom"::: )  (Set (Var "g")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "E"))) & (Bool (Set (Var "f")) "is" bbbadV3_VALUED_0()) & (Bool (Set (Var "g")) "is" bbbadV3_VALUED_0()) & (Bool (Set (Var "f"))  ($#r1_mesfunc1 :::"is_measurable_on"::: )  (Set (Var "E"))) & (Bool (Set (Var "g"))  ($#r1_mesfunc1 :::"is_measurable_on"::: )  (Set (Var "E")))) "holds"  (Bool (Set (Set (Var "f"))  ($#k5_mesfunc1 :::"(#)"::: )  (Set (Var "g")))  ($#r1_mesfunc1 :::"is_measurable_on"::: )  (Set (Var "E"))))))) ; 
 
theorem :: MESFUNC7:16 (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   ($#k2_relset_1 :::"rng"::: )  (Set (Var "f"))) "is"   ($#v5_xxreal_2 :::"real-bounded"::: )  )) "holds"  (Bool (Set (Var "f")) "is" bbbadV3_VALUED_0()))) ; 
 
theorem :: MESFUNC7: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")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set  ($#k7_numbers :::"ExtREAL"::: ) )  (Bool  "for" (Set (Var "E")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set (Var "S"))  (Bool  "for" (Set (Var "F")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k7_numbers :::"ExtREAL"::: ) )  "st" (Bool (Bool (Set (Set  "("  ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")) ")" )  ($#k9_subset_1 :::"/\"::: )  (Set  "("  ($#k1_relset_1 :::"dom"::: )  (Set (Var "g")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "E"))) & (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Var "F"))) & (Bool (Set (Var "g")) "is" bbbadV3_VALUED_0()) & (Bool (Set (Var "f"))  ($#r1_mesfunc1 :::"is_measurable_on"::: )  (Set (Var "E"))) & (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "f"))) "is"   ($#v5_xxreal_2 :::"real-bounded"::: )  ) & (Bool (Set (Var "g"))  ($#r1_mesfunc5 :::"is_integrable_on"::: )  (Set (Var "M")))) "holds"  (Bool  "("  (Bool (Set (Set  "(" (Set (Var "f"))  ($#k5_mesfunc1 :::"(#)"::: )  (Set (Var "g")) ")" )  ($#k2_partfun1 :::"|"::: )  (Set (Var "E")))  ($#r1_mesfunc5 :::"is_integrable_on"::: )  (Set (Var "M"))) & (Bool  "ex" (Set (Var "c")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  ) "st"  (Bool  "("  (Bool (Set (Var "c"))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k7_supinf_2 :::"inf"::: )  (Set (Var "F")))) & (Bool (Set (Var "c"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k8_supinf_2 :::"sup"::: )  (Set (Var "F")))) & (Bool (Set   ($#k7_mesfunc5 :::"Integral"::: )   "(" (Set (Var "M")) "," (Set  "(" (Set  "(" (Set (Var "f"))  ($#k5_mesfunc1 :::"(#)"::: )  (Set  ($#k10_mesfunc1 :::"|."::: ) (Set (Var "g")) ($#k10_mesfunc1 :::".|"::: ) ) ")" )  ($#k2_partfun1 :::"|"::: )  (Set (Var "E")) ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_measure6 :::"R_EAL"::: )  (Set (Var "c")) ")" )  ($#k1_extreal1 :::"*"::: )  (Set  "("  ($#k7_mesfunc5 :::"Integral"::: )   "(" (Set (Var "M")) "," (Set  "(" (Set  ($#k10_mesfunc1 :::"|."::: ) (Set (Var "g")) ($#k10_mesfunc1 :::".|"::: ) )  ($#k2_partfun1 :::"|"::: )  (Set (Var "E")) ")" ) ")"  ")" )))  ")" ))  ")" ))))))) ; 
 begin  












theorem :: MESFUNC7:18 (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 (Set (Set  ($#k10_mesfunc1 :::"|."::: ) (Set (Var "f")) ($#k10_mesfunc1 :::".|"::: ) )  ($#k2_partfun1 :::"|"::: )  (Set (Var "A")))  ($#r2_relset_1 :::"="::: )  (Set  ($#k10_mesfunc1 :::"|."::: ) (Set  "(" (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "A")) ")" ) ($#k10_mesfunc1 :::".|"::: ) ))))) ; 
 
theorem :: MESFUNC7:19 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set  ($#k7_numbers :::"ExtREAL"::: ) ) "holds"   (Bool  "("  (Bool (Set   ($#k1_relset_1 :::"dom"::: )  (Set  "(" (Set  ($#k10_mesfunc1 :::"|."::: ) (Set (Var "f")) ($#k10_mesfunc1 :::".|"::: ) )  ($#k3_mesfunc1 :::"+"::: )  (Set  ($#k10_mesfunc1 :::"|."::: ) (Set (Var "g")) ($#k10_mesfunc1 :::".|"::: ) ) ")" ))  ($#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  ($#k10_mesfunc1 :::"|."::: ) (Set  "(" (Set (Var "f"))  ($#k3_mesfunc1 :::"+"::: )  (Set (Var "g")) ")" ) ($#k10_mesfunc1 :::".|"::: ) ))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set  ($#k10_mesfunc1 :::"|."::: ) (Set (Var "f")) ($#k10_mesfunc1 :::".|"::: ) )))  ")" ))) ; 
 
theorem :: MESFUNC7:20 (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"::: ) ) "holds"  (Bool (Set (Set  "(" (Set  ($#k10_mesfunc1 :::"|."::: ) (Set (Var "f")) ($#k10_mesfunc1 :::".|"::: ) )  ($#k2_partfun1 :::"|"::: )  (Set  "("  ($#k1_relset_1 :::"dom"::: )  (Set  ($#k10_mesfunc1 :::"|."::: ) (Set  "(" (Set (Var "f"))  ($#k3_mesfunc1 :::"+"::: )  (Set (Var "g")) ")" ) ($#k10_mesfunc1 :::".|"::: ) ) ")" ) ")" )  ($#k3_mesfunc1 :::"+"::: )  (Set  "(" (Set  ($#k10_mesfunc1 :::"|."::: ) (Set (Var "g")) ($#k10_mesfunc1 :::".|"::: ) )  ($#k2_partfun1 :::"|"::: )  (Set  "("  ($#k1_relset_1 :::"dom"::: )  (Set  ($#k10_mesfunc1 :::"|."::: ) (Set  "(" (Set (Var "f"))  ($#k3_mesfunc1 :::"+"::: )  (Set (Var "g")) ")" ) ($#k10_mesfunc1 :::".|"::: ) ) ")" ) ")" ))  ($#r2_relset_1 :::"="::: )  (Set (Set  "(" (Set  ($#k10_mesfunc1 :::"|."::: ) (Set (Var "f")) ($#k10_mesfunc1 :::".|"::: ) )  ($#k3_mesfunc1 :::"+"::: )  (Set  ($#k10_mesfunc1 :::"|."::: ) (Set (Var "g")) ($#k10_mesfunc1 :::".|"::: ) ) ")" )  ($#k2_partfun1 :::"|"::: )  (Set  "("  ($#k1_relset_1 :::"dom"::: )  (Set  ($#k10_mesfunc1 :::"|."::: ) (Set  "(" (Set (Var "f"))  ($#k3_mesfunc1 :::"+"::: )  (Set (Var "g")) ")" ) ($#k10_mesfunc1 :::".|"::: ) ) ")" ))))) ; 
 
theorem :: MESFUNC7: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"::: ) )  (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set  ($#k10_mesfunc1 :::"|."::: ) (Set  "(" (Set (Var "f"))  ($#k3_mesfunc1 :::"+"::: )  (Set (Var "g")) ")" ) ($#k10_mesfunc1 :::".|"::: ) )))) "holds"  (Bool (Set (Set  ($#k10_mesfunc1 :::"|."::: ) (Set  "(" (Set (Var "f"))  ($#k3_mesfunc1 :::"+"::: )  (Set (Var "g")) ")" ) ($#k10_mesfunc1 :::".|"::: ) )  ($#k12_supinf_2 :::"."::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Set  ($#k10_mesfunc1 :::"|."::: ) (Set (Var "f")) ($#k10_mesfunc1 :::".|"::: ) )  ($#k3_mesfunc1 :::"+"::: )  (Set  ($#k10_mesfunc1 :::"|."::: ) (Set (Var "g")) ($#k10_mesfunc1 :::".|"::: ) ) ")" )  ($#k12_supinf_2 :::"."::: )  (Set (Var "x"))))))) ; 
 
theorem :: MESFUNC7:22 (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   ($#k1_relset_1 :::"dom"::: )  (Set  "(" (Set (Var "f"))  ($#k3_mesfunc1 :::"+"::: )  (Set (Var "g")) ")" ))) & (Bool (Set   ($#k7_mesfunc5 :::"Integral"::: )   "(" (Set (Var "M")) "," (Set  "(" (Set  ($#k10_mesfunc1 :::"|."::: ) (Set  "(" (Set (Var "f"))  ($#k3_mesfunc1 :::"+"::: )  (Set (Var "g")) ")" ) ($#k10_mesfunc1 :::".|"::: ) )  ($#k2_partfun1 :::"|"::: )  (Set (Var "E")) ")" ) ")" )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "("  ($#k7_mesfunc5 :::"Integral"::: )   "(" (Set (Var "M")) "," (Set  "(" (Set  ($#k10_mesfunc1 :::"|."::: ) (Set (Var "f")) ($#k10_mesfunc1 :::".|"::: ) )  ($#k2_partfun1 :::"|"::: )  (Set (Var "E")) ")" ) ")"  ")" )  ($#k3_supinf_2 :::"+"::: )  (Set  "("  ($#k7_mesfunc5 :::"Integral"::: )   "(" (Set (Var "M")) "," (Set  "(" (Set  ($#k10_mesfunc1 :::"|."::: ) (Set (Var "g")) ($#k10_mesfunc1 :::".|"::: ) )  ($#k2_partfun1 :::"|"::: )  (Set (Var "E")) ")" ) ")"  ")" )))  ")" )))))) ; 
 
theorem :: MESFUNC7:23 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "A")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k1_mesfunc2 :::"max+"::: )  (Set  "("  ($#k3_mesfunc2 :::"chi"::: )   "(" (Set (Var "A")) "," (Set (Var "X")) ")"  ")" ))  ($#r2_relset_1 :::"="::: )  (Set   ($#k3_mesfunc2 :::"chi"::: )   "(" (Set (Var "A")) "," (Set (Var "X")) ")" )))) ; 
 
theorem :: MESFUNC7:24 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "S")) "being"   ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "M")) "being"   ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "E")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set (Var "S"))  "st" (Bool (Bool (Set (Set (Var "M"))  ($#k12_supinf_2 :::"."::: )  (Set (Var "E")))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k1_supinf_1 :::"+infty"::: )  ))) "holds"  (Bool  "("  (Bool (Set   ($#k3_mesfunc2 :::"chi"::: )   "(" (Set (Var "E")) "," (Set (Var "X")) ")" )  ($#r1_mesfunc5 :::"is_integrable_on"::: )  (Set (Var "M"))) & (Bool (Set   ($#k7_mesfunc5 :::"Integral"::: )   "(" (Set (Var "M")) "," (Set  "("  ($#k3_mesfunc2 :::"chi"::: )   "(" (Set (Var "E")) "," (Set (Var "X")) ")"  ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "M"))  ($#k12_supinf_2 :::"."::: )  (Set (Var "E")))) & (Bool (Set   ($#k7_mesfunc5 :::"Integral"::: )   "(" (Set (Var "M")) "," (Set  "(" (Set  "("  ($#k3_mesfunc2 :::"chi"::: )   "(" (Set (Var "E")) "," (Set (Var "X")) ")"  ")" )  ($#k2_partfun1 :::"|"::: )  (Set (Var "E")) ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "M"))  ($#k12_supinf_2 :::"."::: )  (Set (Var "E"))))  ")" ))))) ; 
 
theorem :: MESFUNC7:25 (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 "E1")) "," (Set (Var "E2")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set (Var "S"))  "st" (Bool (Bool (Set (Set (Var "M"))  ($#k12_supinf_2 :::"."::: )  (Set  "(" (Set (Var "E1"))  ($#k5_prob_1 :::"/\"::: )  (Set (Var "E2")) ")" ))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k1_supinf_1 :::"+infty"::: )  ))) "holds"  (Bool (Set   ($#k7_mesfunc5 :::"Integral"::: )   "(" (Set (Var "M")) "," (Set  "(" (Set  "("  ($#k3_mesfunc2 :::"chi"::: )   "(" (Set (Var "E1")) "," (Set (Var "X")) ")"  ")" )  ($#k2_partfun1 :::"|"::: )  (Set (Var "E2")) ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "M"))  ($#k12_supinf_2 :::"."::: )  (Set  "(" (Set (Var "E1"))  ($#k5_prob_1 :::"/\"::: )  (Set (Var "E2")) ")" ))))))) ; 
 
theorem :: MESFUNC7:26 (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")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set (Var "S"))  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "f"))  ($#r1_mesfunc5 :::"is_integrable_on"::: )  (Set (Var "M"))) & (Bool (Set (Var "E"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Set (Var "M"))  ($#k12_supinf_2 :::"."::: )  (Set (Var "E")))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k1_supinf_1 :::"+infty"::: )  )) & (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "E")))) "holds"  (Bool  "("  (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "f"))  ($#k12_supinf_2 :::"."::: )  (Set (Var "x")))) & (Bool (Set (Set (Var "f"))  ($#k12_supinf_2 :::"."::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b")))  ")" )  ")" )) "holds"  (Bool  "("  (Bool (Set (Set  "("  ($#k1_measure6 :::"R_EAL"::: )  (Set (Var "a")) ")" )  ($#k1_extreal1 :::"*"::: )  (Set  "(" (Set (Var "M"))  ($#k12_supinf_2 :::"."::: )  (Set (Var "E")) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k7_mesfunc5 :::"Integral"::: )   "(" (Set (Var "M")) "," (Set  "(" (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "E")) ")" ) ")" )) & (Bool (Set   ($#k7_mesfunc5 :::"Integral"::: )   "(" (Set (Var "M")) "," (Set  "(" (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "E")) ")" ) ")" )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "("  ($#k1_measure6 :::"R_EAL"::: )  (Set (Var "b")) ")" )  ($#k1_extreal1 :::"*"::: )  (Set  "(" (Set (Var "M"))  ($#k12_supinf_2 :::"."::: )  (Set (Var "E")) ")" )))  ")" ))))))) ;