:: MESFUNC3 semantic presentation begin theorem :: MESFUNC3:1 (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" ) "," (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "m")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")))) & (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 "p"))))) "holds" (Bool "ex" (Set (Var "r")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "m")))) & (Bool (Set (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set (Var "r")))) & (Bool "(" "for" (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "r"))))) "holds" (Bool (Set (Set (Var "r")) ($#k1_seq_1 :::"."::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_seq_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ))) ")" ) ")" )) ")" ) & (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "m")))) & (Bool "(" "for" (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "q"))))) "holds" (Bool "ex" (Set (Var "s")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")))) & (Bool (Set (Set (Var "q")) ($#k1_seq_1 :::"."::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set (Var "s")))) & (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 "s"))))) "holds" (Bool (Set (Set (Var "s")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_seq_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ))) ")" ) ")" )) ")" )) "holds" (Bool (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set (Var "q"))))))) ; theorem :: MESFUNC3:2 (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set (Var "f")))) "holds" (Bool (Set ($#k4_extreal1 :::"Sum"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set (Var "f")))))) ; theorem :: MESFUNC3: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"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r1_mesfunc2 :::"is_simple_func_in"::: ) (Set (Var "S")))) "holds" (Bool "ex" (Set (Var "F")) "being" ($#m2_finseq_1 :::"Finite_Sep_Sequence":::) "of" (Set (Var "S"))(Bool "ex" (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 ($#k3_tarski :::"union"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "F")) ")" ))) & (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "a")))) & (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 "F"))))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool (Set (Set (Var "f")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k12_supinf_2 :::"."::: ) (Set (Var "n"))))) ")" ) & (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 "ex" (Set (Var "ax")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool "(" (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "ax"))) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "a")))) & (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 "ax"))))) "holds" (Bool (Set (Set (Var "ax")) ($#k12_supinf_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k12_supinf_2 :::"."::: ) (Set (Var "n")) ")" ) ($#k1_extreal1 :::"*"::: ) (Set "(" (Set "(" ($#k3_mesfunc2 :::"chi"::: ) "(" (Set "(" (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) "," (Set (Var "X")) ")" ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "x")) ")" ))) ")" ) ")" )) ")" ) ")" )))))) ; theorem :: MESFUNC3:4 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v1_prob_2 :::"disjoint_valued"::: ) ) "iff" (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "F")))) & (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "F")))) & (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) (Set (Var "j")))) "holds" (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_xboole_0 :::"misses"::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))))) ")" ))) ; theorem :: MESFUNC3:5 (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"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"Finite_Sep_Sequence":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "S")) "st" (Bool (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "G"))) ($#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 "G"))))) "holds" (Bool (Set (Set (Var "G")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k3_xboole_0 :::"/\"::: ) (Set "(" (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ))) ")" )) "holds" (Bool (Set (Var "G")) "is" ($#m2_finseq_1 :::"Finite_Sep_Sequence":::) "of" (Set (Var "S")))))))) ; theorem :: MESFUNC3:6 (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"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "G"))) ($#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 "G"))))) "holds" (Bool (Set (Set (Var "G")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k3_xboole_0 :::"/\"::: ) (Set "(" (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ))) ")" )) "holds" (Bool (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k3_tarski :::"union"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "F")) ")" ) ")" )))))) ; theorem :: MESFUNC3:7 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "X")) (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 "(" (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_tarski :::"c="::: ) (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "F")) ")" ))) & (Bool (Set (Set "(" (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k3_tarski :::"union"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "F")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) ")" )))) ; theorem :: MESFUNC3:8 (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" ($#m2_finseq_1 :::"Finite_Sep_Sequence":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" (Set (Var "M")) ($#k4_finseqop :::"*"::: ) (Set (Var "F")) ")" ))))))) ; theorem :: MESFUNC3:9 (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" ($#m2_finseq_1 :::"Finite_Sep_Sequence":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set "(" ($#k3_tarski :::"union"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "F")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_extreal1 :::"Sum"::: ) (Set "(" (Set (Var "M")) ($#k4_finseqop :::"*"::: ) (Set (Var "F")) ")" ))))))) ; theorem :: MESFUNC3:10 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"R_eal":::) "st" (Bool (Bool "(" (Bool (Set (Var "a")) "is" ($#v1_xreal_0 :::"real"::: ) ) "or" (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 (Set (Var "F")) ($#k12_supinf_2 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_supinf_2 :::"0."::: ) ))) "or" (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 (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "G")))) & (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 (Set (Var "G")) ($#k12_supinf_2 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_extreal1 :::"*"::: ) (Set "(" (Set (Var "F")) ($#k12_supinf_2 :::"."::: ) (Set (Var "i")) ")" ))) ")" )) "holds" (Bool (Set ($#k4_extreal1 :::"Sum"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_extreal1 :::"*"::: ) (Set "(" ($#k4_extreal1 :::"Sum"::: ) (Set (Var "F")) ")" ))))) ; theorem :: MESFUNC3:11 (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Var "F")) "is" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ))) ; 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 "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ); let "F" be ($#m2_finseq_1 :::"Finite_Sep_Sequence":::) "of" (Set (Const "S")); let "a" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ); pred "F" "," "a" :::"are_Re-presentation_of"::: "f" means :: MESFUNC3:def 1 (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) "f") ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) "F" ")" ))) & (Bool (Set ($#k4_finseq_1 :::"dom"::: ) "F") ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "a")) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "F"))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "F" ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool (Set "f" ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set "a" ($#k12_supinf_2 :::"."::: ) (Set (Var "n"))))) ")" ) ")" ); end; :: deftheorem defines :::"are_Re-presentation_of"::: MESFUNC3:def 1 : (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 "F")) "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"::: ) ) "holds" (Bool "(" (Bool (Set (Var "F")) "," (Set (Var "a")) ($#r1_mesfunc3 :::"are_Re-presentation_of"::: ) (Set (Var "f"))) "iff" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "F")) ")" ))) & (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "a")))) & (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 "F"))))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool (Set (Set (Var "f")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k12_supinf_2 :::"."::: ) (Set (Var "n"))))) ")" ) ")" ) ")" )))))); theorem :: MESFUNC3:12 (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 "ex" (Set (Var "F")) "being" ($#m2_finseq_1 :::"Finite_Sep_Sequence":::) "of" (Set (Var "S"))(Bool "ex" (Set (Var "a")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Set (Var "F")) "," (Set (Var "a")) ($#r1_mesfunc3 :::"are_Re-presentation_of"::: ) (Set (Var "f")))))))) ; theorem :: MESFUNC3:13 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"Finite_Sep_Sequence":::) "of" (Set (Var "S")) (Bool "ex" (Set (Var "G")) "being" ($#m2_finseq_1 :::"Finite_Sep_Sequence":::) "of" (Set (Var "S")) "st" (Bool "(" (Bool (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "G")) ")" ))) & (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 "G"))))) "holds" (Bool "(" (Bool (Set (Set (Var "G")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool "ex" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "(" (Bool (Set (Var "m")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "F")))) & (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) ")" )) ")" ) ")" ) ")" ))))) ; theorem :: MESFUNC3: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"))) & (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 ($#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")) "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 ($#k1_supinf_2 :::"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 ($#k4_finseq_1 :::"dom"::: ) (Set (Var "a"))))) "holds" (Bool "(" (Bool (Set ($#k1_supinf_2 :::"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"::: ) )) ")" ) ")" ) ")" )))))) ; theorem :: MESFUNC3: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")) "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")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "F")) "," (Set (Var "a")) ($#r1_mesfunc3 :::"are_Re-presentation_of"::: ) (Set (Var "f"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool "ex" (Set (Var "ax")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool "(" (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "ax"))) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "a")))) & (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 "ax"))))) "holds" (Bool (Set (Set (Var "ax")) ($#k12_supinf_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k12_supinf_2 :::"."::: ) (Set (Var "n")) ")" ) ($#k1_extreal1 :::"*"::: ) (Set "(" (Set "(" ($#k3_mesfunc2 :::"chi"::: ) "(" (Set "(" (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) "," (Set (Var "X")) ")" ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "x")) ")" ))) ")" ) & (Bool (Set (Set (Var "f")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_extreal1 :::"Sum"::: ) (Set (Var "ax")))) ")" )))))))) ; theorem :: MESFUNC3:16 (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Var "q")))) "holds" (Bool (Set ($#k4_extreal1 :::"Sum"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set (Var "q")))))) ; theorem :: MESFUNC3:17 (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool (Bool "not" (Set ($#k2_supinf_1 :::"-infty"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "p"))))) & (Bool (Set ($#k1_supinf_1 :::"+infty"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "p"))))) "holds" (Bool (Set ($#k4_extreal1 :::"Sum"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k1_supinf_1 :::"+infty"::: ) ))) ; 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 (Bool "(" (Bool (Set (Const "f")) ($#r1_mesfunc2 :::"is_simple_func_in"::: ) (Set (Const "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 (Const "f"))))) "holds" (Bool (Set ($#k1_supinf_2 :::"0."::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Const "f")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x")))) ")" ) ")" ) ; func :::"integral"::: "(" "X" "," "S" "," "M" "," "f" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) means :: MESFUNC3:def 2 (Bool "ex" (Set (Var "F")) "being" ($#m2_finseq_1 :::"Finite_Sep_Sequence":::) "of" "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"::: ) "f") & (Bool (Set (Set (Var "a")) ($#k12_supinf_2 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k1_supinf_2 :::"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 ($#k4_finseq_1 :::"dom"::: ) (Set (Var "a"))))) "holds" (Bool "(" (Bool (Set ($#k1_supinf_2 :::"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 ($#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 "(" "M" ($#k4_finseqop :::"*"::: ) (Set (Var "F")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "n")) ")" ))) ")" ) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k4_extreal1 :::"Sum"::: ) (Set (Var "x")))) ")" ))); end; :: deftheorem defines :::"integral"::: MESFUNC3:def 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 "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 "(" "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 ($#k1_supinf_2 :::"0."::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "f")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x")))) ")" )) "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 ($#k1_mesfunc3 :::"integral"::: ) "(" (Set (Var "X")) "," (Set (Var "S")) "," (Set (Var "M")) "," (Set (Var "f")) ")" )) "iff" (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 ($#k1_supinf_2 :::"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 ($#k4_finseq_1 :::"dom"::: ) (Set (Var "a"))))) "holds" (Bool "(" (Bool (Set ($#k1_supinf_2 :::"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 ($#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")) ($#k4_finseqop :::"*"::: ) (Set (Var "F")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "n")) ")" ))) ")" ) & (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k4_extreal1 :::"Sum"::: ) (Set (Var "x")))) ")" ))) ")" )))))); begin theorem :: MESFUNC3:18 (Bool "for" (Set (Var "a")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "p")) "," (Set (Var "N")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool (Set (Var "N")) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "a")))) & (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 "a"))))) "holds" (Bool (Set (Set (Var "a")) ($#k12_supinf_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Var "p"))) ")" )) "holds" (Bool (Set ($#k4_extreal1 :::"Sum"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "N")) ($#k1_extreal1 :::"*"::: ) (Set (Var "p")))))) ;