:: MESFUN6C semantic presentation begin theorem :: MESFUN6C:1 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k1_measure6 :::"R_EAL"::: ) (Set (Var "a")) ")" ) ($#k3_supinf_2 :::"+"::: ) (Set "(" ($#k1_measure6 :::"R_EAL"::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "b")))) & (Bool (Set ($#k2_supinf_2 :::"-"::: ) (Set "(" ($#k1_measure6 :::"R_EAL"::: ) (Set (Var "a")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "a")))) & (Bool (Set (Set "(" ($#k1_measure6 :::"R_EAL"::: ) (Set (Var "a")) ")" ) ($#k4_supinf_2 :::"-"::: ) (Set "(" ($#k1_measure6 :::"R_EAL"::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "b")))) & (Bool (Set (Set "(" ($#k1_measure6 :::"R_EAL"::: ) (Set (Var "a")) ")" ) ($#k1_extreal1 :::"*"::: ) (Set "(" ($#k1_measure6 :::"R_EAL"::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "b")))) ")" )) ; 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"::: ) ); let "E" be ($#m2_subset_1 :::"Element"::: ) "of" (Set (Const "S")); pred "f" :::"is_measurable_on"::: "E" means :: MESFUN6C:def 1 (Bool "(" (Bool (Set ($#k5_comseq_3 :::"Re"::: ) "f") ($#r1_mesfunc6 :::"is_measurable_on"::: ) "E") & (Bool (Set ($#k6_comseq_3 :::"Im"::: ) "f") ($#r1_mesfunc6 :::"is_measurable_on"::: ) "E") ")" ); end; :: deftheorem defines :::"is_measurable_on"::: MESFUN6C:def 1 : (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "E")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_mesfun6c :::"is_measurable_on"::: ) (Set (Var "E"))) "iff" (Bool "(" (Bool (Set ($#k5_comseq_3 :::"Re"::: ) (Set (Var "f"))) ($#r1_mesfunc6 :::"is_measurable_on"::: ) (Set (Var "E"))) & (Bool (Set ($#k6_comseq_3 :::"Im"::: ) (Set (Var "f"))) ($#r1_mesfunc6 :::"is_measurable_on"::: ) (Set (Var "E"))) ")" ) ")" ))))); theorem :: MESFUN6C: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 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" (Bool (Set (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set "(" ($#k5_comseq_3 :::"Re"::: ) (Set (Var "f")) ")" )) ($#r2_relset_1 :::"="::: ) (Set ($#k5_comseq_3 :::"Re"::: ) (Set "(" (Set (Var "r")) ($#k25_valued_1 :::"(#)"::: ) (Set (Var "f")) ")" ))) & (Bool (Set (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set "(" ($#k6_comseq_3 :::"Im"::: ) (Set (Var "f")) ")" )) ($#r2_relset_1 :::"="::: ) (Set ($#k6_comseq_3 :::"Im"::: ) (Set "(" (Set (Var "r")) ($#k25_valued_1 :::"(#)"::: ) (Set (Var "f")) ")" ))) ")" )))) ; theorem :: MESFUN6C: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 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "c")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set ($#k5_comseq_3 :::"Re"::: ) (Set "(" (Set (Var "c")) ($#k25_valued_1 :::"(#)"::: ) (Set (Var "f")) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "c")) ")" ) ($#k26_valued_1 :::"(#)"::: ) (Set "(" ($#k5_comseq_3 :::"Re"::: ) (Set (Var "f")) ")" ) ")" ) ($#k47_valued_1 :::"-"::: ) (Set "(" (Set "(" ($#k4_complex1 :::"Im"::: ) (Set (Var "c")) ")" ) ($#k26_valued_1 :::"(#)"::: ) (Set "(" ($#k6_comseq_3 :::"Im"::: ) (Set (Var "f")) ")" ) ")" ))) & (Bool (Set ($#k6_comseq_3 :::"Im"::: ) (Set "(" (Set (Var "c")) ($#k25_valued_1 :::"(#)"::: ) (Set (Var "f")) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set "(" ($#k4_complex1 :::"Im"::: ) (Set (Var "c")) ")" ) ($#k26_valued_1 :::"(#)"::: ) (Set "(" ($#k5_comseq_3 :::"Re"::: ) (Set (Var "f")) ")" ) ")" ) ($#k3_valued_1 :::"+"::: ) (Set "(" (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "c")) ")" ) ($#k26_valued_1 :::"(#)"::: ) (Set "(" ($#k6_comseq_3 :::"Im"::: ) (Set (Var "f")) ")" ) ")" ))) ")" )))) ; theorem :: MESFUN6C: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 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool "(" (Bool (Set ($#k32_valued_1 :::"-"::: ) (Set "(" ($#k6_comseq_3 :::"Im"::: ) (Set (Var "f")) ")" )) ($#r2_relset_1 :::"="::: ) (Set ($#k5_comseq_3 :::"Re"::: ) (Set "(" (Set ($#k7_complex1 :::""::: ) ) ($#k25_valued_1 :::"(#)"::: ) (Set (Var "f")) ")" ))) & (Bool (Set ($#k5_comseq_3 :::"Re"::: ) (Set (Var "f"))) ($#r2_relset_1 :::"="::: ) (Set ($#k6_comseq_3 :::"Im"::: ) (Set "(" (Set ($#k7_complex1 :::""::: ) ) ($#k25_valued_1 :::"(#)"::: ) (Set (Var "f")) ")" ))) ")" ))) ; theorem :: MESFUN6C:5 (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")) ($#k2_valued_1 :::"+"::: ) (Set (Var "g")) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set "(" ($#k5_comseq_3 :::"Re"::: ) (Set (Var "f")) ")" ) ($#k3_valued_1 :::"+"::: ) (Set "(" ($#k5_comseq_3 :::"Re"::: ) (Set (Var "g")) ")" ))) & (Bool (Set ($#k6_comseq_3 :::"Im"::: ) (Set "(" (Set (Var "f")) ($#k2_valued_1 :::"+"::: ) (Set (Var "g")) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set "(" ($#k6_comseq_3 :::"Im"::: ) (Set (Var "f")) ")" ) ($#k3_valued_1 :::"+"::: ) (Set "(" ($#k6_comseq_3 :::"Im"::: ) (Set (Var "g")) ")" ))) ")" ))) ; theorem :: MESFUN6C:6 (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")) ($#k46_valued_1 :::"-"::: ) (Set (Var "g")) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set "(" ($#k5_comseq_3 :::"Re"::: ) (Set (Var "f")) ")" ) ($#k47_valued_1 :::"-"::: ) (Set "(" ($#k5_comseq_3 :::"Re"::: ) (Set (Var "g")) ")" ))) & (Bool (Set ($#k6_comseq_3 :::"Im"::: ) (Set "(" (Set (Var "f")) ($#k46_valued_1 :::"-"::: ) (Set (Var "g")) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set "(" ($#k6_comseq_3 :::"Im"::: ) (Set (Var "f")) ")" ) ($#k47_valued_1 :::"-"::: ) (Set "(" ($#k6_comseq_3 :::"Im"::: ) (Set (Var "g")) ")" ))) ")" ))) ; theorem :: MESFUN6C:7 (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" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "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 :: MESFUN6C: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 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set (Var "f")) ($#r2_relset_1 :::"="::: ) (Set (Set "(" ($#k5_comseq_3 :::"Re"::: ) (Set (Var "f")) ")" ) ($#k2_valued_1 :::"+"::: ) (Set "(" (Set ($#k7_complex1 :::""::: ) ) ($#k25_valued_1 :::"(#)"::: ) (Set "(" ($#k6_comseq_3 :::"Im"::: ) (Set (Var "f")) ")" ) ")" ))))) ; theorem :: MESFUN6C:9 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "B")) "," (Set (Var "A")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) & (Bool (Set (Var "f")) ($#r1_mesfun6c :::"is_measurable_on"::: ) (Set (Var "A")))) "holds" (Bool (Set (Var "f")) ($#r1_mesfun6c :::"is_measurable_on"::: ) (Set (Var "B"))))))) ; theorem :: MESFUN6C:10 (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")) "," (Set (Var "B")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "f")) ($#r1_mesfun6c :::"is_measurable_on"::: ) (Set (Var "A"))) & (Bool (Set (Var "f")) ($#r1_mesfun6c :::"is_measurable_on"::: ) (Set (Var "B")))) "holds" (Bool (Set (Var "f")) ($#r1_mesfun6c :::"is_measurable_on"::: ) (Set (Set (Var "A")) ($#k6_prob_1 :::"\/"::: ) (Set (Var "B")))))))) ; theorem :: MESFUN6C:11 (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 "A")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "f")) ($#r1_mesfun6c :::"is_measurable_on"::: ) (Set (Var "A"))) & (Bool (Set (Var "g")) ($#r1_mesfun6c :::"is_measurable_on"::: ) (Set (Var "A")))) "holds" (Bool (Set (Set (Var "f")) ($#k2_valued_1 :::"+"::: ) (Set (Var "g"))) ($#r1_mesfun6c :::"is_measurable_on"::: ) (Set (Var "A"))))))) ; theorem :: MESFUN6C:12 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "f")) ($#r1_mesfun6c :::"is_measurable_on"::: ) (Set (Var "A"))) & (Bool (Set (Var "g")) ($#r1_mesfun6c :::"is_measurable_on"::: ) (Set (Var "A"))) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "g"))))) "holds" (Bool (Set (Set (Var "f")) ($#k46_valued_1 :::"-"::: ) (Set (Var "g"))) ($#r1_mesfun6c :::"is_measurable_on"::: ) (Set (Var "A"))))))) ; theorem :: MESFUN6C:13 (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")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set (Var "Y")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k2_valued_1 :::"+"::: ) (Set (Var "g")) ")" )))) "holds" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "Y")) ")" ) ($#k2_valued_1 :::"+"::: ) (Set "(" (Set (Var "g")) ($#k2_partfun1 :::"|"::: ) (Set (Var "Y")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "Y"))) & (Bool (Set (Set "(" (Set (Var "f")) ($#k2_valued_1 :::"+"::: ) (Set (Var "g")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set (Var "Y"))) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "Y")) ")" ) ($#k2_valued_1 :::"+"::: ) (Set "(" (Set (Var "g")) ($#k2_partfun1 :::"|"::: ) (Set (Var "Y")) ")" ))) ")" )))) ; theorem :: MESFUN6C: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 ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "B")) "," (Set (Var "A")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "f")) ($#r1_mesfun6c :::"is_measurable_on"::: ) (Set (Var "B"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set (Var "B"))))) "holds" (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "B"))) ($#r1_mesfun6c :::"is_measurable_on"::: ) (Set (Var "A"))))))) ; theorem :: MESFUN6C: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")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) & (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "g"))) ($#r2_hidden :::"in"::: ) (Set (Var "S")))) "holds" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k2_valued_1 :::"+"::: ) (Set (Var "g")) ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "S")))))) ; theorem :: MESFUN6C: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" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "A")))) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_mesfun6c :::"is_measurable_on"::: ) (Set (Var "B"))) "iff" (Bool (Set (Var "f")) ($#r1_mesfun6c :::"is_measurable_on"::: ) (Set (Set (Var "A")) ($#k5_prob_1 :::"/\"::: ) (Set (Var "B")))) ")" ))))) ; theorem :: MESFUN6C: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" ($#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"::: ) (Bool "for" (Set (Var "A")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "f")) ($#r1_mesfun6c :::"is_measurable_on"::: ) (Set (Var "A"))) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "c")) ($#k25_valued_1 :::"(#)"::: ) (Set (Var "f"))) ($#r1_mesfun6c :::"is_measurable_on"::: ) (Set (Var "A")))))))) ; theorem :: MESFUN6C: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" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool "ex" (Set (Var "A")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "A"))))) "holds" (Bool "for" (Set (Var "c")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "B")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "f")) ($#r1_mesfun6c :::"is_measurable_on"::: ) (Set (Var "B")))) "holds" (Bool (Set (Set (Var "c")) ($#k25_valued_1 :::"(#)"::: ) (Set (Var "f"))) ($#r1_mesfun6c :::"is_measurable_on"::: ) (Set (Var "B")))))))) ; 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 "M" be ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Const "S")); let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ); pred "f" :::"is_integrable_on"::: "M" means :: MESFUN6C:def 2 (Bool "(" (Bool (Set ($#k5_comseq_3 :::"Re"::: ) "f") ($#r3_mesfunc6 :::"is_integrable_on"::: ) "M") & (Bool (Set ($#k6_comseq_3 :::"Im"::: ) "f") ($#r3_mesfunc6 :::"is_integrable_on"::: ) "M") ")" ); end; :: deftheorem defines :::"is_integrable_on"::: MESFUN6C:def 2 : (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_mesfun6c :::"is_integrable_on"::: ) (Set (Var "M"))) "iff" (Bool "(" (Bool (Set ($#k5_comseq_3 :::"Re"::: ) (Set (Var "f"))) ($#r3_mesfunc6 :::"is_integrable_on"::: ) (Set (Var "M"))) & (Bool (Set ($#k6_comseq_3 :::"Im"::: ) (Set (Var "f"))) ($#r3_mesfunc6 :::"is_integrable_on"::: ) (Set (Var "M"))) ")" ) ")" ))))); definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "X")); let "M" be ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Const "S")); let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ); assume (Bool (Set (Const "f")) ($#r2_mesfun6c :::"is_integrable_on"::: ) (Set (Const "M"))) ; func :::"Integral"::: "(" "M" "," "f" ")" -> ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) means :: MESFUN6C:def 3 (Bool "ex" (Set (Var "R")) "," (Set (Var "I")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "R")) ($#r1_hidden :::"="::: ) (Set ($#k1_mesfunc6 :::"Integral"::: ) "(" "M" "," (Set "(" ($#k5_comseq_3 :::"Re"::: ) "f" ")" ) ")" )) & (Bool (Set (Var "I")) ($#r1_hidden :::"="::: ) (Set ($#k1_mesfunc6 :::"Integral"::: ) "(" "M" "," (Set "(" ($#k6_comseq_3 :::"Im"::: ) "f" ")" ) ")" )) & (Bool it ($#r1_hidden :::"="::: ) (Set (Set (Var "R")) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "I")) ($#k3_xcmplx_0 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ))) ")" )); end; :: deftheorem defines :::"Integral"::: MESFUN6C:def 3 : (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "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 "for" (Set (Var "b5")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k1_mesfun6c :::"Integral"::: ) "(" (Set (Var "M")) "," (Set (Var "f")) ")" )) "iff" (Bool "ex" (Set (Var "R")) "," (Set (Var "I")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "R")) ($#r1_hidden :::"="::: ) (Set ($#k1_mesfunc6 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" ($#k5_comseq_3 :::"Re"::: ) (Set (Var "f")) ")" ) ")" )) & (Bool (Set (Var "I")) ($#r1_hidden :::"="::: ) (Set ($#k1_mesfunc6 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" ($#k6_comseq_3 :::"Im"::: ) (Set (Var "f")) ")" ) ")" )) & (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set (Set (Var "R")) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "I")) ($#k3_xcmplx_0 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ))) ")" )) ")" )))))); theorem :: MESFUN6C: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 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "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 "f")) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "E"))) ")" )) & (Bool (Set (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A"))) ($#r1_mesfunc5 :::"is_integrable_on"::: ) (Set (Var "M")))))))) ; theorem :: MESFUN6C:20 (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 ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "E")) "," (Set (Var "A")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "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 "f")) ($#r1_mesfunc6 :::"is_measurable_on"::: ) (Set (Var "E"))) ")" )) & (Bool (Set (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A"))) ($#r3_mesfunc6 :::"is_integrable_on"::: ) (Set (Var "M")))))))) ; theorem :: MESFUN6C: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 "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"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "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 "f")) ($#r1_mesfun6c :::"is_measurable_on"::: ) (Set (Var "E"))) ")" )) & (Bool (Set (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A"))) ($#r2_mesfun6c :::"is_integrable_on"::: ) (Set (Var "M"))) & (Bool (Set ($#k1_mesfun6c :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )))))) ; theorem :: MESFUN6C: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 "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"::: ) ) (Bool "for" (Set (Var "E")) "," (Set (Var "A")) "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 "f")) ($#r2_mesfun6c :::"is_integrable_on"::: ) (Set (Var "M"))) & (Bool (Set (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k1_mesfun6c :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set "(" (Set (Var "E")) ($#k7_prob_1 :::"\"::: ) (Set (Var "A")) ")" ) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_mesfun6c :::"Integral"::: ) "(" (Set (Var "M")) "," (Set (Var "f")) ")" ))))))) ; theorem :: MESFUN6C:23 (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"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "f")) ($#r2_mesfun6c :::"is_integrable_on"::: ) (Set (Var "M")))) "holds" (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A"))) ($#r2_mesfun6c :::"is_integrable_on"::: ) (Set (Var "M")))))))) ; theorem :: MESFUN6C:24 (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"::: ) ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "f")) ($#r2_mesfun6c :::"is_integrable_on"::: ) (Set (Var "M"))) & (Bool (Set (Var "A")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "B")))) "holds" (Bool (Set ($#k1_mesfun6c :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set "(" (Set (Var "A")) ($#k6_prob_1 :::"\/"::: ) (Set (Var "B")) ")" ) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_mesfun6c :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A")) ")" ) ")" ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k1_mesfun6c :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "B")) ")" ) ")" ")" )))))))) ; theorem :: MESFUN6C:25 (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"::: ) ) (Bool "for" (Set (Var "B")) "," (Set (Var "A")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "f")) ($#r2_mesfun6c :::"is_integrable_on"::: ) (Set (Var "M"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set (Var "A"))))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A"))) ($#r2_mesfun6c :::"is_integrable_on"::: ) (Set (Var "M"))) & (Bool (Set ($#k1_mesfun6c :::"Integral"::: ) "(" (Set (Var "M")) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_mesfun6c :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A")) ")" ) ")" ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k1_mesfun6c :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "B")) ")" ) ")" ")" ))) ")" )))))) ; definitionlet "k" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; let "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); func "f" :::"to_power"::: "k" -> ($#m1_subset_1 :::"PartFunc":::) "of" "X" "," (Set ($#k1_numbers :::"REAL"::: ) ) means :: MESFUN6C:def 4 (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) "f")) & (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_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "f" ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k3_power :::"to_power"::: ) "k")) ")" ) ")" ); end; :: deftheorem defines :::"to_power"::: MESFUN6C:def 4 : (Bool "for" (Set (Var "k")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "b4")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k2_mesfun6c :::"to_power"::: ) (Set (Var "k")))) "iff" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (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 "b4"))))) "holds" (Bool (Set (Set (Var "b4")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k3_power :::"to_power"::: ) (Set (Var "k")))) ")" ) ")" ) ")" )))); registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) "X" ($#v4_relat_1 :::"-defined"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_VALUED_0() bbbadV2_VALUED_0() bbbadV3_VALUED_0() ($#v6_supinf_2 :::"nonnegative"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1("X" "," (Set ($#k1_numbers :::"REAL"::: ) ))))); end; registrationlet "k" be ($#v1_xreal_0 :::"real"::: ) ($#~v3_xxreal_0 "non" ($#v3_xxreal_0 :::"negative"::: ) ) ($#m1_hidden :::"number"::: ) ; let "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#v6_supinf_2 :::"nonnegative"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set "f" ($#k2_mesfun6c :::"to_power"::: ) "k") -> ($#v6_supinf_2 :::"nonnegative"::: ) ; end; theorem :: MESFUN6C:26 (Bool "for" (Set (Var "k")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (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")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) "is" ($#v6_supinf_2 :::"nonnegative"::: ) ) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k")))) "holds" (Bool (Set (Set (Var "f")) ($#k2_mesfun6c :::"to_power"::: ) (Set (Var "k"))) "is" ($#v6_supinf_2 :::"nonnegative"::: ) )))))) ; theorem :: MESFUN6C:27 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (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")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) "is" ($#v6_supinf_2 :::"nonnegative"::: ) )) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k4_power :::"to_power"::: ) (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" )))))))) ; theorem :: MESFUN6C: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 "A")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "A")) ($#k8_subset_1 :::"/\"::: ) (Set "(" ($#k11_mesfunc1 :::"less_dom"::: ) "(" (Set (Var "f")) "," (Set (Var "a")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k7_subset_1 :::"\"::: ) (Set "(" (Set (Var "A")) ($#k8_subset_1 :::"/\"::: ) (Set "(" ($#k14_mesfunc1 :::"great_eq_dom"::: ) "(" (Set (Var "f")) "," (Set (Var "a")) ")" ")" ) ")" )))))))) ; theorem :: MESFUN6C:29 (Bool "for" (Set (Var "k")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (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")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f")) "is" ($#v6_supinf_2 :::"nonnegative"::: ) ) & (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_mesfunc6 :::"is_measurable_on"::: ) (Set (Var "E")))) "holds" (Bool (Set (Set (Var "f")) ($#k2_mesfun6c :::"to_power"::: ) (Set (Var "k"))) ($#r1_mesfunc6 :::"is_measurable_on"::: ) (Set (Var "E")))))))) ; theorem :: MESFUN6C:30 (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" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "f")) ($#r1_mesfun6c :::"is_measurable_on"::: ) (Set (Var "A"))) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set ($#k55_valued_1 :::"|."::: ) (Set (Var "f")) ($#k55_valued_1 :::".|"::: ) ) ($#r1_mesfunc6 :::"is_measurable_on"::: ) (Set (Var "A"))))))) ; theorem :: MESFUN6C: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 "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 "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"))) ")" ))) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_mesfun6c :::"is_integrable_on"::: ) (Set (Var "M"))) "iff" (Bool (Set ($#k55_valued_1 :::"|."::: ) (Set (Var "f")) ($#k55_valued_1 :::".|"::: ) ) ($#r3_mesfunc6 :::"is_integrable_on"::: ) (Set (Var "M"))) ")" ))))) ; theorem :: MESFUN6C:32 (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 (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k2_valued_1 :::"+"::: ) (Set (Var "g")) ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "S"))))))) ; theorem :: MESFUN6C: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 "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 (Set (Set (Var "f")) ($#k2_valued_1 :::"+"::: ) (Set (Var "g"))) ($#r2_mesfun6c :::"is_integrable_on"::: ) (Set (Var "M"))))))) ; theorem :: MESFUN6C: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 (Set (Var "f")) ($#r3_mesfunc6 :::"is_integrable_on"::: ) (Set (Var "M"))) & (Bool (Set (Var "g")) ($#r3_mesfunc6 :::"is_integrable_on"::: ) (Set (Var "M")))) "holds" (Bool (Set (Set (Var "f")) ($#k47_valued_1 :::"-"::: ) (Set (Var "g"))) ($#r3_mesfunc6 :::"is_integrable_on"::: ) (Set (Var "M"))))))) ; theorem :: MESFUN6C: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")) "," (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 (Set (Set (Var "f")) ($#k46_valued_1 :::"-"::: ) (Set (Var "g"))) ($#r2_mesfun6c :::"is_integrable_on"::: ) (Set (Var "M"))))))) ; theorem :: MESFUN6C: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")) "," (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 (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "g")) ")" ))) & (Bool (Set ($#k1_mesfun6c :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "f")) ($#k2_valued_1 :::"+"::: ) (Set (Var "g")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_mesfun6c :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "E")) ")" ) ")" ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k1_mesfun6c :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "g")) ($#k2_partfun1 :::"|"::: ) (Set (Var "E")) ")" ) ")" ")" ))) ")" )))))) ; theorem :: MESFUN6C: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 "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 (Set (Var "f")) ($#r3_mesfunc6 :::"is_integrable_on"::: ) (Set (Var "M"))) & (Bool (Set (Var "g")) ($#r3_mesfunc6 :::"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 (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "g")) ")" ))) & (Bool (Set ($#k1_mesfunc6 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "f")) ($#k47_valued_1 :::"-"::: ) (Set (Var "g")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_mesfunc6 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "E")) ")" ) ")" ")" ) ($#k3_supinf_2 :::"+"::: ) (Set "(" ($#k1_mesfunc6 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" (Set "(" ($#k32_valued_1 :::"-"::: ) (Set (Var "g")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set (Var "E")) ")" ) ")" ")" ))) ")" )))))) ; theorem :: MESFUN6C: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 "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"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "f")) ($#r2_mesfun6c :::"is_integrable_on"::: ) (Set (Var "M")))) "holds" (Bool "(" (Bool (Set (Set (Var "r")) ($#k25_valued_1 :::"(#)"::: ) (Set (Var "f"))) ($#r2_mesfun6c :::"is_integrable_on"::: ) (Set (Var "M"))) & (Bool (Set ($#k1_mesfun6c :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "r")) ($#k25_valued_1 :::"(#)"::: ) (Set (Var "f")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k1_mesfun6c :::"Integral"::: ) "(" (Set (Var "M")) "," (Set (Var "f")) ")" ")" ))) ")" )))))) ; theorem :: MESFUN6C: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 "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 (Set (Set ($#k7_complex1 :::""::: ) ) ($#k25_valued_1 :::"(#)"::: ) (Set (Var "f"))) ($#r2_mesfun6c :::"is_integrable_on"::: ) (Set (Var "M"))) & (Bool (Set ($#k1_mesfun6c :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" (Set ($#k7_complex1 :::""::: ) ) ($#k25_valued_1 :::"(#)"::: ) (Set (Var "f")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set ($#k7_complex1 :::""::: ) ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k1_mesfun6c :::"Integral"::: ) "(" (Set (Var "M")) "," (Set (Var "f")) ")" ")" ))) ")" ))))) ; theorem :: MESFUN6C: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 :::"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")) ($#r2_mesfun6c :::"is_integrable_on"::: ) (Set (Var "M")))) "holds" (Bool "(" (Bool (Set (Set (Var "c")) ($#k25_valued_1 :::"(#)"::: ) (Set (Var "f"))) ($#r2_mesfun6c :::"is_integrable_on"::: ) (Set (Var "M"))) & (Bool (Set ($#k1_mesfun6c :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "c")) ($#k25_valued_1 :::"(#)"::: ) (Set (Var "f")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "c")) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k1_mesfun6c :::"Integral"::: ) "(" (Set (Var "M")) "," (Set (Var "f")) ")" ")" ))) ")" )))))) ; theorem :: MESFUN6C:41 (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 ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set (Set "(" (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set (Var "Y"))) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "Y")) ")" ))))))) ; theorem :: MESFUN6C: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 ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool "ex" (Set (Var "A")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool "(" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "g")) ")" ))) & (Bool (Set (Var "f")) ($#r1_mesfunc6 :::"is_measurable_on"::: ) (Set (Var "A"))) & (Bool (Set (Var "g")) ($#r1_mesfunc6 :::"is_measurable_on"::: ) (Set (Var "A"))) ")" )) & (Bool (Set (Var "f")) ($#r3_mesfunc6 :::"is_integrable_on"::: ) (Set (Var "M"))) & (Bool (Set (Var "g")) ($#r3_mesfunc6 :::"is_integrable_on"::: ) (Set (Var "M"))) & (Bool (Set (Set (Var "g")) ($#k47_valued_1 :::"-"::: ) (Set (Var "f"))) "is" ($#v6_supinf_2 :::"nonnegative"::: ) )) "holds" (Bool "ex" (Set (Var "E")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool "(" (Bool (Set (Var "E")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "g")) ")" ))) & (Bool (Set ($#k1_mesfunc6 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "E")) ")" ) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_mesfunc6 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "g")) ($#k2_partfun1 :::"|"::: ) (Set (Var "E")) ")" ) ")" )) ")" )))))) ; theorem :: MESFUN6C: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 "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 "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 (Var "f")) ($#r2_mesfun6c :::"is_integrable_on"::: ) (Set (Var "M")))) "holds" (Bool (Set ($#k17_complex1 :::"|."::: ) (Set "(" ($#k1_mesfun6c :::"Integral"::: ) "(" (Set (Var "M")) "," (Set (Var "f")) ")" ")" ) ($#k17_complex1 :::".|"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_mesfunc6 :::"Integral"::: ) "(" (Set (Var "M")) "," (Set ($#k55_valued_1 :::"|."::: ) (Set (Var "f")) ($#k55_valued_1 :::".|"::: ) ) ")" )))))) ; definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "X")); let "M" be ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Const "S")); let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ); let "B" be ($#m2_subset_1 :::"Element"::: ) "of" (Set (Const "S")); func :::"Integral_on"::: "(" "M" "," "B" "," "f" ")" -> ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) equals :: MESFUN6C:def 5 (Set ($#k1_mesfun6c :::"Integral"::: ) "(" "M" "," (Set "(" "f" ($#k2_partfun1 :::"|"::: ) "B" ")" ) ")" ); end; :: deftheorem defines :::"Integral_on"::: MESFUN6C:def 5 : (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "B")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "holds" (Bool (Set ($#k3_mesfun6c :::"Integral_on"::: ) "(" (Set (Var "M")) "," (Set (Var "B")) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_mesfun6c :::"Integral"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "B")) ")" ) ")" ))))))); theorem :: MESFUN6C: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 "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"::: ) ) (Bool "for" (Set (Var "B")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "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"))) & (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k2_valued_1 :::"+"::: ) (Set (Var "g")) ")" )))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k2_valued_1 :::"+"::: ) (Set (Var "g"))) ($#r2_mesfun6c :::"is_integrable_on"::: ) (Set (Var "M"))) & (Bool (Set ($#k3_mesfun6c :::"Integral_on"::: ) "(" (Set (Var "M")) "," (Set (Var "B")) "," (Set "(" (Set (Var "f")) ($#k2_valued_1 :::"+"::: ) (Set (Var "g")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_mesfun6c :::"Integral_on"::: ) "(" (Set (Var "M")) "," (Set (Var "B")) "," (Set (Var "f")) ")" ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k3_mesfun6c :::"Integral_on"::: ) "(" (Set (Var "M")) "," (Set (Var "B")) "," (Set (Var "g")) ")" ")" ))) ")" )))))) ; theorem :: MESFUN6C: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 "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"::: ) ) (Bool "for" (Set (Var "c")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "B")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "f")) ($#r2_mesfun6c :::"is_integrable_on"::: ) (Set (Var "M")))) "holds" (Bool (Set ($#k3_mesfun6c :::"Integral_on"::: ) "(" (Set (Var "M")) "," (Set (Var "B")) "," (Set "(" (Set (Var "c")) ($#k25_valued_1 :::"(#)"::: ) (Set (Var "f")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "c")) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k3_mesfun6c :::"Integral_on"::: ) "(" (Set (Var "M")) "," (Set (Var "B")) "," (Set (Var "f")) ")" ")" ))))))))) ; begin theorem :: MESFUN6C: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 "A")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "A")) ($#k8_subset_1 :::"/\"::: ) (Set "(" ($#k14_mesfunc1 :::"great_eq_dom"::: ) "(" (Set (Var "f")) "," (Set (Var "a")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k7_subset_1 :::"\"::: ) (Set "(" (Set (Var "A")) ($#k8_subset_1 :::"/\"::: ) (Set "(" ($#k11_mesfunc1 :::"less_dom"::: ) "(" (Set (Var "f")) "," (Set (Var "a")) ")" ")" ) ")" )))))))) ; theorem :: MESFUN6C: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 "A")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "A")) ($#k8_subset_1 :::"/\"::: ) (Set "(" ($#k13_mesfunc1 :::"great_dom"::: ) "(" (Set (Var "f")) "," (Set (Var "a")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k7_subset_1 :::"\"::: ) (Set "(" (Set (Var "A")) ($#k8_subset_1 :::"/\"::: ) (Set "(" ($#k12_mesfunc1 :::"less_eq_dom"::: ) "(" (Set (Var "f")) "," (Set (Var "a")) ")" ")" ) ")" )))))))) ; theorem :: MESFUN6C: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 "A")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "A")) ($#k8_subset_1 :::"/\"::: ) (Set "(" ($#k12_mesfunc1 :::"less_eq_dom"::: ) "(" (Set (Var "f")) "," (Set (Var "a")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k7_subset_1 :::"\"::: ) (Set "(" (Set (Var "A")) ($#k8_subset_1 :::"/\"::: ) (Set "(" ($#k13_mesfunc1 :::"great_dom"::: ) "(" (Set (Var "f")) "," (Set (Var "a")) ")" ")" ) ")" )))))))) ; theorem :: MESFUN6C: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 "A")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set (Set (Var "A")) ($#k8_subset_1 :::"/\"::: ) (Set "(" ($#k10_relat_1 :::"eq_dom"::: ) "(" (Set (Var "f")) "," (Set (Var "a")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k8_subset_1 :::"/\"::: ) (Set "(" ($#k14_mesfunc1 :::"great_eq_dom"::: ) "(" (Set (Var "f")) "," (Set (Var "a")) ")" ")" ) ")" ) ($#k8_subset_1 :::"/\"::: ) (Set "(" ($#k12_mesfunc1 :::"less_eq_dom"::: ) "(" (Set (Var "f")) "," (Set (Var "a")) ")" ")" )))))))) ;