:: MESFUNC4  semantic presentation begin  
theorem :: MESFUNC4:1 (Bool  "for" (Set (Var "F")) "," (Set (Var "G")) "," (Set (Var "H")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k7_numbers :::"ExtREAL"::: )  )  "st" (Bool (Bool  "("   "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "F"))))) "holds"  (Bool (Set   ($#k1_supinf_2 :::"0."::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "F"))  ($#k12_supinf_2 :::"."::: )  (Set (Var "i"))))  ")" ) & (Bool  "("   "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "G"))))) "holds"  (Bool (Set   ($#k1_supinf_2 :::"0."::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "G"))  ($#k12_supinf_2 :::"."::: )  (Set (Var "i"))))  ")" ) & (Bool (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "F")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "G")))) & (Bool (Set (Var "H"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "F"))  ($#k3_mesfunc1 :::"+"::: )  (Set (Var "G"))))) "holds"  (Bool (Set   ($#k4_extreal1 :::"Sum"::: )  (Set (Var "H")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_extreal1 :::"Sum"::: )  (Set (Var "F")) ")" )  ($#k3_supinf_2 :::"+"::: )  (Set  "("  ($#k4_extreal1 :::"Sum"::: )  (Set (Var "G")) ")" )))) ; 
 
theorem :: MESFUNC4:2 (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 "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set  ($#k7_numbers :::"ExtREAL"::: ) )  (Bool  "for" (Set (Var "F")) "being"   ($#m2_finseq_1 :::"Finite_Sep_Sequence":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "a")) "," (Set (Var "x")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k7_numbers :::"ExtREAL"::: )  )  "st" (Bool (Bool (Set (Var "f"))  ($#r1_mesfunc2 :::"is_simple_func_in"::: )  (Set (Var "S"))) & (Bool (Set   ($#k9_xtuple_0 :::"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   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f"))))) "holds"  (Bool (Set   ($#k1_supinf_2 :::"0."::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "f"))  ($#k12_supinf_2 :::"."::: )  (Set (Var "x"))))  ")" ) & (Bool (Set (Var "F")) "," (Set (Var "a"))  ($#r1_mesfunc3 :::"are_Re-presentation_of"::: )  (Set (Var "f"))) & (Bool (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "F")))) & (Bool  "("   "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "x"))))) "holds"  (Bool (Set (Set (Var "x"))  ($#k12_supinf_2 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k12_supinf_2 :::"."::: )  (Set (Var "i")) ")" )  ($#k1_extreal1 :::"*"::: )  (Set  "(" (Set  "(" (Set (Var "M"))  ($#k1_partfun1 :::"*"::: )  (Set (Var "F")) ")" )  ($#k12_supinf_2 :::"."::: )  (Set (Var "i")) ")" )))  ")" ) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "F")))  ($#r1_hidden :::"="::: )  (Set (Var "n")))) "holds"  (Bool (Set   ($#k1_mesfunc3 :::"integral"::: )   "(" (Set (Var "X")) "," (Set (Var "S")) "," (Set (Var "M")) "," (Set (Var "f")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k4_extreal1 :::"Sum"::: )  (Set (Var "x"))))))))))) ; 
 
theorem :: MESFUNC4: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 "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set  ($#k7_numbers :::"ExtREAL"::: ) )  (Bool  "for" (Set (Var "M")) "being"   ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "F")) "being"   ($#m2_finseq_1 :::"Finite_Sep_Sequence":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "a")) "," (Set (Var "x")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k7_numbers :::"ExtREAL"::: )  )  "st" (Bool (Bool (Set (Var "f"))  ($#r1_mesfunc2 :::"is_simple_func_in"::: )  (Set (Var "S"))) & (Bool (Set   ($#k9_xtuple_0 :::"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   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f"))))) "holds"  (Bool (Set   ($#k1_supinf_2 :::"0."::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "f"))  ($#k12_supinf_2 :::"."::: )  (Set (Var "x"))))  ")" ) & (Bool (Set (Var "F")) "," (Set (Var "a"))  ($#r1_mesfunc3 :::"are_Re-presentation_of"::: )  (Set (Var "f"))) & (Bool (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "F")))) & (Bool  "("   "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_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"))  ($#k1_partfun1 :::"*"::: )  (Set (Var "F")) ")" )  ($#k12_supinf_2 :::"."::: )  (Set (Var "n")) ")" )))  ")" )) "holds"  (Bool (Set   ($#k1_mesfunc3 :::"integral"::: )   "(" (Set (Var "X")) "," (Set (Var "S")) "," (Set (Var "M")) "," (Set (Var "f")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k4_extreal1 :::"Sum"::: )  (Set (Var "x")))))))))) ; 
 
theorem :: MESFUNC4: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 "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set  ($#k7_numbers :::"ExtREAL"::: ) )  (Bool  "for" (Set (Var "M")) "being"   ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S"))  "st" (Bool (Bool (Set (Var "f"))  ($#r1_mesfunc2 :::"is_simple_func_in"::: )  (Set (Var "S"))) & (Bool (Set   ($#k9_xtuple_0 :::"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   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f"))))) "holds"  (Bool (Set   ($#k1_supinf_2 :::"0."::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "f"))  ($#k12_supinf_2 :::"."::: )  (Set (Var "x"))))  ")" )) "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   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "F")))) & (Bool  "("   "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_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"))  ($#k1_partfun1 :::"*"::: )  (Set (Var "F")) ")" )  ($#k12_supinf_2 :::"."::: )  (Set (Var "n")) ")" )))  ")" ) & (Bool (Set   ($#k1_mesfunc3 :::"integral"::: )   "(" (Set (Var "X")) "," (Set (Var "S")) "," (Set (Var "M")) "," (Set (Var "f")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k4_extreal1 :::"Sum"::: )  (Set (Var "x"))))  ")" ))))))) ; 
 
theorem :: MESFUNC4:5 (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   ($#k9_xtuple_0 :::"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   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f"))))) "holds"  (Bool (Set   ($#k1_supinf_2 :::"0."::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "f"))  ($#k12_supinf_2 :::"."::: )  (Set (Var "x"))))  ")" ) & (Bool (Set (Var "g"))  ($#r1_mesfunc2 :::"is_simple_func_in"::: )  (Set (Var "S"))) & (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "g")))  ($#r1_hidden :::"="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f")))) & (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "g"))))) "holds"  (Bool (Set   ($#k1_supinf_2 :::"0."::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "g"))  ($#k12_supinf_2 :::"."::: )  (Set (Var "x"))))  ")" )) "holds"  (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k3_mesfunc1 :::"+"::: )  (Set (Var "g")))  ($#r1_mesfunc2 :::"is_simple_func_in"::: )  (Set (Var "S"))) & (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" (Set (Var "f"))  ($#k3_mesfunc1 :::"+"::: )  (Set (Var "g")) ")" ))  ($#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   ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" (Set (Var "f"))  ($#k3_mesfunc1 :::"+"::: )  (Set (Var "g")) ")" )))) "holds"  (Bool (Set   ($#k1_supinf_2 :::"0."::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Set (Var "f"))  ($#k3_mesfunc1 :::"+"::: )  (Set (Var "g")) ")" )  ($#k12_supinf_2 :::"."::: )  (Set (Var "x"))))  ")" ) & (Bool (Set   ($#k1_mesfunc3 :::"integral"::: )   "(" (Set (Var "X")) "," (Set (Var "S")) "," (Set (Var "M")) "," (Set  "(" (Set (Var "f"))  ($#k3_mesfunc1 :::"+"::: )  (Set (Var "g")) ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_mesfunc3 :::"integral"::: )   "(" (Set (Var "X")) "," (Set (Var "S")) "," (Set (Var "M")) "," (Set (Var "f")) ")"  ")" )  ($#k3_supinf_2 :::"+"::: )  (Set  "("  ($#k1_mesfunc3 :::"integral"::: )   "(" (Set (Var "X")) "," (Set (Var "S")) "," (Set (Var "M")) "," (Set (Var "g")) ")"  ")" )))  ")" ))))) ; 
 
theorem :: MESFUNC4:6 (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 "c")) "being"   ($#m1_subset_1 :::"R_eal":::)  "st" (Bool (Bool (Set (Var "f"))  ($#r1_mesfunc2 :::"is_simple_func_in"::: )  (Set (Var "S"))) & (Bool (Set   ($#k9_xtuple_0 :::"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   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f"))))) "holds"  (Bool (Set   ($#k1_supinf_2 :::"0."::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "f"))  ($#k12_supinf_2 :::"."::: )  (Set (Var "x"))))  ")" ) & (Bool (Set   ($#k1_supinf_2 :::"0."::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "c"))) & (Bool (Set (Var "c"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k1_supinf_1 :::"+infty"::: )  )) & (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "g")))  ($#r1_hidden :::"="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f")))) & (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "g"))))) "holds"  (Bool (Set (Set (Var "g"))  ($#k12_supinf_2 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "c"))  ($#k1_extreal1 :::"*"::: )  (Set  "(" (Set (Var "f"))  ($#k12_supinf_2 :::"."::: )  (Set (Var "x")) ")" )))  ")" )) "holds"  (Bool (Set   ($#k1_mesfunc3 :::"integral"::: )   "(" (Set (Var "X")) "," (Set (Var "S")) "," (Set (Var "M")) "," (Set (Var "g")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "c"))  ($#k1_extreal1 :::"*"::: )  (Set  "("  ($#k1_mesfunc3 :::"integral"::: )   "(" (Set (Var "X")) "," (Set (Var "S")) "," (Set (Var "M")) "," (Set (Var "f")) ")"  ")" )))))))) ;