:: MESFUNC1 semantic presentation begin definitionfunc :::"INT-"::: -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) means :: MESFUNC1:def 1 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set (Var "k"))))) ")" )); end; :: deftheorem defines :::"INT-"::: MESFUNC1:def 1 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k1_mesfunc1 :::"INT-"::: ) )) "iff" (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "b1"))) "iff" (Bool "ex" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set (Var "k"))))) ")" )) ")" )); registration cluster (Set ($#k1_mesfunc1 :::"INT-"::: ) ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: MESFUNC1:1 (Bool (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k1_mesfunc1 :::"INT-"::: ) ) ($#r2_tarski :::"are_equipotent"::: ) ) ; theorem :: MESFUNC1:2 (Bool (Set ($#k4_numbers :::"INT"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_mesfunc1 :::"INT-"::: ) ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k5_numbers :::"NAT"::: ) ))) ; theorem :: MESFUNC1:3 (Bool (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k4_numbers :::"INT"::: ) ) ($#r2_tarski :::"are_equipotent"::: ) ) ; definitionlet "n" be ($#m1_hidden :::"Nat":::); func :::"RAT_with_denominator"::: "n" -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_numbers :::"RAT"::: ) ) means :: MESFUNC1:def 2 (Bool "for" (Set (Var "q")) "being" ($#m1_hidden :::"Rational":::) "holds" (Bool "(" (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k7_xcmplx_0 :::"/"::: ) "n"))) ")" )); end; :: deftheorem defines :::"RAT_with_denominator"::: MESFUNC1:def 2 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_numbers :::"RAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k2_mesfunc1 :::"RAT_with_denominator"::: ) (Set (Var "n")))) "iff" (Bool "for" (Set (Var "q")) "being" ($#m1_hidden :::"Rational":::) "holds" (Bool "(" (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "iff" (Bool "ex" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k7_xcmplx_0 :::"/"::: ) (Set (Var "n"))))) ")" )) ")" ))); registrationlet "n" be ($#m1_hidden :::"Nat":::); cluster (Set ($#k2_mesfunc1 :::"RAT_with_denominator"::: ) (Set "(" "n" ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: MESFUNC1:4 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k4_numbers :::"INT"::: ) ) "," (Set ($#k2_mesfunc1 :::"RAT_with_denominator"::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r2_tarski :::"are_equipotent"::: ) )) ; theorem :: MESFUNC1:5 (Bool (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k3_numbers :::"RAT"::: ) ) ($#r2_tarski :::"are_equipotent"::: ) ) ; begin definitionlet "C" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f1", "f2" be (Set (Const "C")) ($#v4_relat_1 :::"-defined"::: ) (Set ($#k7_numbers :::"ExtREAL"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::); func "f1" :::"+"::: "f2" -> ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) means :: MESFUNC1:def 3 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "f1" ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "f2" ")" ) ")" ) ($#k6_subset_1 :::"\"::: ) (Set "(" (Set "(" (Set "(" "f1" ($#k8_relat_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k2_supinf_1 :::"-infty"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" "f2" ($#k8_relat_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_supinf_1 :::"+infty"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set "(" "f1" ($#k8_relat_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_supinf_1 :::"+infty"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" "f2" ($#k8_relat_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k2_supinf_1 :::"-infty"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" ) ")" ) ")" ))) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "C" "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) it))) "holds" (Bool (Set it ($#k12_supinf_2 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "f1" ($#k12_supinf_2 :::"."::: ) (Set (Var "c")) ")" ) ($#k3_supinf_2 :::"+"::: ) (Set "(" "f2" ($#k12_supinf_2 :::"."::: ) (Set (Var "c")) ")" ))) ")" ) ")" ); commutativity (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "C")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" (Set (Const "C")) ($#v4_relat_1 :::"-defined"::: ) (Set ($#k7_numbers :::"ExtREAL"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f1")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f2")) ")" ) ")" ) ($#k6_subset_1 :::"\"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "f1")) ($#k8_relat_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k2_supinf_1 :::"-infty"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" (Set (Var "f2")) ($#k8_relat_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_supinf_1 :::"+infty"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set "(" (Set (Var "f1")) ($#k8_relat_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_supinf_1 :::"+infty"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" (Set (Var "f2")) ($#k8_relat_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k2_supinf_1 :::"-infty"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" ) ")" ) ")" ))) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "C")) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b1"))))) "holds" (Bool (Set (Set (Var "b1")) ($#k12_supinf_2 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f1")) ($#k12_supinf_2 :::"."::: ) (Set (Var "c")) ")" ) ($#k3_supinf_2 :::"+"::: ) (Set "(" (Set (Var "f2")) ($#k12_supinf_2 :::"."::: ) (Set (Var "c")) ")" ))) ")" )) "holds" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f2")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f1")) ")" ) ")" ) ($#k6_subset_1 :::"\"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "f2")) ($#k8_relat_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k2_supinf_1 :::"-infty"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" (Set (Var "f1")) ($#k8_relat_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_supinf_1 :::"+infty"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set "(" (Set (Var "f2")) ($#k8_relat_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_supinf_1 :::"+infty"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" (Set (Var "f1")) ($#k8_relat_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k2_supinf_1 :::"-infty"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" ) ")" ) ")" ))) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "C")) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b1"))))) "holds" (Bool (Set (Set (Var "b1")) ($#k12_supinf_2 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f2")) ($#k12_supinf_2 :::"."::: ) (Set (Var "c")) ")" ) ($#k3_supinf_2 :::"+"::: ) (Set "(" (Set (Var "f1")) ($#k12_supinf_2 :::"."::: ) (Set (Var "c")) ")" ))) ")" ) ")" ))) ; func "f1" :::"-"::: "f2" -> ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) means :: MESFUNC1:def 4 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "f1" ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "f2" ")" ) ")" ) ($#k6_subset_1 :::"\"::: ) (Set "(" (Set "(" (Set "(" "f1" ($#k8_relat_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_supinf_1 :::"+infty"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" "f2" ($#k8_relat_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_supinf_1 :::"+infty"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set "(" "f1" ($#k8_relat_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k2_supinf_1 :::"-infty"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" "f2" ($#k8_relat_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k2_supinf_1 :::"-infty"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" ) ")" ) ")" ))) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "C" "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) it))) "holds" (Bool (Set it ($#k12_supinf_2 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "f1" ($#k12_supinf_2 :::"."::: ) (Set (Var "c")) ")" ) ($#k4_supinf_2 :::"-"::: ) (Set "(" "f2" ($#k12_supinf_2 :::"."::: ) (Set (Var "c")) ")" ))) ")" ) ")" ); func "f1" :::"(#)"::: "f2" -> ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) means :: MESFUNC1:def 5 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "f1" ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "f2" ")" ))) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "C" "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) it))) "holds" (Bool (Set it ($#k12_supinf_2 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "f1" ($#k12_supinf_2 :::"."::: ) (Set (Var "c")) ")" ) ($#k1_extreal1 :::"*"::: ) (Set "(" "f2" ($#k12_supinf_2 :::"."::: ) (Set (Var "c")) ")" ))) ")" ) ")" ); commutativity (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "C")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" (Set (Const "C")) ($#v4_relat_1 :::"-defined"::: ) (Set ($#k7_numbers :::"ExtREAL"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f1")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f2")) ")" ))) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "C")) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b1"))))) "holds" (Bool (Set (Set (Var "b1")) ($#k12_supinf_2 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f1")) ($#k12_supinf_2 :::"."::: ) (Set (Var "c")) ")" ) ($#k1_extreal1 :::"*"::: ) (Set "(" (Set (Var "f2")) ($#k12_supinf_2 :::"."::: ) (Set (Var "c")) ")" ))) ")" )) "holds" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f2")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f1")) ")" ))) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "C")) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b1"))))) "holds" (Bool (Set (Set (Var "b1")) ($#k12_supinf_2 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f2")) ($#k12_supinf_2 :::"."::: ) (Set (Var "c")) ")" ) ($#k1_extreal1 :::"*"::: ) (Set "(" (Set (Var "f1")) ($#k12_supinf_2 :::"."::: ) (Set (Var "c")) ")" ))) ")" ) ")" ))) ; end; :: deftheorem defines :::"+"::: MESFUNC1:def 3 : (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" (Set (Var "b1")) ($#v4_relat_1 :::"-defined"::: ) (Set ($#k7_numbers :::"ExtREAL"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f1")) ($#k3_mesfunc1 :::"+"::: ) (Set (Var "f2")))) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f1")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f2")) ")" ) ")" ) ($#k6_subset_1 :::"\"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "f1")) ($#k8_relat_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k2_supinf_1 :::"-infty"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" (Set (Var "f2")) ($#k8_relat_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_supinf_1 :::"+infty"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set "(" (Set (Var "f1")) ($#k8_relat_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_supinf_1 :::"+infty"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" (Set (Var "f2")) ($#k8_relat_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k2_supinf_1 :::"-infty"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" ) ")" ) ")" ))) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b4"))))) "holds" (Bool (Set (Set (Var "b4")) ($#k12_supinf_2 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f1")) ($#k12_supinf_2 :::"."::: ) (Set (Var "c")) ")" ) ($#k3_supinf_2 :::"+"::: ) (Set "(" (Set (Var "f2")) ($#k12_supinf_2 :::"."::: ) (Set (Var "c")) ")" ))) ")" ) ")" ) ")" )))); :: deftheorem defines :::"-"::: MESFUNC1:def 4 : (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" (Set (Var "b1")) ($#v4_relat_1 :::"-defined"::: ) (Set ($#k7_numbers :::"ExtREAL"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f1")) ($#k4_mesfunc1 :::"-"::: ) (Set (Var "f2")))) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f1")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f2")) ")" ) ")" ) ($#k6_subset_1 :::"\"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "f1")) ($#k8_relat_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_supinf_1 :::"+infty"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" (Set (Var "f2")) ($#k8_relat_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_supinf_1 :::"+infty"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set "(" (Set (Var "f1")) ($#k8_relat_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k2_supinf_1 :::"-infty"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" (Set (Var "f2")) ($#k8_relat_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k2_supinf_1 :::"-infty"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" ) ")" ) ")" ))) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b4"))))) "holds" (Bool (Set (Set (Var "b4")) ($#k12_supinf_2 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f1")) ($#k12_supinf_2 :::"."::: ) (Set (Var "c")) ")" ) ($#k4_supinf_2 :::"-"::: ) (Set "(" (Set (Var "f2")) ($#k12_supinf_2 :::"."::: ) (Set (Var "c")) ")" ))) ")" ) ")" ) ")" )))); :: deftheorem defines :::"(#)"::: MESFUNC1:def 5 : (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" (Set (Var "b1")) ($#v4_relat_1 :::"-defined"::: ) (Set ($#k7_numbers :::"ExtREAL"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f1")) ($#k5_mesfunc1 :::"(#)"::: ) (Set (Var "f2")))) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f1")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f2")) ")" ))) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b4"))))) "holds" (Bool (Set (Set (Var "b4")) ($#k12_supinf_2 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f1")) ($#k12_supinf_2 :::"."::: ) (Set (Var "c")) ")" ) ($#k1_extreal1 :::"*"::: ) (Set "(" (Set (Var "f2")) ($#k12_supinf_2 :::"."::: ) (Set (Var "c")) ")" ))) ")" ) ")" ) ")" )))); definitionlet "C" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be (Set (Const "C")) ($#v4_relat_1 :::"-defined"::: ) (Set ($#k7_numbers :::"ExtREAL"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::); let "r" be ($#m1_subset_1 :::"Real":::); func "r" :::"(#)"::: "f" -> ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) means :: MESFUNC1:def 6 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f")) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "C" "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) it))) "holds" (Bool (Set it ($#k12_supinf_2 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_measure6 :::"R_EAL"::: ) "r" ")" ) ($#k1_extreal1 :::"*"::: ) (Set "(" "f" ($#k12_supinf_2 :::"."::: ) (Set (Var "c")) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"(#)"::: MESFUNC1:def 6 : (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" (Set (Var "b1")) ($#v4_relat_1 :::"-defined"::: ) (Set ($#k7_numbers :::"ExtREAL"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k6_mesfunc1 :::"(#)"::: ) (Set (Var "f")))) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b4"))))) "holds" (Bool (Set (Set (Var "b4")) ($#k12_supinf_2 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_measure6 :::"R_EAL"::: ) (Set (Var "r")) ")" ) ($#k1_extreal1 :::"*"::: ) (Set "(" (Set (Var "f")) ($#k12_supinf_2 :::"."::: ) (Set (Var "c")) ")" ))) ")" ) ")" ) ")" ))))); theorem :: MESFUNC1:6 (Bool "for" (Set (Var "C")) "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 "C")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "r")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "r")) ($#k6_mesfunc1 :::"(#)"::: ) (Set (Var "f")) ")" )))) "holds" (Bool (Set (Set (Var "f")) ($#k12_supinf_2 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "r")) ($#k6_mesfunc1 :::"(#)"::: ) (Set (Var "f")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "c")) ")" ) ($#k2_extreal1 :::"/"::: ) (Set "(" ($#k1_measure6 :::"R_EAL"::: ) (Set (Var "r")) ")" ))))))) ; definitionlet "C" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be (Set (Const "C")) ($#v4_relat_1 :::"-defined"::: ) (Set ($#k7_numbers :::"ExtREAL"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::); func :::"-"::: "f" -> ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) means :: MESFUNC1:def 7 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f")) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "C" "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) it))) "holds" (Bool (Set it ($#k12_supinf_2 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set ($#k2_supinf_2 :::"-"::: ) (Set "(" "f" ($#k12_supinf_2 :::"."::: ) (Set (Var "c")) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"-"::: MESFUNC1:def 7 : (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" (Set (Var "b1")) ($#v4_relat_1 :::"-defined"::: ) (Set ($#k7_numbers :::"ExtREAL"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k7_mesfunc1 :::"-"::: ) (Set (Var "f")))) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b3"))))) "holds" (Bool (Set (Set (Var "b3")) ($#k12_supinf_2 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set ($#k2_supinf_2 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k12_supinf_2 :::"."::: ) (Set (Var "c")) ")" ))) ")" ) ")" ) ")" )))); definitionfunc :::"1."::: -> ($#m1_subset_1 :::"R_eal":::) equals :: MESFUNC1:def 8 (Num 1); end; :: deftheorem defines :::"1."::: MESFUNC1:def 8 : (Bool (Set ($#k8_mesfunc1 :::"1."::: ) ) ($#r1_hidden :::"="::: ) (Num 1)); definitionlet "C" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be (Set (Const "C")) ($#v4_relat_1 :::"-defined"::: ) (Set ($#k7_numbers :::"ExtREAL"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::); let "r" be ($#m1_subset_1 :::"Real":::); func "r" :::"/"::: "f" -> ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) means :: MESFUNC1:def 9 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "f" ")" ) ($#k6_subset_1 :::"\"::: ) (Set "(" "f" ($#k8_relat_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_supinf_2 :::"0."::: ) ) ($#k1_tarski :::"}"::: ) ) ")" ))) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "C" "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) it))) "holds" (Bool (Set it ($#k12_supinf_2 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_measure6 :::"R_EAL"::: ) "r" ")" ) ($#k2_extreal1 :::"/"::: ) (Set "(" "f" ($#k12_supinf_2 :::"."::: ) (Set (Var "c")) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"/"::: MESFUNC1:def 9 : (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" (Set (Var "b1")) ($#v4_relat_1 :::"-defined"::: ) (Set ($#k7_numbers :::"ExtREAL"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k9_mesfunc1 :::"/"::: ) (Set (Var "f")))) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set "(" (Set (Var "f")) ($#k8_relat_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_supinf_2 :::"0."::: ) ) ($#k1_tarski :::"}"::: ) ) ")" ))) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b4"))))) "holds" (Bool (Set (Set (Var "b4")) ($#k12_supinf_2 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_measure6 :::"R_EAL"::: ) (Set (Var "r")) ")" ) ($#k2_extreal1 :::"/"::: ) (Set "(" (Set (Var "f")) ($#k12_supinf_2 :::"."::: ) (Set (Var "c")) ")" ))) ")" ) ")" ) ")" ))))); theorem :: MESFUNC1:7 (Bool "for" (Set (Var "C")) "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 "C")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "holds" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Num 1) ($#k9_mesfunc1 :::"/"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set "(" (Set (Var "f")) ($#k8_relat_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_supinf_2 :::"0."::: ) ) ($#k1_tarski :::"}"::: ) ) ")" ))) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Num 1) ($#k9_mesfunc1 :::"/"::: ) (Set (Var "f")) ")" )))) "holds" (Bool (Set (Set "(" (Num 1) ($#k9_mesfunc1 :::"/"::: ) (Set (Var "f")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k8_mesfunc1 :::"1."::: ) ) ($#k2_extreal1 :::"/"::: ) (Set "(" (Set (Var "f")) ($#k12_supinf_2 :::"."::: ) (Set (Var "c")) ")" ))) ")" ) ")" ))) ; definitionlet "C" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be (Set (Const "C")) ($#v4_relat_1 :::"-defined"::: ) (Set ($#k7_numbers :::"ExtREAL"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::); func :::"|.":::"f":::".|"::: -> ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) means :: MESFUNC1:def 10 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f")) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "C" "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) it))) "holds" (Bool (Set it ($#k12_supinf_2 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set ($#k3_extreal1 :::"|."::: ) (Set "(" "f" ($#k12_supinf_2 :::"."::: ) (Set (Var "c")) ")" ) ($#k3_extreal1 :::".|"::: ) )) ")" ) ")" ); end; :: deftheorem defines :::"|."::: MESFUNC1:def 10 : (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" (Set (Var "b1")) ($#v4_relat_1 :::"-defined"::: ) (Set ($#k7_numbers :::"ExtREAL"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k10_mesfunc1 :::"|."::: ) (Set (Var "f")) ($#k10_mesfunc1 :::".|"::: ) )) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b3"))))) "holds" (Bool (Set (Set (Var "b3")) ($#k12_supinf_2 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set ($#k3_extreal1 :::"|."::: ) (Set "(" (Set (Var "f")) ($#k12_supinf_2 :::"."::: ) (Set (Var "c")) ")" ) ($#k3_extreal1 :::".|"::: ) )) ")" ) ")" ) ")" )))); begin theorem :: MESFUNC1:8 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "ex" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))))) ; theorem :: MESFUNC1:9 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "ex" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Set ($#k1_real_1 :::"-"::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))))) ; theorem :: MESFUNC1:10 (Bool "for" (Set (Var "r")) "," (Set (Var "s")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "s")))) "holds" (Bool "ex" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Set (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "s")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "r")))))) ; theorem :: MESFUNC1:11 (Bool "for" (Set (Var "r")) "," (Set (Var "s")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "r")) ($#k5_real_1 :::"-"::: ) (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "s"))) ")" )) "holds" (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "s")))) ; theorem :: MESFUNC1:12 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"R_eal":::) "st" (Bool (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set ($#k1_measure6 :::"R_EAL"::: ) (Set (Var "r"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "a"))) ")" )) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k1_supinf_1 :::"+infty"::: ) ))) ; theorem :: MESFUNC1:13 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"R_eal":::) "st" (Bool (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_measure6 :::"R_EAL"::: ) (Set (Var "r")))) ")" )) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k2_supinf_1 :::"-infty"::: ) ))) ; notationlet "f" be ($#v2_valued_0 :::"ext-real-valued"::: ) ($#m1_hidden :::"Function":::); let "a" be ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) ; synonym :::"eq_dom"::: "(" "f" "," "a" ")" for :::"Coim"::: "(" "f" "," "a" ")" ; end; definitionlet "f" be ($#v2_valued_0 :::"ext-real-valued"::: ) ($#m1_hidden :::"Function":::); let "a" be ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) ; func :::"less_dom"::: "(" "f" "," "a" ")" -> ($#m1_hidden :::"set"::: ) means :: MESFUNC1:def 11 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f")) & (Bool (Set "f" ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<"::: ) "a") ")" ) ")" )); func :::"less_eq_dom"::: "(" "f" "," "a" ")" -> ($#m1_hidden :::"set"::: ) means :: MESFUNC1:def 12 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f")) & (Bool (Set "f" ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<="::: ) "a") ")" ) ")" )); func :::"great_dom"::: "(" "f" "," "a" ")" -> ($#m1_hidden :::"set"::: ) means :: MESFUNC1:def 13 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f")) & (Bool "a" ($#r1_xxreal_0 :::"<"::: ) (Set "f" ($#k12_supinf_2 :::"."::: ) (Set (Var "x")))) ")" ) ")" )); func :::"great_eq_dom"::: "(" "f" "," "a" ")" -> ($#m1_hidden :::"set"::: ) means :: MESFUNC1:def 14 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f")) & (Bool "a" ($#r1_xxreal_0 :::"<="::: ) (Set "f" ($#k12_supinf_2 :::"."::: ) (Set (Var "x")))) ")" ) ")" )); redefine func :::"Coim"::: "(" "f" "," "a" ")" means :: MESFUNC1:def 15 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f")) & (Bool (Set "f" ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) "a") ")" ) ")" )); end; :: deftheorem defines :::"less_dom"::: MESFUNC1:def 11 : (Bool "for" (Set (Var "f")) "being" ($#v2_valued_0 :::"ext-real-valued"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "a")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k11_mesfunc1 :::"less_dom"::: ) "(" (Set (Var "f")) "," (Set (Var "a")) ")" )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Set (Var "f")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "a"))) ")" ) ")" )) ")" )))); :: deftheorem defines :::"less_eq_dom"::: MESFUNC1:def 12 : (Bool "for" (Set (Var "f")) "being" ($#v2_valued_0 :::"ext-real-valued"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "a")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k12_mesfunc1 :::"less_eq_dom"::: ) "(" (Set (Var "f")) "," (Set (Var "a")) ")" )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Set (Var "f")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "a"))) ")" ) ")" )) ")" )))); :: deftheorem defines :::"great_dom"::: MESFUNC1:def 13 : (Bool "for" (Set (Var "f")) "being" ($#v2_valued_0 :::"ext-real-valued"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "a")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k13_mesfunc1 :::"great_dom"::: ) "(" (Set (Var "f")) "," (Set (Var "a")) ")" )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "f")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x")))) ")" ) ")" )) ")" )))); :: deftheorem defines :::"great_eq_dom"::: MESFUNC1:def 14 : (Bool "for" (Set (Var "f")) "being" ($#v2_valued_0 :::"ext-real-valued"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "a")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k14_mesfunc1 :::"great_eq_dom"::: ) "(" (Set (Var "f")) "," (Set (Var "a")) ")" )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "f")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x")))) ")" ) ")" )) ")" )))); :: deftheorem defines :::"eq_dom"::: MESFUNC1:def 15 : (Bool "for" (Set (Var "f")) "being" ($#v2_valued_0 :::"ext-real-valued"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "a")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k10_relat_1 :::"eq_dom"::: ) "(" (Set (Var "f")) "," (Set (Var "a")) ")" )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Set (Var "f")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) ")" ) ")" )) ")" )))); definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ); let "a" be ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) ; :: original: :::"less_dom"::: redefine func :::"less_dom"::: "(" "f" "," "a" ")" -> ($#m1_subset_1 :::"Subset":::) "of" "X"; :: original: :::"less_eq_dom"::: redefine func :::"less_eq_dom"::: "(" "f" "," "a" ")" -> ($#m1_subset_1 :::"Subset":::) "of" "X"; :: original: :::"great_dom"::: redefine func :::"great_dom"::: "(" "f" "," "a" ")" -> ($#m1_subset_1 :::"Subset":::) "of" "X"; :: original: :::"great_eq_dom"::: redefine func :::"great_eq_dom"::: "(" "f" "," "a" ")" -> ($#m1_subset_1 :::"Subset":::) "of" "X"; :: original: :::"eq_dom"::: redefine func :::"eq_dom"::: "(" "f" "," "a" ")" -> ($#m1_subset_1 :::"Subset":::) "of" "X"; end; theorem :: MESFUNC1:14 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"R_eal":::) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k18_mesfunc1 :::"great_eq_dom"::: ) "(" (Set (Var "f")) "," (Set (Var "a")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k6_subset_1 :::"\"::: ) (Set "(" (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k15_mesfunc1 :::"less_dom"::: ) "(" (Set (Var "f")) "," (Set (Var "a")) ")" ")" ) ")" ))))))) ; theorem :: MESFUNC1:15 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"R_eal":::) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k17_mesfunc1 :::"great_dom"::: ) "(" (Set (Var "f")) "," (Set (Var "a")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k6_subset_1 :::"\"::: ) (Set "(" (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k16_mesfunc1 :::"less_eq_dom"::: ) "(" (Set (Var "f")) "," (Set (Var "a")) ")" ")" ) ")" ))))))) ; theorem :: MESFUNC1:16 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"R_eal":::) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k16_mesfunc1 :::"less_eq_dom"::: ) "(" (Set (Var "f")) "," (Set (Var "a")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k6_subset_1 :::"\"::: ) (Set "(" (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k17_mesfunc1 :::"great_dom"::: ) "(" (Set (Var "f")) "," (Set (Var "a")) ")" ")" ) ")" ))))))) ; theorem :: MESFUNC1:17 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"R_eal":::) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k15_mesfunc1 :::"less_dom"::: ) "(" (Set (Var "f")) "," (Set (Var "a")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k6_subset_1 :::"\"::: ) (Set "(" (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k18_mesfunc1 :::"great_eq_dom"::: ) "(" (Set (Var "f")) "," (Set (Var "a")) ")" ")" ) ")" ))))))) ; theorem :: MESFUNC1:18 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"R_eal":::) "holds" (Bool (Set (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k19_mesfunc1 :::"eq_dom"::: ) "(" (Set (Var "f")) "," (Set (Var "a")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k18_mesfunc1 :::"great_eq_dom"::: ) "(" (Set (Var "f")) "," (Set (Var "a")) ")" ")" ) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k16_mesfunc1 :::"less_eq_dom"::: ) "(" (Set (Var "f")) "," (Set (Var "a")) ")" ")" ))))))) ; theorem :: MESFUNC1:19 (Bool "for" (Set (Var "X")) "being" ($#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 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (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" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k17_mesfunc1 :::"great_dom"::: ) "(" (Set (Var "f")) "," (Set "(" ($#k1_measure6 :::"R_EAL"::: ) (Set "(" (Set (Var "r")) ($#k9_real_1 :::"-"::: ) (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ")" ) ")" ")" ))) ")" )) "holds" (Bool (Set (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k18_mesfunc1 :::"great_eq_dom"::: ) "(" (Set (Var "f")) "," (Set "(" ($#k1_measure6 :::"R_EAL"::: ) (Set (Var "r")) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_measure2 :::"meet"::: ) (Set "(" ($#k1_measure3 :::"rng"::: ) (Set (Var "F")) ")" ))))))))) ; theorem :: MESFUNC1:20 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set (Var "S")) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k15_mesfunc1 :::"less_dom"::: ) "(" (Set (Var "f")) "," (Set "(" ($#k1_measure6 :::"R_EAL"::: ) (Set "(" (Set (Var "r")) ($#k3_real_1 :::"+"::: ) (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ")" ) ")" ")" ))) ")" )) "holds" (Bool (Set (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k16_mesfunc1 :::"less_eq_dom"::: ) "(" (Set (Var "f")) "," (Set "(" ($#k1_measure6 :::"R_EAL"::: ) (Set (Var "r")) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_measure2 :::"meet"::: ) (Set "(" ($#k1_measure3 :::"rng"::: ) (Set (Var "F")) ")" ))))))))) ; theorem :: MESFUNC1:21 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set (Var "S")) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k16_mesfunc1 :::"less_eq_dom"::: ) "(" (Set (Var "f")) "," (Set "(" ($#k1_measure6 :::"R_EAL"::: ) (Set "(" (Set (Var "r")) ($#k5_real_1 :::"-"::: ) (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ")" ) ")" ")" ))) ")" )) "holds" (Bool (Set (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k15_mesfunc1 :::"less_dom"::: ) "(" (Set (Var "f")) "," (Set "(" ($#k1_measure6 :::"R_EAL"::: ) (Set (Var "r")) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_measure2 :::"union"::: ) (Set "(" ($#k1_measure3 :::"rng"::: ) (Set (Var "F")) ")" ))))))))) ; theorem :: MESFUNC1:22 (Bool "for" (Set (Var "X")) "being" ($#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 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (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" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k18_mesfunc1 :::"great_eq_dom"::: ) "(" (Set (Var "f")) "," (Set "(" ($#k1_measure6 :::"R_EAL"::: ) (Set "(" (Set (Var "r")) ($#k7_real_1 :::"+"::: ) (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ")" ) ")" ")" ))) ")" )) "holds" (Bool (Set (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k17_mesfunc1 :::"great_dom"::: ) "(" (Set (Var "f")) "," (Set "(" ($#k1_measure6 :::"R_EAL"::: ) (Set (Var "r")) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_measure2 :::"union"::: ) (Set "(" ($#k1_measure3 :::"rng"::: ) (Set (Var "F")) ")" ))))))))) ; theorem :: MESFUNC1:23 (Bool "for" (Set (Var "X")) "being" ($#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 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (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" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k17_mesfunc1 :::"great_dom"::: ) "(" (Set (Var "f")) "," (Set "(" ($#k1_measure6 :::"R_EAL"::: ) (Set (Var "n")) ")" ) ")" ")" ))) ")" )) "holds" (Bool (Set (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k19_mesfunc1 :::"eq_dom"::: ) "(" (Set (Var "f")) "," (Set ($#k1_supinf_1 :::"+infty"::: ) ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_measure2 :::"meet"::: ) (Set "(" ($#k1_measure3 :::"rng"::: ) (Set (Var "F")) ")" )))))))) ; theorem :: MESFUNC1:24 (Bool "for" (Set (Var "X")) "being" ($#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 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (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" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k15_mesfunc1 :::"less_dom"::: ) "(" (Set (Var "f")) "," (Set "(" ($#k1_measure6 :::"R_EAL"::: ) (Set (Var "n")) ")" ) ")" ")" ))) ")" )) "holds" (Bool (Set (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k15_mesfunc1 :::"less_dom"::: ) "(" (Set (Var "f")) "," (Set ($#k1_supinf_1 :::"+infty"::: ) ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_measure2 :::"union"::: ) (Set "(" ($#k1_measure3 :::"rng"::: ) (Set (Var "F")) ")" )))))))) ; theorem :: MESFUNC1:25 (Bool "for" (Set (Var "X")) "being" ($#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 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (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" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k15_mesfunc1 :::"less_dom"::: ) "(" (Set (Var "f")) "," (Set "(" ($#k1_measure6 :::"R_EAL"::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "n")) ")" ) ")" ) ")" ")" ))) ")" )) "holds" (Bool (Set (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k19_mesfunc1 :::"eq_dom"::: ) "(" (Set (Var "f")) "," (Set ($#k2_supinf_1 :::"-infty"::: ) ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_measure2 :::"meet"::: ) (Set "(" ($#k1_measure3 :::"rng"::: ) (Set (Var "F")) ")" )))))))) ; theorem :: MESFUNC1:26 (Bool "for" (Set (Var "X")) "being" ($#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 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (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" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k17_mesfunc1 :::"great_dom"::: ) "(" (Set (Var "f")) "," (Set "(" ($#k1_measure6 :::"R_EAL"::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "n")) ")" ) ")" ) ")" ")" ))) ")" )) "holds" (Bool (Set (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k17_mesfunc1 :::"great_dom"::: ) "(" (Set (Var "f")) "," (Set ($#k2_supinf_1 :::"-infty"::: ) ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_measure2 :::"union"::: ) (Set "(" ($#k1_measure3 :::"rng"::: ) (Set (Var "F")) ")" )))))))) ; 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 ($#k7_numbers :::"ExtREAL"::: ) ); let "A" be ($#m2_subset_1 :::"Element"::: ) "of" (Set (Const "S")); pred "f" :::"is_measurable_on"::: "A" means :: MESFUNC1:def 16 (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set "A" ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k15_mesfunc1 :::"less_dom"::: ) "(" "f" "," (Set "(" ($#k1_measure6 :::"R_EAL"::: ) (Set (Var "r")) ")" ) ")" ")" )) ($#r2_hidden :::"in"::: ) "S")); end; :: deftheorem defines :::"is_measurable_on"::: MESFUNC1:def 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 ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "A"))) "iff" (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k15_mesfunc1 :::"less_dom"::: ) "(" (Set (Var "f")) "," (Set "(" ($#k1_measure6 :::"R_EAL"::: ) (Set (Var "r")) ")" ) ")" ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "S")))) ")" ))))); theorem :: MESFUNC1: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" ($#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 (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "A"))) "iff" (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k18_mesfunc1 :::"great_eq_dom"::: ) "(" (Set (Var "f")) "," (Set "(" ($#k1_measure6 :::"R_EAL"::: ) (Set (Var "r")) ")" ) ")" ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "S")))) ")" ))))) ; theorem :: MESFUNC1: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 "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")) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "A"))) "iff" (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k16_mesfunc1 :::"less_eq_dom"::: ) "(" (Set (Var "f")) "," (Set "(" ($#k1_measure6 :::"R_EAL"::: ) (Set (Var "r")) ")" ) ")" ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "S")))) ")" ))))) ; theorem :: MESFUNC1: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 ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "A")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "A"))) "iff" (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k17_mesfunc1 :::"great_dom"::: ) "(" (Set (Var "f")) "," (Set "(" ($#k1_measure6 :::"R_EAL"::: ) (Set (Var "r")) ")" ) ")" ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "S")))) ")" ))))) ; theorem :: MESFUNC1: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 ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "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_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "A")))) "holds" (Bool (Set (Var "f")) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "B"))))))) ; theorem :: MESFUNC1: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 "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "f")) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "A"))) & (Bool (Set (Var "f")) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "B")))) "holds" (Bool (Set (Var "f")) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Set (Var "A")) ($#k6_prob_1 :::"\/"::: ) (Set (Var "B")))))))) ; theorem :: MESFUNC1: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 "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")) (Bool "for" (Set (Var "r")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "f")) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "A"))) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k17_mesfunc1 :::"great_dom"::: ) "(" (Set (Var "f")) "," (Set "(" ($#k1_measure6 :::"R_EAL"::: ) (Set (Var "r")) ")" ) ")" ")" ) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k15_mesfunc1 :::"less_dom"::: ) "(" (Set (Var "f")) "," (Set "(" ($#k1_measure6 :::"R_EAL"::: ) (Set (Var "s")) ")" ) ")" ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "S")))))))) ; theorem :: MESFUNC1: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")) "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 (Set (Var "f")) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "A"))) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k19_mesfunc1 :::"eq_dom"::: ) "(" (Set (Var "f")) "," (Set ($#k1_supinf_1 :::"+infty"::: ) ) ")" ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "S"))))))) ; theorem :: MESFUNC1: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 "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 (Set (Var "f")) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "A")))) "holds" (Bool (Set (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k19_mesfunc1 :::"eq_dom"::: ) "(" (Set (Var "f")) "," (Set ($#k2_supinf_1 :::"-infty"::: ) ) ")" ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "S"))))))) ; theorem :: MESFUNC1: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 "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 (Set (Var "f")) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "A"))) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k17_mesfunc1 :::"great_dom"::: ) "(" (Set (Var "f")) "," (Set ($#k2_supinf_1 :::"-infty"::: ) ) ")" ")" ) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k15_mesfunc1 :::"less_dom"::: ) "(" (Set (Var "f")) "," (Set ($#k1_supinf_1 :::"+infty"::: ) ) ")" ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "S"))))))) ; theorem :: MESFUNC1: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 "f")) "," (Set (Var "g")) "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")) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "f")) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "A"))) & (Bool (Set (Var "g")) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "A"))) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g"))))) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k15_mesfunc1 :::"less_dom"::: ) "(" (Set (Var "f")) "," (Set "(" ($#k1_measure6 :::"R_EAL"::: ) (Set (Var "r")) ")" ) ")" ")" ) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k17_mesfunc1 :::"great_dom"::: ) "(" (Set (Var "g")) "," (Set "(" ($#k1_measure6 :::"R_EAL"::: ) (Set (Var "r")) ")" ) ")" ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "S")))))))) ; theorem :: MESFUNC1: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 "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")) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "f")) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "A"))) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "r")) ($#k6_mesfunc1 :::"(#)"::: ) (Set (Var "f"))) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "A")))))))) ;