:: MESFUN9C semantic presentation begin definitionlet "X", "Y" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Const "X")) "," (Set (Const "Y")); let "D" be ($#m1_hidden :::"set"::: ) ; func "F" :::"||"::: "D" -> ($#m1_subset_1 :::"Functional_Sequence":::) "of" "X" "," "Y" means :: MESFUN9C:def 1 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set it ($#k4_mesfunc5 :::"."::: ) (Set (Var "n"))) ($#r2_relset_1 :::"="::: ) (Set (Set "(" "F" ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ($#k2_partfun1 :::"|"::: ) "D"))); end; :: deftheorem defines :::"||"::: MESFUN9C:def 1 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_mesfun9c :::"||"::: ) (Set (Var "D")))) "iff" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "b5")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n"))) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set (Var "D"))))) ")" ))))); theorem :: MESFUN9C:1 (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 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) & (Bool (Set (Set (Var "F")) ($#k10_seqfunc :::"#"::: ) (Set (Var "x"))) "is" ($#v2_comseq_2 :::"convergent"::: ) )) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k1_mesfun9c :::"||"::: ) (Set (Var "D")) ")" ) ($#k10_seqfunc :::"#"::: ) (Set (Var "x"))) "is" ($#v2_comseq_2 :::"convergent"::: ) ))))) ; theorem :: MESFUN9C:2 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_mesfunc8 :::"with_the_same_dom"::: ) )) "holds" (Bool (Set (Set (Var "F")) ($#k1_mesfun9c :::"||"::: ) (Set (Var "D"))) "is" ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ))) ; theorem :: MESFUN9C:3 (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 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "D")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ))) & (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 "D")))) "holds" (Bool (Set (Set (Var "F")) ($#k10_seqfunc :::"#"::: ) (Set (Var "x"))) "is" ($#v2_comseq_2 :::"convergent"::: ) ) ")" )) "holds" (Bool (Set (Set "(" ($#k8_mesfun7c :::"lim"::: ) (Set (Var "F")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set (Var "D"))) ($#r2_relset_1 :::"="::: ) (Set ($#k8_mesfun7c :::"lim"::: ) (Set "(" (Set (Var "F")) ($#k1_mesfun9c :::"||"::: ) (Set (Var "D")) ")" )))))) ; theorem :: MESFUN9C: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 "E")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "S")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ) & (Bool (Set (Var "E")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ))) & (Bool "(" "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "m"))) ($#r1_mesfunc6 :::"is_measurable_on"::: ) (Set (Var "E"))) ")" )) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k1_mesfun9c :::"||"::: ) (Set (Var "E")) ")" ) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n"))) ($#r1_mesfunc6 :::"is_measurable_on"::: ) (Set (Var "E")))))))) ; theorem :: MESFUN9C:5 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "holds" (Bool (Set ($#k2_mesfunc9 :::"Partial_Sums"::: ) (Set "(" ($#k1_mesfunc5 :::"R_EAL"::: ) (Set (Var "seq")) ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k1_mesfunc5 :::"R_EAL"::: ) (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set (Var "seq")) ")" )))) ; theorem :: MESFUN9C: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 "E")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "S")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "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 (Var "E")))) "holds" (Bool (Set (Set (Var "F")) ($#k10_seqfunc :::"#"::: ) (Set (Var "x"))) "is" ($#v1_series_1 :::"summable"::: ) ) ")" )) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "E")))) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k1_mesfun9c :::"||"::: ) (Set (Var "E")) ")" ) ($#k10_seqfunc :::"#"::: ) (Set (Var "x"))) "is" ($#v1_series_1 :::"summable"::: ) )))))) ; definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); func :::"Partial_Sums"::: "F" -> ($#m1_subset_1 :::"Functional_Sequence":::) "of" "X" "," (Set ($#k1_numbers :::"REAL"::: ) ) means :: MESFUN9C:def 2 (Bool "(" (Bool (Set it ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r2_relset_1 :::"="::: ) (Set "F" ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set it ($#k4_mesfunc5 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set "(" it ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ($#k3_valued_1 :::"+"::: ) (Set "(" "F" ($#k4_mesfunc5 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"Partial_Sums"::: MESFUN9C:def 2 : (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "b3")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k2_mesfun9c :::"Partial_Sums"::: ) (Set (Var "F")))) "iff" (Bool "(" (Bool (Set (Set (Var "b3")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "b3")) ($#k4_mesfunc5 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "b3")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ($#k3_valued_1 :::"+"::: ) (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ))) ")" ) ")" ) ")" ))); theorem :: MESFUN9C:7 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k4_mesfunc9 :::"Partial_Sums"::: ) (Set "(" ($#k1_mesfun7c :::"R_EAL"::: ) (Set (Var "F")) ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k1_mesfun7c :::"R_EAL"::: ) (Set "(" ($#k2_mesfun9c :::"Partial_Sums"::: ) (Set (Var "F")) ")" ))))) ; theorem :: MESFUN9C:8 (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 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" ($#k2_mesfun9c :::"Partial_Sums"::: ) (Set (Var "F")) ")" ) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ))) & (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool "(" (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" ($#k2_mesfun9c :::"Partial_Sums"::: ) (Set (Var "F")) ")" ) ($#k4_mesfunc5 :::"."::: ) (Set (Var "m")) ")" ))) & (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "m")) ")" ))) ")" ))))) ; theorem :: MESFUN9C:9 (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 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k1_mesfun7c :::"R_EAL"::: ) (Set (Var "F"))) "is" ($#v2_mesfunc9 :::"additive"::: ) ))) ; theorem :: MESFUN9C:10 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" ($#k2_mesfun9c :::"Partial_Sums"::: ) (Set (Var "F")) ")" ) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_setfam_1 :::"meet"::: ) "{" (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "k")) ")" ) ")" ) where k "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) "}" ))))) ; theorem :: MESFUN9C:11 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_mesfunc8 :::"with_the_same_dom"::: ) )) "holds" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" ($#k2_mesfun9c :::"Partial_Sums"::: ) (Set (Var "F")) ")" ) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )))))) ; theorem :: MESFUN9C:12 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ) & (Bool (Set (Var "D")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "D")))) "holds" (Bool (Set (Set "(" ($#k3_series_1 :::"Partial_Sums"::: ) (Set "(" (Set (Var "F")) ($#k10_seqfunc :::"#"::: ) (Set (Var "x")) ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k2_mesfun9c :::"Partial_Sums"::: ) (Set (Var "F")) ")" ) ($#k10_seqfunc :::"#"::: ) (Set (Var "x")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))))))))) ; theorem :: MESFUN9C:13 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ) & (Bool (Set (Var "D")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "D")))) "holds" (Bool "(" (Bool (Set ($#k3_series_1 :::"Partial_Sums"::: ) (Set "(" (Set (Var "F")) ($#k10_seqfunc :::"#"::: ) (Set (Var "x")) ")" )) "is" ($#v2_comseq_2 :::"convergent"::: ) ) "iff" (Bool (Set (Set "(" ($#k2_mesfun9c :::"Partial_Sums"::: ) (Set (Var "F")) ")" ) ($#k10_seqfunc :::"#"::: ) (Set (Var "x"))) "is" ($#v2_comseq_2 :::"convergent"::: ) ) ")" ))))) ; theorem :: MESFUN9C:14 (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 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ) & (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_series_1 :::"Sum"::: ) (Set "(" (Set (Var "F")) ($#k10_seqfunc :::"#"::: ) (Set (Var "x")) ")" )))) "holds" (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k2_seq_2 :::"lim"::: ) (Set "(" (Set "(" ($#k2_mesfun9c :::"Partial_Sums"::: ) (Set (Var "F")) ")" ) ($#k10_seqfunc :::"#"::: ) (Set (Var "x")) ")" ))))))) ; theorem :: MESFUN9C: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 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool "(" "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "m"))) ($#r2_mesfunc6 :::"is_simple_func_in"::: ) (Set (Var "S"))) ")" )) "holds" (Bool (Set (Set "(" ($#k2_mesfun9c :::"Partial_Sums"::: ) (Set (Var "F")) ")" ) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n"))) ($#r2_mesfunc6 :::"is_simple_func_in"::: ) (Set (Var "S"))))))) ; theorem :: MESFUN9C:16 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "E")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "S")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n"))) ($#r1_mesfunc6 :::"is_measurable_on"::: ) (Set (Var "E"))) ")" )) "holds" (Bool (Set (Set "(" ($#k2_mesfun9c :::"Partial_Sums"::: ) (Set (Var "F")) ")" ) ($#k4_mesfunc5 :::"."::: ) (Set (Var "m"))) ($#r1_mesfunc6 :::"is_measurable_on"::: ) (Set (Var "E")))))))) ; theorem :: MESFUN9C:17 (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 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_mesfunc8 :::"with_the_same_dom"::: ) )) "holds" (Bool (Set ($#k2_mesfun9c :::"Partial_Sums"::: ) (Set (Var "F"))) "is" ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ))) ; theorem :: MESFUN9C:18 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "E")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "S")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "E"))) & (Bool (Set (Var "F")) "is" ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" ($#k2_mesfun9c :::"Partial_Sums"::: ) (Set (Var "F")) ")" ) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n"))) ($#r1_mesfunc6 :::"is_measurable_on"::: ) (Set (Var "E"))) ")" ) & (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")) ($#k10_seqfunc :::"#"::: ) (Set (Var "x"))) "is" ($#v1_series_1 :::"summable"::: ) ) ")" )) "holds" (Bool (Set ($#k8_mesfun7c :::"lim"::: ) (Set "(" ($#k2_mesfun9c :::"Partial_Sums"::: ) (Set (Var "F")) ")" )) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "E"))))))) ; theorem :: MESFUN9C:19 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n"))) ($#r3_mesfunc6 :::"is_integrable_on"::: ) (Set (Var "M"))) ")" )) "holds" (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" ($#k2_mesfun9c :::"Partial_Sums"::: ) (Set (Var "F")) ")" ) ($#k4_mesfunc5 :::"."::: ) (Set (Var "m"))) ($#r3_mesfunc6 :::"is_integrable_on"::: ) (Set (Var "M")))))))) ; begin theorem :: MESFUN9C:20 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k5_comseq_3 :::"Re"::: ) (Set (Var "f")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set (Var "A"))) ($#r2_relset_1 :::"="::: ) (Set ($#k5_comseq_3 :::"Re"::: ) (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A")) ")" ))) & (Bool (Set (Set "(" ($#k6_comseq_3 :::"Im"::: ) (Set (Var "f")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set (Var "A"))) ($#r2_relset_1 :::"="::: ) (Set ($#k6_comseq_3 :::"Im"::: ) (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A")) ")" ))) ")" )))) ; theorem :: MESFUN9C:21 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set ($#k11_mesfun7c :::"Re"::: ) (Set "(" (Set (Var "F")) ($#k1_mesfun9c :::"||"::: ) (Set (Var "D")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k11_mesfun7c :::"Re"::: ) (Set (Var "F")) ")" ) ($#k1_mesfun9c :::"||"::: ) (Set (Var "D"))))))) ; theorem :: MESFUN9C:22 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set ($#k12_mesfun7c :::"Im"::: ) (Set "(" (Set (Var "F")) ($#k1_mesfun9c :::"||"::: ) (Set (Var "D")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k12_mesfun7c :::"Im"::: ) (Set (Var "F")) ")" ) ($#k1_mesfun9c :::"||"::: ) (Set (Var "D"))))))) ; theorem :: MESFUN9C:23 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ) & (Bool (Set (Var "D")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) & (Bool (Set (Set (Var "F")) ($#k9_mesfun7c :::"#"::: ) (Set (Var "x"))) "is" ($#v2_comseq_2 :::"convergent"::: ) )) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k1_mesfun9c :::"||"::: ) (Set (Var "D")) ")" ) ($#k9_mesfun7c :::"#"::: ) (Set (Var "x"))) "is" ($#v2_comseq_2 :::"convergent"::: ) ))))) ; theorem :: MESFUN9C:24 (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 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ) "iff" (Bool (Set ($#k11_mesfun7c :::"Re"::: ) (Set (Var "F"))) "is" ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ) ")" ))) ; theorem :: MESFUN9C:25 (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 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool "(" (Bool (Set ($#k11_mesfun7c :::"Re"::: ) (Set (Var "F"))) "is" ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ) "iff" (Bool (Set ($#k12_mesfun7c :::"Im"::: ) (Set (Var "F"))) "is" ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ) ")" ))) ; theorem :: MESFUN9C:26 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ) & (Bool (Set (Var "D")) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ))) & (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 "D")))) "holds" (Bool (Set (Set (Var "F")) ($#k9_mesfun7c :::"#"::: ) (Set (Var "x"))) "is" ($#v2_comseq_2 :::"convergent"::: ) ) ")" )) "holds" (Bool (Set (Set "(" ($#k10_mesfun7c :::"lim"::: ) (Set (Var "F")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set (Var "D"))) ($#r2_relset_1 :::"="::: ) (Set ($#k10_mesfun7c :::"lim"::: ) (Set "(" (Set (Var "F")) ($#k1_mesfun9c :::"||"::: ) (Set (Var "D")) ")" )))))) ; theorem :: MESFUN9C:27 (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 "E")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "S")) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ) & (Bool (Set (Var "E")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ))) & (Bool "(" "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "m"))) ($#r1_mesfun6c :::"is_measurable_on"::: ) (Set (Var "E"))) ")" )) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k1_mesfun9c :::"||"::: ) (Set (Var "E")) ")" ) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n"))) ($#r1_mesfun6c :::"is_measurable_on"::: ) (Set (Var "E")))))))) ; theorem :: MESFUN9C:28 (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 "E")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "S")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set (Var "E")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ))) & (Bool (Set (Var "F")) "is" ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ) & (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")) ($#k9_mesfun7c :::"#"::: ) (Set (Var "x"))) "is" ($#v1_comseq_3 :::"summable"::: ) ) ")" )) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "E")))) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k1_mesfun9c :::"||"::: ) (Set (Var "E")) ")" ) ($#k9_mesfun7c :::"#"::: ) (Set (Var "x"))) "is" ($#v1_comseq_3 :::"summable"::: ) )))))) ; definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Const "X")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ); func :::"Partial_Sums"::: "F" -> ($#m1_subset_1 :::"Functional_Sequence":::) "of" "X" "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) means :: MESFUN9C:def 3 (Bool "(" (Bool (Set it ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r2_relset_1 :::"="::: ) (Set "F" ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set it ($#k4_mesfunc5 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set "(" it ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ($#k2_valued_1 :::"+"::: ) (Set "(" "F" ($#k4_mesfunc5 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"Partial_Sums"::: MESFUN9C:def 3 : (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "b3")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k3_mesfun9c :::"Partial_Sums"::: ) (Set (Var "F")))) "iff" (Bool "(" (Bool (Set (Set (Var "b3")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "b3")) ($#k4_mesfunc5 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "b3")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ($#k2_valued_1 :::"+"::: ) (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ))) ")" ) ")" ) ")" ))); theorem :: MESFUN9C:29 (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 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool "(" (Bool (Set ($#k2_mesfun9c :::"Partial_Sums"::: ) (Set "(" ($#k11_mesfun7c :::"Re"::: ) (Set (Var "F")) ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k11_mesfun7c :::"Re"::: ) (Set "(" ($#k3_mesfun9c :::"Partial_Sums"::: ) (Set (Var "F")) ")" ))) & (Bool (Set ($#k2_mesfun9c :::"Partial_Sums"::: ) (Set "(" ($#k12_mesfun7c :::"Im"::: ) (Set (Var "F")) ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k12_mesfun7c :::"Im"::: ) (Set "(" ($#k3_mesfun9c :::"Partial_Sums"::: ) (Set (Var "F")) ")" ))) ")" ))) ; theorem :: MESFUN9C:30 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" ($#k3_mesfun9c :::"Partial_Sums"::: ) (Set (Var "F")) ")" ) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ))) & (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool "(" (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" ($#k3_mesfun9c :::"Partial_Sums"::: ) (Set (Var "F")) ")" ) ($#k4_mesfunc5 :::"."::: ) (Set (Var "m")) ")" ))) & (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "m")) ")" ))) ")" ))))) ; theorem :: MESFUN9C:31 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" ($#k3_mesfun9c :::"Partial_Sums"::: ) (Set (Var "F")) ")" ) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_setfam_1 :::"meet"::: ) "{" (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "k")) ")" ) ")" ) where k "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) "}" ))))) ; theorem :: MESFUN9C:32 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_mesfunc8 :::"with_the_same_dom"::: ) )) "holds" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" ($#k3_mesfun9c :::"Partial_Sums"::: ) (Set (Var "F")) ")" ) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )))))) ; theorem :: MESFUN9C:33 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ) & (Bool (Set (Var "D")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "D")))) "holds" (Bool (Set (Set "(" ($#k10_comseq_3 :::"Partial_Sums"::: ) (Set "(" (Set (Var "F")) ($#k9_mesfun7c :::"#"::: ) (Set (Var "x")) ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k3_mesfun9c :::"Partial_Sums"::: ) (Set (Var "F")) ")" ) ($#k9_mesfun7c :::"#"::: ) (Set (Var "x")) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))))))))) ; theorem :: MESFUN9C:34 (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 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_mesfunc8 :::"with_the_same_dom"::: ) )) "holds" (Bool (Set ($#k3_mesfun9c :::"Partial_Sums"::: ) (Set (Var "F"))) "is" ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ))) ; theorem :: MESFUN9C:35 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ) & (Bool (Set (Var "D")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "D")))) "holds" (Bool "(" (Bool (Set ($#k10_comseq_3 :::"Partial_Sums"::: ) (Set "(" (Set (Var "F")) ($#k9_mesfun7c :::"#"::: ) (Set (Var "x")) ")" )) "is" ($#v2_comseq_2 :::"convergent"::: ) ) "iff" (Bool (Set (Set "(" ($#k3_mesfun9c :::"Partial_Sums"::: ) (Set (Var "F")) ")" ) ($#k9_mesfun7c :::"#"::: ) (Set (Var "x"))) "is" ($#v2_comseq_2 :::"convergent"::: ) ) ")" ))))) ; theorem :: MESFUN9C:36 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ) & (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Set (Var "F")) ($#k9_mesfun7c :::"#"::: ) (Set (Var "x"))) "is" ($#v1_comseq_3 :::"summable"::: ) ) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k11_comseq_3 :::"Sum"::: ) (Set "(" (Set (Var "F")) ($#k9_mesfun7c :::"#"::: ) (Set (Var "x")) ")" )))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k3_comseq_2 :::"lim"::: ) (Set "(" (Set "(" ($#k3_mesfun9c :::"Partial_Sums"::: ) (Set (Var "F")) ")" ) ($#k9_mesfun7c :::"#"::: ) (Set (Var "x")) ")" ))))))) ; theorem :: MESFUN9C:37 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "m"))) ($#r1_mesfun7c :::"is_simple_func_in"::: ) (Set (Var "S"))) ")" )) "holds" (Bool (Set (Set "(" ($#k3_mesfun9c :::"Partial_Sums"::: ) (Set (Var "F")) ")" ) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n"))) ($#r1_mesfun7c :::"is_simple_func_in"::: ) (Set (Var "S"))))))) ; theorem :: MESFUN9C:38 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "E")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "S")) (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n"))) ($#r1_mesfun6c :::"is_measurable_on"::: ) (Set (Var "E"))) ")" )) "holds" (Bool (Set (Set "(" ($#k3_mesfun9c :::"Partial_Sums"::: ) (Set (Var "F")) ")" ) ($#k4_mesfunc5 :::"."::: ) (Set (Var "m"))) ($#r1_mesfun6c :::"is_measurable_on"::: ) (Set (Var "E")))))))) ; theorem :: MESFUN9C:39 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "E")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "S")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "E"))) & (Bool (Set (Var "F")) "is" ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" ($#k3_mesfun9c :::"Partial_Sums"::: ) (Set (Var "F")) ")" ) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n"))) ($#r1_mesfun6c :::"is_measurable_on"::: ) (Set (Var "E"))) ")" ) & (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")) ($#k9_mesfun7c :::"#"::: ) (Set (Var "x"))) "is" ($#v1_comseq_3 :::"summable"::: ) ) ")" )) "holds" (Bool (Set ($#k10_mesfun7c :::"lim"::: ) (Set "(" ($#k3_mesfun9c :::"Partial_Sums"::: ) (Set (Var "F")) ")" )) ($#r1_mesfun6c :::"is_measurable_on"::: ) (Set (Var "E"))))))) ; theorem :: MESFUN9C:40 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n"))) ($#r2_mesfun6c :::"is_integrable_on"::: ) (Set (Var "M"))) ")" )) "holds" (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" ($#k3_mesfun9c :::"Partial_Sums"::: ) (Set (Var "F")) ")" ) ($#k4_mesfunc5 :::"."::: ) (Set (Var "m"))) ($#r2_mesfun6c :::"is_integrable_on"::: ) (Set (Var "M")))))))) ; begin theorem :: MESFUN9C:41 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "f")) ($#r1_mesfun7c :::"is_simple_func_in"::: ) (Set (Var "S")))) "holds" (Bool (Set (Var "f")) ($#r1_mesfun6c :::"is_measurable_on"::: ) (Set (Var "A"))))))) ; theorem :: MESFUN9C:42 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "f")) ($#r1_mesfun7c :::"is_simple_func_in"::: ) (Set (Var "S")))) "holds" (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A"))) ($#r1_mesfun7c :::"is_simple_func_in"::: ) (Set (Var "S"))))))) ; theorem :: MESFUN9C:43 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r1_mesfun7c :::"is_simple_func_in"::: ) (Set (Var "S")))) "holds" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))) "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "S")))))) ; theorem :: MESFUN9C:44 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r1_mesfun7c :::"is_simple_func_in"::: ) (Set (Var "S"))) & (Bool (Set (Var "g")) ($#r1_mesfun7c :::"is_simple_func_in"::: ) (Set (Var "S")))) "holds" (Bool (Set (Set (Var "f")) ($#k2_valued_1 :::"+"::: ) (Set (Var "g"))) ($#r1_mesfun7c :::"is_simple_func_in"::: ) (Set (Var "S")))))) ; theorem :: MESFUN9C:45 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "c")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "f")) ($#r1_mesfun7c :::"is_simple_func_in"::: ) (Set (Var "S")))) "holds" (Bool (Set (Set (Var "c")) ($#k25_valued_1 :::"(#)"::: ) (Set (Var "f"))) ($#r1_mesfun7c :::"is_simple_func_in"::: ) (Set (Var "S"))))))) ; begin theorem :: MESFUN9C:46 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "E")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "S")) (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 "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 :::".|"::: ) ) ($#k1_mesfunc9 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "P")) ($#k1_mesfunc9 :::"."::: ) (Set (Var "x"))))) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "E")))) "holds" (Bool (Set (Set (Var "F")) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x"))) "is" ($#v10_mesfunc5 :::"convergent"::: ) ) ")" )) "holds" (Bool (Set ($#k7_mesfunc8 :::"lim"::: ) (Set (Var "F"))) ($#r1_mesfunc5 :::"is_integrable_on"::: ) (Set (Var "M"))))))))) ; theorem :: MESFUN9C:47 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "E")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "S")) (Bool "for" (Set (Var "F")) "being" ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "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_mesfunc6 :::"is_measurable_on"::: ) (Set (Var "E"))) ")" ) & (Bool (Set (Var "P")) ($#r3_mesfunc6 :::"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 ($#k55_valued_1 :::"|."::: ) (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ($#k55_valued_1 :::".|"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "P")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))))) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "E")))) "holds" (Bool (Set (Set (Var "F")) ($#k10_seqfunc :::"#"::: ) (Set (Var "x"))) "is" ($#v2_comseq_2 :::"convergent"::: ) ) ")" )) "holds" (Bool (Set ($#k8_mesfun7c :::"lim"::: ) (Set (Var "F"))) ($#r1_mesfunc5 :::"is_integrable_on"::: ) (Set (Var "M"))))))))) ; theorem :: MESFUN9C:48 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "E")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "S")) (Bool "for" (Set (Var "F")) "being" ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "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_mesfunc6 :::"is_measurable_on"::: ) (Set (Var "E"))) ")" ) & (Bool (Set (Var "P")) ($#r3_mesfunc6 :::"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 ($#k55_valued_1 :::"|."::: ) (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ($#k55_valued_1 :::".|"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "P")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))))) ")" )) "holds" (Bool "ex" (Set (Var "I")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool "(" (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "I")) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k1_mesfunc6 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ")" )) ")" ) & "(" (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")) ($#k10_seqfunc :::"#"::: ) (Set (Var "x"))) "is" ($#v2_comseq_2 :::"convergent"::: ) ) ")" )) "implies" (Bool "(" (Bool (Set (Var "I")) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set (Var "I"))) ($#r1_hidden :::"="::: ) (Set ($#k7_mesfunc5 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" ($#k8_mesfun7c :::"lim"::: ) (Set (Var "F")) ")" ) ")" )) ")" ) ")" ")" )))))))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); attr "F" is :::"uniformly_bounded"::: means :: MESFUN9C:def 4 (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_subset_1 :::"Element"::: ) "of" "X" "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 ($#k17_complex1 :::"|."::: ) (Set "(" (Set "(" "F" ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k17_complex1 :::".|"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "K")))))); end; :: deftheorem defines :::"uniformly_bounded"::: MESFUN9C:def 4 : (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 ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v1_mesfun9c :::"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_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "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 ($#k17_complex1 :::"|."::: ) (Set "(" (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k17_complex1 :::".|"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "K")))))) ")" ))); theorem :: MESFUN9C:49 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "E")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "S")) (Bool "for" (Set (Var "F")) "being" ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Set (Var "M")) ($#k1_mesfunc9 :::"."::: ) (Set (Var "E"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_xxreal_0 :::"+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_mesfunc6 :::"is_measurable_on"::: ) (Set (Var "E"))) ")" ) & (Bool (Set (Var "F")) "is" ($#v1_mesfun9c :::"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")) ($#k10_seqfunc :::"#"::: ) (Set (Var "x"))) "is" ($#v2_comseq_2 :::"convergent"::: ) ) ")" )) "holds" (Bool "(" (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n"))) ($#r3_mesfunc6 :::"is_integrable_on"::: ) (Set (Var "M"))) ")" ) & (Bool (Set ($#k8_mesfun7c :::"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")) ($#k1_mesfunc9 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k1_mesfunc6 :::"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 "(" ($#k8_mesfun7c :::"lim"::: ) (Set (Var "F")) ")" ) ")" )) ")" )) ")" )))))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); pred "F" :::"is_uniformly_convergent_to"::: "f" means :: MESFUN9C:def 5 (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_subset_1 :::"Element"::: ) "of" "X" "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 ($#k17_complex1 :::"|."::: ) (Set "(" (Set "(" (Set "(" "F" ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" "f" ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ")" ) ($#k17_complex1 :::".|"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "e")))))) ")" ) ")" ); end; :: deftheorem defines :::"is_uniformly_convergent_to"::: MESFUN9C:def 5 : (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 ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "F")) ($#r1_mesfun9c :::"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_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "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 ($#k17_complex1 :::"|."::: ) (Set "(" (Set "(" (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ")" ) ($#k17_complex1 :::".|"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "e")))))) ")" ) ")" ) ")" )))); theorem :: MESFUN9C:50 (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" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "S")) (Bool "for" (Set (Var "F")) "being" ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Set (Var "M")) ($#k1_mesfunc9 :::"."::: ) (Set (Var "E"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_xxreal_0 :::"+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"))) ($#r3_mesfunc6 :::"is_integrable_on"::: ) (Set (Var "M"))) ")" ) & (Bool (Set (Var "F")) ($#r1_mesfun9c :::"is_uniformly_convergent_to"::: ) (Set (Var "f")))) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r3_mesfunc6 :::"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")) ($#k1_mesfunc9 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k1_mesfunc6 :::"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 ($#k1_mesfunc6 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set (Var "f")) ")" )) ")" )) ")" ))))))) ; theorem :: MESFUN9C:51 (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" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "S")) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) "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_mesfun6c :::"is_measurable_on"::: ) (Set (Var "E"))) ")" ) & (Bool (Set (Var "P")) ($#r3_mesfunc6 :::"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 ($#k55_valued_1 :::"|."::: ) (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ($#k55_valued_1 :::".|"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "P")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))))) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "E")))) "holds" (Bool (Set (Set (Var "F")) ($#k9_mesfun7c :::"#"::: ) (Set (Var "x"))) "is" ($#v2_comseq_2 :::"convergent"::: ) ) ")" )) "holds" (Bool (Set ($#k10_mesfun7c :::"lim"::: ) (Set (Var "F"))) ($#r2_mesfun6c :::"is_integrable_on"::: ) (Set (Var "M"))))))))) ; theorem :: MESFUN9C:52 (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" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "S")) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) "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_mesfun6c :::"is_measurable_on"::: ) (Set (Var "E"))) ")" ) & (Bool (Set (Var "P")) ($#r3_mesfunc6 :::"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 ($#k55_valued_1 :::"|."::: ) (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ($#k55_valued_1 :::".|"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "P")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))))) ")" )) "holds" (Bool "ex" (Set (Var "I")) "being" ($#m1_subset_1 :::"Complex_Sequence":::) "st" (Bool "(" (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "I")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k1_mesfun6c :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ")" )) ")" ) & "(" (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")) ($#k9_mesfun7c :::"#"::: ) (Set (Var "x"))) "is" ($#v2_comseq_2 :::"convergent"::: ) ) ")" )) "implies" (Bool "(" (Bool (Set (Var "I")) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k3_comseq_2 :::"lim"::: ) (Set (Var "I"))) ($#r1_hidden :::"="::: ) (Set ($#k1_mesfun6c :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" ($#k10_mesfun7c :::"lim"::: ) (Set (Var "F")) ")" ) ")" )) ")" ) ")" ")" )))))))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Const "X")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ); attr "F" is :::"uniformly_bounded"::: means :: MESFUN9C:def 6 (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_subset_1 :::"Element"::: ) "of" "X" "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 ($#k17_complex1 :::"|."::: ) (Set "(" (Set "(" "F" ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k17_complex1 :::".|"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "K")))))); end; :: deftheorem defines :::"uniformly_bounded"::: MESFUN9C:def 6 : (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 ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v2_mesfun9c :::"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_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "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 ($#k17_complex1 :::"|."::: ) (Set "(" (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k17_complex1 :::".|"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "K")))))) ")" ))); theorem :: MESFUN9C:53 (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" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "S")) (Bool "for" (Set (Var "F")) "being" ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set (Set (Var "M")) ($#k1_mesfunc9 :::"."::: ) (Set (Var "E"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_xxreal_0 :::"+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_mesfun6c :::"is_measurable_on"::: ) (Set (Var "E"))) ")" ) & (Bool (Set (Var "F")) "is" ($#v2_mesfun9c :::"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")) ($#k9_mesfun7c :::"#"::: ) (Set (Var "x"))) "is" ($#v2_comseq_2 :::"convergent"::: ) ) ")" )) "holds" (Bool "(" (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n"))) ($#r2_mesfun6c :::"is_integrable_on"::: ) (Set (Var "M"))) ")" ) & (Bool (Set ($#k10_mesfun7c :::"lim"::: ) (Set (Var "F"))) ($#r2_mesfun6c :::"is_integrable_on"::: ) (Set (Var "M"))) & (Bool "ex" (Set (Var "I")) "being" ($#m1_subset_1 :::"Complex_Sequence":::) "st" (Bool "(" (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "I")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k1_mesfun6c :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ")" )) ")" ) & (Bool (Set (Var "I")) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k3_comseq_2 :::"lim"::: ) (Set (Var "I"))) ($#r1_hidden :::"="::: ) (Set ($#k1_mesfun6c :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" ($#k10_mesfun7c :::"lim"::: ) (Set (Var "F")) ")" ) ")" )) ")" )) ")" )))))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Const "X")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ); let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ); pred "F" :::"is_uniformly_convergent_to"::: "f" means :: MESFUN9C:def 7 (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_subset_1 :::"Element"::: ) "of" "X" "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 ($#k17_complex1 :::"|."::: ) (Set "(" (Set "(" (Set "(" "F" ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" "f" ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ")" ) ($#k17_complex1 :::".|"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "e")))))) ")" ) ")" ); end; :: deftheorem defines :::"is_uniformly_convergent_to"::: MESFUN9C:def 7 : (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 ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool "(" (Bool (Set (Var "F")) ($#r2_mesfun9c :::"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_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "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 ($#k17_complex1 :::"|."::: ) (Set "(" (Set "(" (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ")" ) ($#k17_complex1 :::".|"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "e")))))) ")" ) ")" ) ")" )))); theorem :: MESFUN9C:54 (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" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "S")) (Bool "for" (Set (Var "F")) "being" ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set (Set (Var "M")) ($#k1_mesfunc9 :::"."::: ) (Set (Var "E"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_xxreal_0 :::"+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"))) ($#r2_mesfun6c :::"is_integrable_on"::: ) (Set (Var "M"))) ")" ) & (Bool (Set (Var "F")) ($#r2_mesfun9c :::"is_uniformly_convergent_to"::: ) (Set (Var "f")))) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_mesfun6c :::"is_integrable_on"::: ) (Set (Var "M"))) & (Bool "ex" (Set (Var "I")) "being" ($#m1_subset_1 :::"Complex_Sequence":::) "st" (Bool "(" (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "I")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k1_mesfun6c :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ")" )) ")" ) & (Bool (Set (Var "I")) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set ($#k3_comseq_2 :::"lim"::: ) (Set (Var "I"))) ($#r1_hidden :::"="::: ) (Set ($#k1_mesfun6c :::"Integral"::: ) "(" (Set (Var "M")) "," (Set (Var "f")) ")" )) ")" )) ")" ))))))) ;