:: MESFUN10 semantic presentation begin theorem :: MESFUN10:1 (Bool "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "seq1")) ($#k12_supinf_2 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "seq2")) ($#k12_supinf_2 :::"."::: ) (Set (Var "n")))) ")" )) "holds" (Bool (Set ($#k7_supinf_2 :::"inf"::: ) (Set "(" ($#k17_supinf_2 :::"rng"::: ) (Set (Var "seq1")) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k7_supinf_2 :::"inf"::: ) (Set "(" ($#k17_supinf_2 :::"rng"::: ) (Set (Var "seq2")) ")" )))) ; theorem :: MESFUN10:2 (Bool "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "seq1")) ($#k12_supinf_2 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "seq2")) ($#k12_supinf_2 :::"."::: ) (Set (Var "n")))) ")" )) "holds" (Bool "(" (Bool (Set (Set "(" ($#k3_rinfsup2 :::"inferior_realsequence"::: ) (Set (Var "seq1")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "k"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k3_rinfsup2 :::"inferior_realsequence"::: ) (Set (Var "seq2")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "k")))) & (Bool (Set (Set "(" ($#k4_rinfsup2 :::"superior_realsequence"::: ) (Set (Var "seq1")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "k"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k4_rinfsup2 :::"superior_realsequence"::: ) (Set (Var "seq2")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "k")))) ")" ))) ; theorem :: MESFUN10:3 (Bool "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "seq1")) ($#k12_supinf_2 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "seq2")) ($#k12_supinf_2 :::"."::: ) (Set (Var "n")))) ")" )) "holds" (Bool "(" (Bool (Set ($#k6_rinfsup2 :::"lim_inf"::: ) (Set (Var "seq1"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_rinfsup2 :::"lim_inf"::: ) (Set (Var "seq2")))) & (Bool (Set ($#k5_rinfsup2 :::"lim_sup"::: ) (Set (Var "seq1"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k5_rinfsup2 :::"lim_sup"::: ) (Set (Var "seq2")))) ")" )) ; theorem :: MESFUN10:4 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"R_eal":::) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "seq")) ($#k12_supinf_2 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::">="::: ) (Set (Var "a"))) ")" )) "holds" (Bool (Set ($#k2_rinfsup2 :::"inf"::: ) (Set (Var "seq"))) ($#r1_xxreal_0 :::">="::: ) (Set (Var "a"))))) ; theorem :: MESFUN10:5 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"R_eal":::) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "seq")) ($#k12_supinf_2 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "a"))) ")" )) "holds" (Bool (Set ($#k1_rinfsup2 :::"sup"::: ) (Set (Var "seq"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "a"))))) ; theorem :: MESFUN10:6 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ($#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 "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k1_mesfunc8 :::"inf"::: ) (Set "(" (Set (Var "F")) ($#k1_valued_0 :::"^\"::: ) (Set (Var "n")) ")" ) ")" )))) "holds" (Bool (Set (Set "(" ($#k1_mesfunc8 :::"inf"::: ) (Set "(" (Set (Var "F")) ($#k1_valued_0 :::"^\"::: ) (Set (Var "n")) ")" ) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k2_rinfsup2 :::"inf"::: ) (Set "(" (Set "(" (Set (Var "F")) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x")) ")" ) ($#k1_valued_0 :::"^\"::: ) (Set (Var "n")) ")" ))))))) ; theorem :: MESFUN10:7 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (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" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "E")) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n"))) "is" ($#v6_supinf_2 :::"nonnegative"::: ) ) & (Bool (Set (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n"))) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "E"))) ")" ) ")" )) "holds" (Bool "ex" (Set (Var "I")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) "st" (Bool "(" (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "I")) ($#k12_supinf_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k7_mesfunc5 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ")" )) ")" ) & (Bool (Set ($#k7_mesfunc5 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" ($#k5_mesfunc8 :::"lim_inf"::: ) (Set (Var "F")) ")" ) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_rinfsup2 :::"lim_inf"::: ) (Set (Var "I")))) ")" ))))))) ; begin theorem :: MESFUN10:8 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"R_eal":::) "st" (Bool (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set ($#k1_numbers :::"REAL"::: ) ))) "holds" (Bool (Set ($#k8_supinf_2 :::"sup"::: ) (Set "(" (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "r")) ($#k6_domain_1 :::"}"::: ) ) ($#k5_supinf_2 :::"+"::: ) (Set (Var "Y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k8_supinf_2 :::"sup"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "r")) ($#k6_domain_1 :::"}"::: ) ) ")" ) ($#k3_supinf_2 :::"+"::: ) (Set "(" ($#k8_supinf_2 :::"sup"::: ) (Set (Var "Y")) ")" ))))) ; theorem :: MESFUN10:9 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"R_eal":::) "st" (Bool (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set ($#k1_numbers :::"REAL"::: ) ))) "holds" (Bool (Set ($#k7_supinf_2 :::"inf"::: ) (Set "(" (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "r")) ($#k6_domain_1 :::"}"::: ) ) ($#k5_supinf_2 :::"+"::: ) (Set (Var "Y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_supinf_2 :::"inf"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "r")) ($#k6_domain_1 :::"}"::: ) ) ")" ) ($#k3_supinf_2 :::"+"::: ) (Set "(" ($#k7_supinf_2 :::"inf"::: ) (Set (Var "Y")) ")" ))))) ; theorem :: MESFUN10:10 (Bool "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"R_eal":::) "st" (Bool (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set ($#k1_numbers :::"REAL"::: ) )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "seq1")) ($#k12_supinf_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k3_supinf_2 :::"+"::: ) (Set "(" (Set (Var "seq2")) ($#k12_supinf_2 :::"."::: ) (Set (Var "n")) ")" ))) ")" )) "holds" (Bool "(" (Bool (Set ($#k6_rinfsup2 :::"lim_inf"::: ) (Set (Var "seq1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k3_supinf_2 :::"+"::: ) (Set "(" ($#k6_rinfsup2 :::"lim_inf"::: ) (Set (Var "seq2")) ")" ))) & (Bool (Set ($#k5_rinfsup2 :::"lim_sup"::: ) (Set (Var "seq1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k3_supinf_2 :::"+"::: ) (Set "(" ($#k5_rinfsup2 :::"lim_sup"::: ) (Set (Var "seq2")) ")" ))) ")" ))) ; theorem :: MESFUN10:11 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F1")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F2")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ))) & (Bool (Set (Var "F1")) "is" ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ) & (Bool (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set ($#k1_supinf_1 :::"+infty"::: ) ) ($#k6_domain_1 :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set ($#k2_supinf_1 :::"-infty"::: ) ) ($#k6_domain_1 :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "F1")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n"))) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "f")) ($#k3_mesfunc1 :::"+"::: ) (Set "(" (Set (Var "F2")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ))) ")" )) "holds" (Bool "(" (Bool (Set ($#k5_mesfunc8 :::"lim_inf"::: ) (Set (Var "F1"))) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "f")) ($#k3_mesfunc1 :::"+"::: ) (Set "(" ($#k5_mesfunc8 :::"lim_inf"::: ) (Set (Var "F2")) ")" ))) & (Bool (Set ($#k6_mesfunc8 :::"lim_sup"::: ) (Set (Var "F1"))) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "f")) ($#k3_mesfunc1 :::"+"::: ) (Set "(" ($#k6_mesfunc8 :::"lim_sup"::: ) (Set (Var "F2")) ")" ))) ")" )))) ; theorem :: MESFUN10: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 "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")) ($#k4_mesfunc1 :::"-"::: ) (Set (Var "g"))) ($#r1_mesfunc5 :::"is_integrable_on"::: ) (Set (Var "M"))))))) ; theorem :: MESFUN10:13 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "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" ($#m1_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")) ($#k4_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 "(" ($#k7_mesfunc1 :::"-"::: ) (Set (Var "g")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set (Var "E")) ")" ) ")" ")" ))) ")" )))))) ; theorem :: MESFUN10:14 (Bool "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "seq1")) ($#k12_supinf_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k2_supinf_2 :::"-"::: ) (Set "(" (Set (Var "seq2")) ($#k12_supinf_2 :::"."::: ) (Set (Var "n")) ")" ))) ")" )) "holds" (Bool "(" (Bool (Set ($#k6_rinfsup2 :::"lim_inf"::: ) (Set (Var "seq2"))) ($#r1_hidden :::"="::: ) (Set ($#k2_supinf_2 :::"-"::: ) (Set "(" ($#k5_rinfsup2 :::"lim_sup"::: ) (Set (Var "seq1")) ")" ))) & (Bool (Set ($#k5_rinfsup2 :::"lim_sup"::: ) (Set (Var "seq2"))) ($#r1_hidden :::"="::: ) (Set ($#k2_supinf_2 :::"-"::: ) (Set "(" ($#k6_rinfsup2 :::"lim_inf"::: ) (Set (Var "seq1")) ")" ))) ")" )) ; theorem :: MESFUN10:15 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F1")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F2")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ))) & (Bool (Set (Var "F1")) "is" ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "F1")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n"))) ($#r2_relset_1 :::"="::: ) (Set ($#k7_mesfunc1 :::"-"::: ) (Set "(" (Set (Var "F2")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ))) ")" )) "holds" (Bool "(" (Bool (Set ($#k5_mesfunc8 :::"lim_inf"::: ) (Set (Var "F1"))) ($#r2_relset_1 :::"="::: ) (Set ($#k7_mesfunc1 :::"-"::: ) (Set "(" ($#k6_mesfunc8 :::"lim_sup"::: ) (Set (Var "F2")) ")" ))) & (Bool (Set ($#k6_mesfunc8 :::"lim_sup"::: ) (Set (Var "F1"))) ($#r2_relset_1 :::"="::: ) (Set ($#k7_mesfunc1 :::"-"::: ) (Set "(" ($#k5_mesfunc8 :::"lim_inf"::: ) (Set (Var "F2")) ")" ))) ")" ))) ; theorem :: MESFUN10:16 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (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" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "S")) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool (Set (Var "E")) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ))) & (Bool (Set (Var "E")) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "P")))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n"))) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "E"))) ")" ) & (Bool (Set (Var "P")) ($#r1_mesfunc5 :::"is_integrable_on"::: ) (Set (Var "M"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "E")))) "holds" (Bool (Set (Set ($#k10_mesfunc1 :::"|."::: ) (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ($#k10_mesfunc1 :::".|"::: ) ) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "P")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))))) ")" )) "holds" (Bool "(" (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k10_mesfunc1 :::"|."::: ) (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ($#k10_mesfunc1 :::".|"::: ) ) ($#r1_mesfunc5 :::"is_integrable_on"::: ) (Set (Var "M"))) ")" ) & (Bool (Set ($#k10_mesfunc1 :::"|."::: ) (Set "(" ($#k5_mesfunc8 :::"lim_inf"::: ) (Set (Var "F")) ")" ) ($#k10_mesfunc1 :::".|"::: ) ) ($#r1_mesfunc5 :::"is_integrable_on"::: ) (Set (Var "M"))) & (Bool (Set ($#k10_mesfunc1 :::"|."::: ) (Set "(" ($#k6_mesfunc8 :::"lim_sup"::: ) (Set (Var "F")) ")" ) ($#k10_mesfunc1 :::".|"::: ) ) ($#r1_mesfunc5 :::"is_integrable_on"::: ) (Set (Var "M"))) ")" ))))))) ; theorem :: MESFUN10:17 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (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" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "S")) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool (Set (Var "E")) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ))) & (Bool (Set (Var "E")) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "P")))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n"))) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "E"))) ")" ) & (Bool (Set (Var "P")) ($#r1_mesfunc5 :::"is_integrable_on"::: ) (Set (Var "M"))) & (Bool (Set (Var "P")) "is" ($#v6_supinf_2 :::"nonnegative"::: ) ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "E")))) "holds" (Bool (Set (Set ($#k10_mesfunc1 :::"|."::: ) (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ($#k10_mesfunc1 :::".|"::: ) ) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "P")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))))) ")" )) "holds" (Bool "ex" (Set (Var "I")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) "st" (Bool "(" (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "I")) ($#k12_supinf_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k7_mesfunc5 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ")" )) ")" ) & (Bool (Set ($#k6_rinfsup2 :::"lim_inf"::: ) (Set (Var "I"))) ($#r1_xxreal_0 :::">="::: ) (Set ($#k7_mesfunc5 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" ($#k5_mesfunc8 :::"lim_inf"::: ) (Set (Var "F")) ")" ) ")" )) & (Bool (Set ($#k5_rinfsup2 :::"lim_sup"::: ) (Set (Var "I"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k7_mesfunc5 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" ($#k6_mesfunc8 :::"lim_sup"::: ) (Set (Var "F")) ")" ) ")" )) & "(" (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 (Var "E")))) "holds" (Bool (Set (Set (Var "F")) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x"))) "is" ($#v10_mesfunc5 :::"convergent"::: ) ) ")" )) "implies" (Bool "(" (Bool (Set (Var "I")) "is" ($#v10_mesfunc5 :::"convergent"::: ) ) & (Bool (Set ($#k2_mesfunc5 :::"lim"::: ) (Set (Var "I"))) ($#r1_hidden :::"="::: ) (Set ($#k7_mesfunc5 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" ($#k7_mesfunc8 :::"lim"::: ) (Set (Var "F")) ")" ) ")" )) ")" ) ")" ")" )))))))) ; theorem :: MESFUN10:18 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (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" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "E")) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n"))) "is" ($#v6_supinf_2 :::"nonnegative"::: ) ) & (Bool (Set (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n"))) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "E"))) ")" ) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "E"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m")))) "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 (Set ($#k7_mesfunc5 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k2_partfun1 :::"|"::: ) (Set (Var "E")) ")" ) ")" ) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_supinf_1 :::"+infty"::: ) ))) "holds" (Bool "ex" (Set (Var "I")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) "st" (Bool "(" (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "I")) ($#k12_supinf_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k7_mesfunc5 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ")" )) ")" ) & (Bool (Set (Var "I")) "is" ($#v10_mesfunc5 :::"convergent"::: ) ) & (Bool (Set ($#k2_mesfunc5 :::"lim"::: ) (Set (Var "I"))) ($#r1_hidden :::"="::: ) (Set ($#k7_mesfunc5 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" ($#k7_mesfunc8 :::"lim"::: ) (Set (Var "F")) ")" ) ")" )) ")" ))))))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Const "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ); attr "F" is :::"uniformly_bounded"::: means :: MESFUN10:def 1 (Bool "ex" (Set (Var "K")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" "F" ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )))) "holds" (Bool (Set ($#k3_extreal1 :::"|."::: ) (Set "(" (Set "(" "F" ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k3_extreal1 :::".|"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "K")))))); end; :: deftheorem defines :::"uniformly_bounded"::: MESFUN10:def 1 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v1_mesfun10 :::"uniformly_bounded"::: ) ) "iff" (Bool "ex" (Set (Var "K")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (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_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )))) "holds" (Bool (Set ($#k3_extreal1 :::"|."::: ) (Set "(" (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k3_extreal1 :::".|"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "K")))))) ")" ))); theorem :: MESFUN10:19 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (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" ($#m1_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"::: ) )) & (Bool (Set (Var "E")) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n"))) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "E"))) ")" ) & (Bool (Set (Var "F")) "is" ($#v1_mesfun10 :::"uniformly_bounded"::: ) ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "E")))) "holds" (Bool (Set (Set (Var "F")) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x"))) "is" ($#v10_mesfunc5 :::"convergent"::: ) ) ")" )) "holds" (Bool "(" (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n"))) ($#r1_mesfunc5 :::"is_integrable_on"::: ) (Set (Var "M"))) ")" ) & (Bool (Set ($#k7_mesfunc8 :::"lim"::: ) (Set (Var "F"))) ($#r1_mesfunc5 :::"is_integrable_on"::: ) (Set (Var "M"))) & (Bool "ex" (Set (Var "I")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) "st" (Bool "(" (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "I")) ($#k12_supinf_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k7_mesfunc5 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ")" )) ")" ) & (Bool (Set (Var "I")) "is" ($#v10_mesfunc5 :::"convergent"::: ) ) & (Bool (Set ($#k2_mesfunc5 :::"lim"::: ) (Set (Var "I"))) ($#r1_hidden :::"="::: ) (Set ($#k7_mesfunc5 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" ($#k7_mesfunc8 :::"lim"::: ) (Set (Var "F")) ")" ) ")" )) ")" )) ")" )))))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Const "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ); let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ); pred "F" :::"is_uniformly_convergent_to"::: "f" means :: MESFUN10:def 2 (Bool "(" (Bool "F" "is" ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ) & (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" "F" ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) "f")) & (Bool "(" "for" (Set (Var "e")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "e")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "ex" (Set (Var "N")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Set (Var "N"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" "F" ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )))) "holds" (Bool (Set ($#k3_extreal1 :::"|."::: ) (Set "(" (Set "(" (Set "(" "F" ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k4_supinf_2 :::"-"::: ) (Set "(" "f" ($#k12_supinf_2 :::"."::: ) (Set (Var "x")) ")" ) ")" ) ($#k3_extreal1 :::".|"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "e")))))) ")" ) ")" ); end; :: deftheorem defines :::"is_uniformly_convergent_to"::: MESFUN10:def 2 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (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_mesfun10 :::"is_uniformly_convergent_to"::: ) (Set (Var "f"))) "iff" (Bool "(" (Bool (Set (Var "F")) "is" ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ) & (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool "(" "for" (Set (Var "e")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "e")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "ex" (Set (Var "N")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Set (Var "N"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )))) "holds" (Bool (Set ($#k3_extreal1 :::"|."::: ) (Set "(" (Set "(" (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k4_supinf_2 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x")) ")" ) ")" ) ($#k3_extreal1 :::".|"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "e")))))) ")" ) ")" ) ")" )))); theorem :: MESFUN10:20 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F1")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool (Set (Var "F1")) ($#r1_mesfun10 :::"is_uniformly_convergent_to"::: ) (Set (Var "f")))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F1")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )))) "holds" (Bool "(" (Bool (Set (Set (Var "F1")) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x"))) "is" ($#v10_mesfunc5 :::"convergent"::: ) ) & (Bool (Set ($#k2_mesfunc5 :::"lim"::: ) (Set "(" (Set (Var "F1")) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x")))) ")" ))))) ; theorem :: MESFUN10:21 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (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" ($#m1_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 (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set (Var "E"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_supinf_1 :::"+infty"::: ) )) & (Bool (Set (Var "E")) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n"))) ($#r1_mesfunc5 :::"is_integrable_on"::: ) (Set (Var "M"))) ")" ) & (Bool (Set (Var "F")) ($#r1_mesfun10 :::"is_uniformly_convergent_to"::: ) (Set (Var "f")))) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_mesfunc5 :::"is_integrable_on"::: ) (Set (Var "M"))) & (Bool "ex" (Set (Var "I")) "being" ($#m1_subset_1 :::"ExtREAL_sequence":::) "st" (Bool "(" (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "I")) ($#k12_supinf_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k7_mesfunc5 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ")" )) ")" ) & (Bool (Set (Var "I")) "is" ($#v10_mesfunc5 :::"convergent"::: ) ) & (Bool (Set ($#k2_mesfunc5 :::"lim"::: ) (Set (Var "I"))) ($#r1_hidden :::"="::: ) (Set ($#k7_mesfunc5 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set (Var "f")) ")" )) ")" )) ")" ))))))) ;