:: MESFUN7C semantic presentation begin 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 :::"R_EAL"::: "f" -> ($#m1_subset_1 :::"Functional_Sequence":::) "of" "X" "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) equals :: MESFUN7C:def 1 "f"; end; :: deftheorem defines :::"R_EAL"::: MESFUN7C:def 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"::: ) ) "holds" (Bool (Set ($#k1_mesfun7c :::"R_EAL"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "f"))))); theorem :: MESFUN7C: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")) "holds" (Bool (Set (Set (Var "f")) ($#k10_seqfunc :::"#"::: ) (Set (Var "x"))) ($#r1_funct_2 :::"="::: ) (Set (Set "(" ($#k1_mesfun7c :::"R_EAL"::: ) (Set (Var "f")) ")" ) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x"))))))) ; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set ($#k1_mesfunc5 :::"R_EAL"::: ) "f") -> ($#v1_partfun1 :::"total"::: ) ; end; 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 :::"inf"::: "f" -> ($#m1_subset_1 :::"PartFunc":::) "of" "X" "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) equals :: MESFUN7C:def 2 (Set ($#k1_mesfunc8 :::"inf"::: ) (Set "(" ($#k1_mesfun7c :::"R_EAL"::: ) "f" ")" )); end; :: deftheorem defines :::"inf"::: MESFUN7C:def 2 : (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 ($#k2_mesfun7c :::"inf"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k1_mesfunc8 :::"inf"::: ) (Set "(" ($#k1_mesfun7c :::"R_EAL"::: ) (Set (Var "f")) ")" ))))); theorem :: MESFUN7C:2 (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")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k2_mesfun7c :::"inf"::: ) (Set (Var "f")) ")" )))) "holds" (Bool (Set (Set "(" ($#k2_mesfun7c :::"inf"::: ) (Set (Var "f")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k7_supinf_2 :::"inf"::: ) (Set "(" ($#k17_supinf_2 :::"rng"::: ) (Set "(" ($#k1_mesfunc5 :::"R_EAL"::: ) (Set "(" (Set (Var "f")) ($#k10_seqfunc :::"#"::: ) (Set (Var "x")) ")" ) ")" ) ")" )))))) ; 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 :::"sup"::: "f" -> ($#m1_subset_1 :::"PartFunc":::) "of" "X" "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) equals :: MESFUN7C:def 3 (Set ($#k2_mesfunc8 :::"sup"::: ) (Set "(" ($#k1_mesfun7c :::"R_EAL"::: ) "f" ")" )); end; :: deftheorem defines :::"sup"::: MESFUN7C:def 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"::: ) ) "holds" (Bool (Set ($#k3_mesfun7c :::"sup"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k2_mesfunc8 :::"sup"::: ) (Set "(" ($#k1_mesfun7c :::"R_EAL"::: ) (Set (Var "f")) ")" ))))); theorem :: MESFUN7C: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 "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 "(" ($#k3_mesfun7c :::"sup"::: ) (Set (Var "f")) ")" )))) "holds" (Bool (Set (Set "(" ($#k3_mesfun7c :::"sup"::: ) (Set (Var "f")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k8_supinf_2 :::"sup"::: ) (Set "(" ($#k17_supinf_2 :::"rng"::: ) (Set "(" ($#k1_mesfunc5 :::"R_EAL"::: ) (Set "(" (Set (Var "f")) ($#k10_seqfunc :::"#"::: ) (Set (Var "x")) ")" ) ")" ) ")" )))))) ; 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 :::"inferior_realsequence"::: "f" -> ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ($#m1_subset_1 :::"Functional_Sequence":::) "of" "X" "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) equals :: MESFUN7C:def 4 (Set ($#k3_mesfunc8 :::"inferior_realsequence"::: ) (Set "(" ($#k1_mesfun7c :::"R_EAL"::: ) "f" ")" )); end; :: deftheorem defines :::"inferior_realsequence"::: MESFUN7C:def 4 : (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_mesfun7c :::"inferior_realsequence"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k3_mesfunc8 :::"inferior_realsequence"::: ) (Set "(" ($#k1_mesfun7c :::"R_EAL"::: ) (Set (Var "f")) ")" ))))); theorem :: MESFUN7C:4 (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 "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" ($#k4_mesfun7c :::"inferior_realsequence"::: ) (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"::: ) ) ")" ))) & (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 "(" ($#k4_mesfun7c :::"inferior_realsequence"::: ) (Set (Var "f")) ")" ) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" )))) "holds" (Bool (Set (Set "(" (Set "(" ($#k4_mesfun7c :::"inferior_realsequence"::: ) (Set (Var "f")) ")" ) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_rinfsup2 :::"inferior_realsequence"::: ) (Set "(" ($#k1_mesfunc5 :::"R_EAL"::: ) (Set "(" (Set (Var "f")) ($#k10_seqfunc :::"#"::: ) (Set (Var "x")) ")" ) ")" ) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "n")))) ")" ) ")" )))) ; 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 :::"superior_realsequence"::: "f" -> ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ($#m1_subset_1 :::"Functional_Sequence":::) "of" "X" "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) equals :: MESFUN7C:def 5 (Set ($#k4_mesfunc8 :::"superior_realsequence"::: ) (Set "(" ($#k1_mesfun7c :::"R_EAL"::: ) "f" ")" )); end; :: deftheorem defines :::"superior_realsequence"::: MESFUN7C:def 5 : (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 ($#k5_mesfun7c :::"superior_realsequence"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k4_mesfunc8 :::"superior_realsequence"::: ) (Set "(" ($#k1_mesfun7c :::"R_EAL"::: ) (Set (Var "f")) ")" ))))); theorem :: MESFUN7C:5 (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 "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" ($#k5_mesfun7c :::"superior_realsequence"::: ) (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"::: ) ) ")" ))) & (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 "(" ($#k5_mesfun7c :::"superior_realsequence"::: ) (Set (Var "f")) ")" ) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" )))) "holds" (Bool (Set (Set "(" (Set "(" ($#k5_mesfun7c :::"superior_realsequence"::: ) (Set (Var "f")) ")" ) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_rinfsup2 :::"superior_realsequence"::: ) (Set "(" ($#k1_mesfunc5 :::"R_EAL"::: ) (Set "(" (Set (Var "f")) ($#k10_seqfunc :::"#"::: ) (Set (Var "x")) ")" ) ")" ) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "n")))) ")" ) ")" )))) ; theorem :: MESFUN7C:6 (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")) "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 (Set "(" ($#k4_mesfun7c :::"inferior_realsequence"::: ) (Set (Var "f")) ")" ) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x"))) ($#r2_funct_2 :::"="::: ) (Set ($#k3_rinfsup2 :::"inferior_realsequence"::: ) (Set "(" ($#k1_mesfunc5 :::"R_EAL"::: ) (Set "(" (Set (Var "f")) ($#k10_seqfunc :::"#"::: ) (Set (Var "x")) ")" ) ")" )))))) ; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set ($#k1_mesfun7c :::"R_EAL"::: ) "f") -> ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ; end; theorem :: MESFUN7C: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 ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "E")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Set (Var "f")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n"))) ($#r1_mesfunc6 :::"is_measurable_on"::: ) (Set (Var "E")))) "holds" (Bool (Set (Set "(" ($#k1_mesfun7c :::"R_EAL"::: ) (Set (Var "f")) ")" ) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n"))) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "E")))))))) ; theorem :: MESFUN7C: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")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" ($#k1_mesfun7c :::"R_EAL"::: ) (Set (Var "f")) ")" ) ($#k10_nat_1 :::"^\"::: ) (Set (Var "n"))) ($#r2_funct_2 :::"="::: ) (Set ($#k1_mesfun7c :::"R_EAL"::: ) (Set "(" (Set (Var "f")) ($#k10_nat_1 :::"^\"::: ) (Set (Var "n")) ")" )))))) ; theorem :: MESFUN7C:9 (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 ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" ($#k4_mesfun7c :::"inferior_realsequence"::: ) (Set (Var "f")) ")" ) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n"))) ($#r2_relset_1 :::"="::: ) (Set ($#k2_mesfun7c :::"inf"::: ) (Set "(" (Set (Var "f")) ($#k10_nat_1 :::"^\"::: ) (Set (Var "n")) ")" )))))) ; theorem :: MESFUN7C:10 (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 ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" ($#k5_mesfun7c :::"superior_realsequence"::: ) (Set (Var "f")) ")" ) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n"))) ($#r2_relset_1 :::"="::: ) (Set ($#k3_mesfun7c :::"sup"::: ) (Set "(" (Set (Var "f")) ($#k10_nat_1 :::"^\"::: ) (Set (Var "n")) ")" )))))) ; theorem :: MESFUN7C: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 "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 (Set "(" ($#k5_mesfun7c :::"superior_realsequence"::: ) (Set (Var "f")) ")" ) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x"))) ($#r2_funct_2 :::"="::: ) (Set ($#k4_rinfsup2 :::"superior_realsequence"::: ) (Set "(" ($#k1_mesfunc5 :::"R_EAL"::: ) (Set "(" (Set (Var "f")) ($#k10_seqfunc :::"#"::: ) (Set (Var "x")) ")" ) ")" )))))) ; 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 :::"lim_inf"::: "f" -> ($#m1_subset_1 :::"PartFunc":::) "of" "X" "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) equals :: MESFUN7C:def 6 (Set ($#k5_mesfunc8 :::"lim_inf"::: ) (Set "(" ($#k1_mesfun7c :::"R_EAL"::: ) "f" ")" )); end; :: deftheorem defines :::"lim_inf"::: MESFUN7C:def 6 : (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 ($#k6_mesfun7c :::"lim_inf"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k5_mesfunc8 :::"lim_inf"::: ) (Set "(" ($#k1_mesfun7c :::"R_EAL"::: ) (Set (Var "f")) ")" ))))); theorem :: MESFUN7C: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 "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 "(" ($#k6_mesfun7c :::"lim_inf"::: ) (Set (Var "f")) ")" )))) "holds" (Bool (Set (Set "(" ($#k6_mesfun7c :::"lim_inf"::: ) (Set (Var "f")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k6_rinfsup2 :::"lim_inf"::: ) (Set "(" ($#k1_mesfunc5 :::"R_EAL"::: ) (Set "(" (Set (Var "f")) ($#k10_seqfunc :::"#"::: ) (Set (Var "x")) ")" ) ")" )))))) ; 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 :::"lim_sup"::: "f" -> ($#m1_subset_1 :::"PartFunc":::) "of" "X" "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) equals :: MESFUN7C:def 7 (Set ($#k6_mesfunc8 :::"lim_sup"::: ) (Set "(" ($#k1_mesfun7c :::"R_EAL"::: ) "f" ")" )); end; :: deftheorem defines :::"lim_sup"::: MESFUN7C:def 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 ($#k7_mesfun7c :::"lim_sup"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k6_mesfunc8 :::"lim_sup"::: ) (Set "(" ($#k1_mesfun7c :::"R_EAL"::: ) (Set (Var "f")) ")" ))))); theorem :: MESFUN7C: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")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k7_mesfun7c :::"lim_sup"::: ) (Set (Var "f")) ")" )))) "holds" (Bool (Set (Set "(" ($#k7_mesfun7c :::"lim_sup"::: ) (Set (Var "f")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k5_rinfsup2 :::"lim_sup"::: ) (Set "(" ($#k1_mesfunc5 :::"R_EAL"::: ) (Set "(" (Set (Var "f")) ($#k10_seqfunc :::"#"::: ) (Set (Var "x")) ")" ) ")" )))))) ; 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 :::"lim"::: "f" -> ($#m1_subset_1 :::"PartFunc":::) "of" "X" "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) equals :: MESFUN7C:def 8 (Set ($#k7_mesfunc8 :::"lim"::: ) (Set "(" ($#k1_mesfun7c :::"R_EAL"::: ) "f" ")" )); end; :: deftheorem defines :::"lim"::: MESFUN7C:def 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"::: ) ) "holds" (Bool (Set ($#k8_mesfun7c :::"lim"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k7_mesfunc8 :::"lim"::: ) (Set "(" ($#k1_mesfun7c :::"R_EAL"::: ) (Set (Var "f")) ")" ))))); theorem :: MESFUN7C: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 "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 "(" ($#k8_mesfun7c :::"lim"::: ) (Set (Var "f")) ")" )))) "holds" (Bool (Set (Set "(" ($#k8_mesfun7c :::"lim"::: ) (Set (Var "f")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k2_mesfunc5 :::"lim"::: ) (Set "(" ($#k1_mesfunc5 :::"R_EAL"::: ) (Set "(" (Set (Var "f")) ($#k10_seqfunc :::"#"::: ) (Set (Var "x")) ")" ) ")" )))))) ; theorem :: MESFUN7C:15 (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")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k8_mesfun7c :::"lim"::: ) (Set (Var "f")) ")" ))) & (Bool (Set (Set (Var "f")) ($#k10_seqfunc :::"#"::: ) (Set (Var "x"))) "is" ($#v2_comseq_2 :::"convergent"::: ) )) "holds" (Bool "(" (Bool (Set (Set "(" ($#k8_mesfun7c :::"lim"::: ) (Set (Var "f")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_mesfun7c :::"lim_sup"::: ) (Set (Var "f")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "x")))) & (Bool (Set (Set "(" ($#k8_mesfun7c :::"lim"::: ) (Set (Var "f")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_mesfun7c :::"lim_inf"::: ) (Set (Var "f")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "x")))) ")" )))) ; theorem :: MESFUN7C: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 "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 :::"SetSequence":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ($#k8_subset_1 :::"/\"::: ) (Set "(" ($#k13_mesfunc1 :::"great_dom"::: ) "(" (Set "(" (Set (Var "f")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) "," (Set (Var "r")) ")" ")" ))) ")" )) "holds" (Bool (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k17_mesfunc1 :::"great_dom"::: ) "(" (Set "(" ($#k3_mesfun7c :::"sup"::: ) (Set (Var "f")) ")" ) "," (Set (Var "r")) ")" ")" )))))))) ; theorem :: MESFUN7C:17 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "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 :::"SetSequence":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ($#k8_subset_1 :::"/\"::: ) (Set "(" ($#k14_mesfunc1 :::"great_eq_dom"::: ) "(" (Set "(" (Set (Var "f")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) "," (Set (Var "r")) ")" ")" ))) ")" )) "holds" (Bool (Set ($#k1_setfam_1 :::"meet"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k18_mesfunc1 :::"great_eq_dom"::: ) "(" (Set "(" ($#k2_mesfun7c :::"inf"::: ) (Set (Var "f")) ")" ) "," (Set (Var "r")) ")" ")" )))))))) ; theorem :: MESFUN7C: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 "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 "E")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "E"))) & (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 ($#k7_mesfun7c :::"lim_sup"::: ) (Set (Var "f"))) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "E"))))))) ; theorem :: MESFUN7C: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 "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 "E")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "E"))) & (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 ($#k6_mesfun7c :::"lim_inf"::: ) (Set (Var "f"))) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "E"))))))) ; theorem :: MESFUN7C: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 :::"Functional_Sequence":::) "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 "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ))) & (Bool (Set (Set (Var "f")) ($#k10_seqfunc :::"#"::: ) (Set (Var "x"))) "is" ($#v2_comseq_2 :::"convergent"::: ) )) "holds" (Bool (Set (Set "(" ($#k5_mesfun7c :::"superior_realsequence"::: ) (Set (Var "f")) ")" ) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x"))) "is" ($#v1_rinfsup2 :::"bounded_below"::: ) )))) ; theorem :: MESFUN7C:21 (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" ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "E")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "E"))) & (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 "(" "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_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "E"))))))) ; theorem :: MESFUN7C:22 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "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 "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "E")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "E"))) & (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 ($#k1_relset_1 :::"dom"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (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 "(" (Bool (Set (Set (Var "f")) ($#k10_seqfunc :::"#"::: ) (Set (Var "x"))) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set (Set (Var "g")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k2_seq_2 :::"lim"::: ) (Set "(" (Set (Var "f")) ($#k10_seqfunc :::"#"::: ) (Set (Var "x")) ")" ))) ")" ) ")" )) "holds" (Bool (Set (Var "g")) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "E")))))))) ; begin definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "H" be ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Const "X")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ); let "x" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "X")); func "H" :::"#"::: "x" -> ($#m1_subset_1 :::"Complex_Sequence":::) means :: MESFUN7C:def 9 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "H" ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ($#k1_funct_1 :::"."::: ) "x"))); end; :: deftheorem defines :::"#"::: MESFUN7C:def 9 : (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Complex_Sequence":::) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "H")) ($#k9_mesfun7c :::"#"::: ) (Set (Var "x")))) "iff" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "b4")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "H")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))))) ")" ))))); 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 :::"lim"::: "f" -> ($#m1_subset_1 :::"PartFunc":::) "of" "X" "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) means :: MESFUN7C:def 10 (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" "f" ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "X" "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) it))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k3_comseq_2 :::"lim"::: ) (Set "(" "f" ($#k9_mesfun7c :::"#"::: ) (Set (Var "x")) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"lim"::: MESFUN7C:def 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 ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k10_mesfun7c :::"lim"::: ) (Set (Var "f")))) "iff" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "b3"))) ($#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 ($#k1_relset_1 :::"dom"::: ) (Set (Var "b3"))))) "holds" (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k3_comseq_2 :::"lim"::: ) (Set "(" (Set (Var "f")) ($#k9_mesfun7c :::"#"::: ) (Set (Var "x")) ")" ))) ")" ) ")" ) ")" )))); 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 :::"Re"::: "f" -> ($#m1_subset_1 :::"Functional_Sequence":::) "of" "X" "," (Set ($#k1_numbers :::"REAL"::: ) ) means :: MESFUN7C:def 11 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" it ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" "f" ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ))) & (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 "(" it ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" )))) "holds" (Bool (Set (Set "(" it ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_comseq_3 :::"Re"::: ) (Set "(" "f" ($#k9_mesfun7c :::"#"::: ) (Set (Var "x")) ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "n")))) ")" ) ")" )); end; :: deftheorem defines :::"Re"::: MESFUN7C:def 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 ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (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 ($#k11_mesfun7c :::"Re"::: ) (Set (Var "f")))) "iff" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "b3")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ))) & (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 "b3")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" )))) "holds" (Bool (Set (Set "(" (Set (Var "b3")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_comseq_3 :::"Re"::: ) (Set "(" (Set (Var "f")) ($#k9_mesfun7c :::"#"::: ) (Set (Var "x")) ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "n")))) ")" ) ")" )) ")" )))); registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Const "X")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ); cluster (Set ($#k11_mesfun7c :::"Re"::: ) "f") -> ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ; end; 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 :::"Im"::: "f" -> ($#m1_subset_1 :::"Functional_Sequence":::) "of" "X" "," (Set ($#k1_numbers :::"REAL"::: ) ) means :: MESFUN7C:def 12 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" it ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" "f" ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ))) & (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 "(" it ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" )))) "holds" (Bool (Set (Set "(" it ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k8_comseq_3 :::"Im"::: ) (Set "(" "f" ($#k9_mesfun7c :::"#"::: ) (Set (Var "x")) ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "n")))) ")" ) ")" )); end; :: deftheorem defines :::"Im"::: MESFUN7C:def 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 ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (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 ($#k12_mesfun7c :::"Im"::: ) (Set (Var "f")))) "iff" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "b3")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ))) & (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 "b3")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" )))) "holds" (Bool (Set (Set "(" (Set (Var "b3")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k8_comseq_3 :::"Im"::: ) (Set "(" (Set (Var "f")) ($#k9_mesfun7c :::"#"::: ) (Set (Var "x")) ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "n")))) ")" ) ")" )) ")" )))); registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Const "X")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ); cluster (Set ($#k12_mesfun7c :::"Im"::: ) "f") -> ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ; end; theorem :: MESFUN7C:23 (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 ($#k2_numbers :::"COMPLEX"::: ) ) (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 "(" (Bool (Set (Set "(" ($#k11_mesfun7c :::"Re"::: ) (Set (Var "f")) ")" ) ($#k10_seqfunc :::"#"::: ) (Set (Var "x"))) ($#r2_funct_2 :::"="::: ) (Set ($#k7_comseq_3 :::"Re"::: ) (Set "(" (Set (Var "f")) ($#k9_mesfun7c :::"#"::: ) (Set (Var "x")) ")" ))) & (Bool (Set (Set "(" ($#k12_mesfun7c :::"Im"::: ) (Set (Var "f")) ")" ) ($#k10_seqfunc :::"#"::: ) (Set (Var "x"))) ($#r2_funct_2 :::"="::: ) (Set ($#k8_comseq_3 :::"Im"::: ) (Set "(" (Set (Var "f")) ($#k9_mesfun7c :::"#"::: ) (Set (Var "x")) ")" ))) ")" )))) ; theorem :: MESFUN7C: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"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set (Set "(" ($#k11_mesfun7c :::"Re"::: ) (Set (Var "f")) ")" ) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n"))) ($#r2_relset_1 :::"="::: ) (Set ($#k5_comseq_3 :::"Re"::: ) (Set "(" (Set (Var "f")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ))) & (Bool (Set (Set "(" ($#k12_mesfun7c :::"Im"::: ) (Set (Var "f")) ")" ) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n"))) ($#r2_relset_1 :::"="::: ) (Set ($#k6_comseq_3 :::"Im"::: ) (Set "(" (Set (Var "f")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ))) ")" )))) ; theorem :: MESFUN7C:25 (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 ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )))) "holds" (Bool (Set (Set (Var "f")) ($#k9_mesfun7c :::"#"::: ) (Set (Var "x"))) "is" ($#v2_comseq_2 :::"convergent"::: ) ) ")" )) "holds" (Bool "(" (Bool (Set ($#k8_mesfun7c :::"lim"::: ) (Set "(" ($#k11_mesfun7c :::"Re"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_comseq_3 :::"Re"::: ) (Set "(" ($#k10_mesfun7c :::"lim"::: ) (Set (Var "f")) ")" ))) & (Bool (Set ($#k8_mesfun7c :::"lim"::: ) (Set "(" ($#k12_mesfun7c :::"Im"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_comseq_3 :::"Im"::: ) (Set "(" ($#k10_mesfun7c :::"lim"::: ) (Set (Var "f")) ")" ))) ")" ))) ; theorem :: MESFUN7C:26 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "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 "E")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "E"))) & (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 "(" "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"))) ($#r1_mesfun6c :::"is_measurable_on"::: ) (Set (Var "E"))))))) ; theorem :: MESFUN7C: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 "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 "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "E")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "E"))) & (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 ($#k1_relset_1 :::"dom"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (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 "(" (Bool (Set (Set (Var "f")) ($#k9_mesfun7c :::"#"::: ) (Set (Var "x"))) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k3_comseq_2 :::"lim"::: ) (Set "(" (Set (Var "f")) ($#k9_mesfun7c :::"#"::: ) (Set (Var "x")) ")" ))) ")" ) ")" )) "holds" (Bool (Set (Var "g")) ($#r1_mesfun6c :::"is_measurable_on"::: ) (Set (Var "E")))))))) ; begin theorem :: MESFUN7C:28 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set (Set "(" (Set (Var "r")) ($#k25_valued_1 :::"(#)"::: ) (Set (Var "f")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set (Var "Y"))) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "r")) ($#k25_valued_1 :::"(#)"::: ) (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "Y")) ")" ))))))) ; theorem :: MESFUN7C:29 (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 "k")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "E")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Var "E")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "f")) ($#r1_mesfun6c :::"is_measurable_on"::: ) (Set (Var "E")))) "holds" (Bool (Set (Set ($#k55_valued_1 :::"|."::: ) (Set (Var "f")) ($#k55_valued_1 :::".|"::: ) ) ($#k2_mesfun6c :::"to_power"::: ) (Set (Var "k"))) ($#r1_mesfunc6 :::"is_measurable_on"::: ) (Set (Var "E")))))))) ; theorem :: MESFUN7C:30 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set "(" ($#k1_mesfunc5 :::"R_EAL"::: ) (Set (Var "f")) ")" ) ($#k5_mesfunc1 :::"(#)"::: ) (Set "(" ($#k1_mesfunc5 :::"R_EAL"::: ) (Set (Var "g")) ")" )) ($#r2_relset_1 :::"="::: ) (Set ($#k1_mesfunc5 :::"R_EAL"::: ) (Set "(" (Set (Var "f")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "g")) ")" ))))) ; theorem :: MESFUN7C:31 (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" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "g")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "E"))) & (Bool (Set (Var "f")) ($#r1_mesfunc6 :::"is_measurable_on"::: ) (Set (Var "E"))) & (Bool (Set (Var "g")) ($#r1_mesfunc6 :::"is_measurable_on"::: ) (Set (Var "E")))) "holds" (Bool (Set (Set (Var "f")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "g"))) ($#r1_mesfunc6 :::"is_measurable_on"::: ) (Set (Var "E"))))))) ; theorem :: MESFUN7C:32 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool "(" (Bool (Set ($#k5_comseq_3 :::"Re"::: ) (Set "(" (Set (Var "f")) ($#k19_valued_1 :::"(#)"::: ) (Set (Var "g")) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set "(" ($#k5_comseq_3 :::"Re"::: ) (Set (Var "f")) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set "(" ($#k5_comseq_3 :::"Re"::: ) (Set (Var "g")) ")" ) ")" ) ($#k47_valued_1 :::"-"::: ) (Set "(" (Set "(" ($#k6_comseq_3 :::"Im"::: ) (Set (Var "f")) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set "(" ($#k6_comseq_3 :::"Im"::: ) (Set (Var "g")) ")" ) ")" ))) & (Bool (Set ($#k6_comseq_3 :::"Im"::: ) (Set "(" (Set (Var "f")) ($#k19_valued_1 :::"(#)"::: ) (Set (Var "g")) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set "(" ($#k6_comseq_3 :::"Im"::: ) (Set (Var "f")) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set "(" ($#k5_comseq_3 :::"Re"::: ) (Set (Var "g")) ")" ) ")" ) ($#k3_valued_1 :::"+"::: ) (Set "(" (Set "(" ($#k5_comseq_3 :::"Re"::: ) (Set (Var "f")) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set "(" ($#k6_comseq_3 :::"Im"::: ) (Set (Var "g")) ")" ) ")" ))) ")" ))) ; theorem :: MESFUN7C:33 (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"::: ) ) (Bool "for" (Set (Var "E")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "g")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "E"))) & (Bool (Set (Var "f")) ($#r1_mesfun6c :::"is_measurable_on"::: ) (Set (Var "E"))) & (Bool (Set (Var "g")) ($#r1_mesfun6c :::"is_measurable_on"::: ) (Set (Var "E")))) "holds" (Bool (Set (Set (Var "f")) ($#k19_valued_1 :::"(#)"::: ) (Set (Var "g"))) ($#r1_mesfun6c :::"is_measurable_on"::: ) (Set (Var "E"))))))) ; theorem :: MESFUN7C:34 (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 ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool "ex" (Set (Var "E")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool "(" (Bool (Set (Var "E")) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "E")) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "g")))) & (Bool (Set (Var "f")) ($#r1_mesfunc6 :::"is_measurable_on"::: ) (Set (Var "E"))) & (Bool (Set (Var "g")) ($#r1_mesfunc6 :::"is_measurable_on"::: ) (Set (Var "E"))) ")" )) & (Bool (Set (Var "f")) "is" ($#v6_supinf_2 :::"nonnegative"::: ) ) & (Bool (Set (Var "g")) "is" ($#v6_supinf_2 :::"nonnegative"::: ) ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "g"))))) "holds" (Bool (Set (Set (Var "g")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x")))) ")" )) "holds" (Bool (Set ($#k1_mesfunc6 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set (Var "g")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_mesfunc6 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set (Var "f")) ")" )))))) ; theorem :: MESFUN7C:35 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r2_mesfun6c :::"is_integrable_on"::: ) (Set (Var "M")))) "holds" (Bool "(" (Bool "ex" (Set (Var "A")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool "(" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "f")) ($#r1_mesfun6c :::"is_measurable_on"::: ) (Set (Var "A"))) ")" )) & (Bool (Set ($#k55_valued_1 :::"|."::: ) (Set (Var "f")) ($#k55_valued_1 :::".|"::: ) ) ($#r3_mesfunc6 :::"is_integrable_on"::: ) (Set (Var "M"))) ")" ))))) ; theorem :: MESFUN7C:36 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r2_mesfun6c :::"is_integrable_on"::: ) (Set (Var "M")))) "holds" (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set (Var "S")) "st" (Bool "(" (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k8_subset_1 :::"/\"::: ) (Set "(" ($#k14_mesfunc1 :::"great_eq_dom"::: ) "(" (Set ($#k55_valued_1 :::"|."::: ) (Set (Var "f")) ($#k55_valued_1 :::".|"::: ) ) "," (Set "(" ($#k1_measure6 :::"R_EAL"::: ) (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ")" ")" ))) ")" ) & (Bool (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" ($#k10_relat_1 :::"eq_dom"::: ) "(" (Set ($#k55_valued_1 :::"|."::: ) (Set (Var "f")) ($#k55_valued_1 :::".|"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_setfam_1 :::"union"::: ) (Set "(" ($#k4_measure1 :::"rng"::: ) (Set (Var "F")) ")" ))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) & (Bool (Set (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set "(" (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_supinf_1 :::"+infty"::: ) )) ")" ) ")" ) ")" )))))) ; theorem :: MESFUN7C:37 (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 (Set (Set ($#k55_valued_1 :::"|."::: ) (Set (Var "f")) ($#k55_valued_1 :::".|"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set (Var "A"))) ($#r2_relset_1 :::"="::: ) (Set ($#k55_valued_1 :::"|."::: ) (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A")) ")" ) ($#k55_valued_1 :::".|"::: ) ))))) ; theorem :: MESFUN7C:38 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set ($#k55_valued_1 :::"|."::: ) (Set (Var "f")) ($#k55_valued_1 :::".|"::: ) ) ($#k3_valued_1 :::"+"::: ) (Set ($#k55_valued_1 :::"|."::: ) (Set (Var "g")) ($#k55_valued_1 :::".|"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "g")) ")" ))) & (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k55_valued_1 :::"|."::: ) (Set "(" (Set (Var "f")) ($#k2_valued_1 :::"+"::: ) (Set (Var "g")) ")" ) ($#k55_valued_1 :::".|"::: ) )) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k55_valued_1 :::"|."::: ) (Set (Var "f")) ($#k55_valued_1 :::".|"::: ) ))) ")" ))) ; theorem :: MESFUN7C:39 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set (Set "(" (Set ($#k55_valued_1 :::"|."::: ) (Set (Var "f")) ($#k55_valued_1 :::".|"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set ($#k55_valued_1 :::"|."::: ) (Set "(" (Set (Var "f")) ($#k2_valued_1 :::"+"::: ) (Set (Var "g")) ")" ) ($#k55_valued_1 :::".|"::: ) ) ")" ) ")" ) ($#k3_valued_1 :::"+"::: ) (Set "(" (Set ($#k55_valued_1 :::"|."::: ) (Set (Var "g")) ($#k55_valued_1 :::".|"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set ($#k55_valued_1 :::"|."::: ) (Set "(" (Set (Var "f")) ($#k2_valued_1 :::"+"::: ) (Set (Var "g")) ")" ) ($#k55_valued_1 :::".|"::: ) ) ")" ) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set ($#k55_valued_1 :::"|."::: ) (Set (Var "f")) ($#k55_valued_1 :::".|"::: ) ) ($#k3_valued_1 :::"+"::: ) (Set ($#k55_valued_1 :::"|."::: ) (Set (Var "g")) ($#k55_valued_1 :::".|"::: ) ) ")" ) ($#k2_partfun1 :::"|"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set ($#k55_valued_1 :::"|."::: ) (Set "(" (Set (Var "f")) ($#k2_valued_1 :::"+"::: ) (Set (Var "g")) ")" ) ($#k55_valued_1 :::".|"::: ) ) ")" ))))) ; theorem :: MESFUN7C:40 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k55_valued_1 :::"|."::: ) (Set "(" (Set (Var "f")) ($#k2_valued_1 :::"+"::: ) (Set (Var "g")) ")" ) ($#k55_valued_1 :::".|"::: ) )))) "holds" (Bool (Set (Set ($#k55_valued_1 :::"|."::: ) (Set "(" (Set (Var "f")) ($#k2_valued_1 :::"+"::: ) (Set (Var "g")) ")" ) ($#k55_valued_1 :::".|"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set ($#k55_valued_1 :::"|."::: ) (Set (Var "f")) ($#k55_valued_1 :::".|"::: ) ) ($#k3_valued_1 :::"+"::: ) (Set ($#k55_valued_1 :::"|."::: ) (Set (Var "g")) ($#k55_valued_1 :::".|"::: ) ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))))))) ; theorem :: MESFUN7C:41 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "g")) ($#k1_seq_1 :::"."::: ) (Set (Var "x")))) ")" )) "holds" (Bool (Set (Set (Var "g")) ($#k47_valued_1 :::"-"::: ) (Set (Var "f"))) "is" ($#v6_supinf_2 :::"nonnegative"::: ) ))) ; theorem :: MESFUN7C: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 "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 ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r2_mesfun6c :::"is_integrable_on"::: ) (Set (Var "M"))) & (Bool (Set (Var "g")) ($#r2_mesfun6c :::"is_integrable_on"::: ) (Set (Var "M")))) "holds" (Bool "ex" (Set (Var "E")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool "(" (Bool (Set (Var "E")) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k2_valued_1 :::"+"::: ) (Set (Var "g")) ")" ))) & (Bool (Set ($#k1_mesfunc6 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" (Set ($#k55_valued_1 :::"|."::: ) (Set "(" (Set (Var "f")) ($#k2_valued_1 :::"+"::: ) (Set (Var "g")) ")" ) ($#k55_valued_1 :::".|"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set (Var "E")) ")" ) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k1_mesfunc6 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" (Set ($#k55_valued_1 :::"|."::: ) (Set (Var "f")) ($#k55_valued_1 :::".|"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set (Var "E")) ")" ) ")" ")" ) ($#k3_supinf_2 :::"+"::: ) (Set "(" ($#k1_mesfunc6 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" (Set ($#k55_valued_1 :::"|."::: ) (Set (Var "g")) ($#k55_valued_1 :::".|"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set (Var "E")) ")" ) ")" ")" ))) ")" )))))) ; begin definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "X")); let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ); pred "f" :::"is_simple_func_in"::: "S" means :: MESFUN7C:def 13 (Bool "ex" (Set (Var "F")) "being" ($#m2_finseq_1 :::"Finite_Sep_Sequence":::) "of" "S" "st" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) "f") ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "F")) ")" ))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "X" "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "F")))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "y"))))) ")" ) ")" )); end; :: deftheorem defines :::"is_simple_func_in"::: MESFUN7C:def 13 : (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_mesfun7c :::"is_simple_func_in"::: ) (Set (Var "S"))) "iff" (Bool "ex" (Set (Var "F")) "being" ($#m2_finseq_1 :::"Finite_Sep_Sequence":::) "of" (Set (Var "S")) "st" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "F")) ")" ))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "F")))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "y"))))) ")" ) ")" )) ")" )))); definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "X")); let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); let "F" be ($#m2_finseq_1 :::"Finite_Sep_Sequence":::) "of" (Set (Const "S")); let "a" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ); pred "F" "," "a" :::"are_Re-presentation_of"::: "f" means :: MESFUN7C:def 14 (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) "f") ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) "F" ")" ))) & (Bool (Set ($#k4_finseq_1 :::"dom"::: ) "F") ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "a")) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "F"))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "F" ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool (Set "f" ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set "a" ($#k1_seq_1 :::"."::: ) (Set (Var "n"))))) ")" ) ")" ); end; :: deftheorem defines :::"are_Re-presentation_of"::: MESFUN7C:def 14 : (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"Finite_Sep_Sequence":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "a")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "F")) "," (Set (Var "a")) ($#r2_mesfun7c :::"are_Re-presentation_of"::: ) (Set (Var "f"))) "iff" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "F")) ")" ))) & (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "a")))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))))) ")" ) ")" ) ")" )))))); definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "X")); let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ); let "F" be ($#m2_finseq_1 :::"Finite_Sep_Sequence":::) "of" (Set (Const "S")); let "a" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ); pred "F" "," "a" :::"are_Re-presentation_of"::: "f" means :: MESFUN7C:def 15 (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) "f") ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) "F" ")" ))) & (Bool (Set ($#k4_finseq_1 :::"dom"::: ) "F") ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "a")) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "F"))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "F" ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set "a" ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) ")" ) ")" ); end; :: deftheorem defines :::"are_Re-presentation_of"::: MESFUN7C:def 15 : (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"Finite_Sep_Sequence":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "a")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool "(" (Bool (Set (Var "F")) "," (Set (Var "a")) ($#r3_mesfun7c :::"are_Re-presentation_of"::: ) (Set (Var "f"))) "iff" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "F")) ")" ))) & (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "a")))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) ")" ) ")" ) ")" )))))); theorem :: MESFUN7C: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"::: ) ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_mesfun7c :::"is_simple_func_in"::: ) (Set (Var "S"))) "iff" (Bool "(" (Bool (Set ($#k5_comseq_3 :::"Re"::: ) (Set (Var "f"))) ($#r2_mesfunc6 :::"is_simple_func_in"::: ) (Set (Var "S"))) & (Bool (Set ($#k6_comseq_3 :::"Im"::: ) (Set (Var "f"))) ($#r2_mesfunc6 :::"is_simple_func_in"::: ) (Set (Var "S"))) ")" ) ")" )))) ; theorem :: MESFUN7C: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")) "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 "ex" (Set (Var "F")) "being" ($#m2_finseq_1 :::"Finite_Sep_Sequence":::) "of" (Set (Var "S"))(Bool "ex" (Set (Var "a")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "F")) ")" ))) & (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "a")))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) ")" ) ")" )))))) ; theorem :: MESFUN7C: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"::: ) ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_mesfun7c :::"is_simple_func_in"::: ) (Set (Var "S"))) "iff" (Bool "ex" (Set (Var "F")) "being" ($#m2_finseq_1 :::"Finite_Sep_Sequence":::) "of" (Set (Var "S"))(Bool "ex" (Set (Var "a")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Set (Var "F")) "," (Set (Var "a")) ($#r3_mesfun7c :::"are_Re-presentation_of"::: ) (Set (Var "f"))))) ")" )))) ; theorem :: MESFUN7C:46 (Bool "for" (Set (Var "c")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k6_complsp2 :::"Re"::: ) (Set (Var "c")) ")" )))) "holds" (Bool (Set (Set "(" ($#k6_complsp2 :::"Re"::: ) (Set (Var "c")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k3_complex1 :::"Re"::: ) (Set "(" (Set (Var "c")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ))))) ; theorem :: MESFUN7C:47 (Bool "for" (Set (Var "c")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k7_complsp2 :::"Im"::: ) (Set (Var "c")) ")" )))) "holds" (Bool (Set (Set "(" ($#k7_complsp2 :::"Im"::: ) (Set (Var "c")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k4_complex1 :::"Im"::: ) (Set "(" (Set (Var "c")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ))))) ; theorem :: MESFUN7C: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 "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"Finite_Sep_Sequence":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "a")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool "(" (Bool (Set (Var "F")) "," (Set (Var "a")) ($#r3_mesfun7c :::"are_Re-presentation_of"::: ) (Set (Var "f"))) "iff" (Bool "(" (Bool (Set (Var "F")) "," (Set ($#k6_complsp2 :::"Re"::: ) (Set (Var "a"))) ($#r2_mesfun7c :::"are_Re-presentation_of"::: ) (Set ($#k5_comseq_3 :::"Re"::: ) (Set (Var "f")))) & (Bool (Set (Var "F")) "," (Set ($#k7_complsp2 :::"Im"::: ) (Set (Var "a"))) ($#r2_mesfun7c :::"are_Re-presentation_of"::: ) (Set ($#k6_comseq_3 :::"Im"::: ) (Set (Var "f")))) ")" ) ")" )))))) ; theorem :: MESFUN7C: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 "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_mesfun7c :::"is_simple_func_in"::: ) (Set (Var "S"))) "iff" (Bool "ex" (Set (Var "F")) "being" ($#m2_finseq_1 :::"Finite_Sep_Sequence":::) "of" (Set (Var "S"))(Bool "ex" (Set (Var "c")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "F")) ")" ))) & (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "c")))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool (Set (Set "(" ($#k5_comseq_3 :::"Re"::: ) (Set (Var "f")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_complsp2 :::"Re"::: ) (Set (Var "c")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))))) ")" ) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool (Set (Set "(" ($#k6_comseq_3 :::"Im"::: ) (Set (Var "f")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_complsp2 :::"Im"::: ) (Set (Var "c")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))))) ")" ) ")" ))) ")" )))) ;