:: MEASURE7 semantic presentation begin theorem :: MEASURE7:1 (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "F")) ($#k12_supinf_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k1_supinf_2 :::"0."::: ) )) ")" )) "holds" (Bool (Set ($#k19_supinf_2 :::"SUM"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k1_supinf_2 :::"0."::: ) ))) ; theorem :: MEASURE7:2 (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool (Set (Var "F")) "is" bbbadV6_SUPINF_2())) "holds" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "F")) ($#k12_supinf_2 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k18_supinf_2 :::"Ser"::: ) (Set (Var "F")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "n")))))) ; theorem :: MEASURE7:3 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "," (Set (Var "H")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool (Set (Var "G")) "is" bbbadV6_SUPINF_2()) & (Bool (Set (Var "H")) "is" bbbadV6_SUPINF_2()) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "F")) ($#k12_supinf_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "G")) ($#k12_supinf_2 :::"."::: ) (Set (Var "n")) ")" ) ($#k3_supinf_2 :::"+"::: ) (Set "(" (Set (Var "H")) ($#k12_supinf_2 :::"."::: ) (Set (Var "n")) ")" ))) ")" )) "holds" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" ($#k18_supinf_2 :::"Ser"::: ) (Set (Var "F")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k18_supinf_2 :::"Ser"::: ) (Set (Var "G")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "n")) ")" ) ($#k3_supinf_2 :::"+"::: ) (Set "(" (Set "(" ($#k18_supinf_2 :::"Ser"::: ) (Set (Var "H")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "n")) ")" ))))) ; theorem :: MEASURE7:4 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "," (Set (Var "H")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "F")) ($#k12_supinf_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "G")) ($#k12_supinf_2 :::"."::: ) (Set (Var "n")) ")" ) ($#k3_supinf_2 :::"+"::: ) (Set "(" (Set (Var "H")) ($#k12_supinf_2 :::"."::: ) (Set (Var "n")) ")" ))) ")" ) & (Bool (Set (Var "G")) "is" bbbadV6_SUPINF_2()) & (Bool (Set (Var "H")) "is" bbbadV6_SUPINF_2())) "holds" (Bool (Set ($#k19_supinf_2 :::"SUM"::: ) (Set (Var "F"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k19_supinf_2 :::"SUM"::: ) (Set (Var "G")) ")" ) ($#k3_supinf_2 :::"+"::: ) (Set "(" ($#k19_supinf_2 :::"SUM"::: ) (Set (Var "H")) ")" )))) ; theorem :: MEASURE7:5 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "F")) ($#k12_supinf_2 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "G")) ($#k12_supinf_2 :::"."::: ) (Set (Var "n")))) ")" )) "holds" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" ($#k18_supinf_2 :::"Ser"::: ) (Set (Var "F")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k19_supinf_2 :::"SUM"::: ) (Set (Var "G")))))) ; theorem :: MEASURE7:6 (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool (Set (Var "F")) "is" bbbadV6_SUPINF_2())) "holds" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" ($#k18_supinf_2 :::"Ser"::: ) (Set (Var "F")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k19_supinf_2 :::"SUM"::: ) (Set (Var "F")))))) ; definitionlet "S" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "H" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "S")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ); func :::"On"::: "H" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) means :: MEASURE7:def 1 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) "S")) "implies" (Bool (Set it ($#k12_supinf_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set "H" ($#k12_supinf_2 :::"."::: ) (Set (Var "n")))) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "n")) ($#r2_hidden :::"in"::: ) "S"))) "implies" (Bool (Set it ($#k12_supinf_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k1_supinf_2 :::"0."::: ) )) ")" ")" )); end; :: deftheorem defines :::"On"::: MEASURE7:def 1 : (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k1_measure7 :::"On"::: ) (Set (Var "H")))) "iff" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set (Var "S")))) "implies" (Bool (Set (Set (Var "b3")) ($#k12_supinf_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "H")) ($#k12_supinf_2 :::"."::: ) (Set (Var "n")))) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set (Var "S"))))) "implies" (Bool (Set (Set (Var "b3")) ($#k12_supinf_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k1_supinf_2 :::"0."::: ) )) ")" ")" )) ")" )))); theorem :: MEASURE7:7 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool (Set (Var "G")) "is" bbbadV6_SUPINF_2())) "holds" (Bool (Set ($#k1_measure7 :::"On"::: ) (Set (Var "G"))) "is" bbbadV6_SUPINF_2()))) ; theorem :: MEASURE7:8 (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool (Set (Var "F")) "is" bbbadV6_SUPINF_2())) "holds" (Bool "for" (Set (Var "n")) "," (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k")))) "holds" (Bool (Set (Set "(" ($#k18_supinf_2 :::"Ser"::: ) (Set (Var "F")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k18_supinf_2 :::"Ser"::: ) (Set (Var "F")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "k")))))) ; theorem :: MEASURE7:9 (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_hidden :::"<>"::: ) (Set (Var "k")))) "holds" (Bool (Set (Set (Var "F")) ($#k12_supinf_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k1_supinf_2 :::"0."::: ) )) ")" )) "holds" (Bool "(" (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "k")))) "holds" (Bool (Set (Set "(" ($#k18_supinf_2 :::"Ser"::: ) (Set (Var "F")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k1_supinf_2 :::"0."::: ) )) ")" ) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool (Set (Set "(" ($#k18_supinf_2 :::"Ser"::: ) (Set (Var "F")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k12_supinf_2 :::"."::: ) (Set (Var "k")))) ")" ) ")" ))) ; theorem :: MEASURE7:10 (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool (Set (Var "G")) "is" bbbadV6_SUPINF_2())) "holds" (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "H")) "is" ($#v2_funct_1 :::"one-to-one"::: ) )) "holds" (Bool (Set ($#k19_supinf_2 :::"SUM"::: ) (Set "(" ($#k1_measure7 :::"On"::: ) (Set "(" (Set (Var "G")) ($#k1_partfun1 :::"*"::: ) (Set (Var "H")) ")" ) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k19_supinf_2 :::"SUM"::: ) (Set (Var "G"))))))) ; theorem :: MEASURE7:11 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool (Set (Var "G")) "is" bbbadV6_SUPINF_2())) "holds" (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "H")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool "(" "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set (Var "S")))) "implies" (Bool (Set (Set (Var "F")) ($#k12_supinf_2 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "G")) ($#k1_partfun1 :::"*"::: ) (Set (Var "H")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "k")))) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set (Var "S"))))) "implies" (Bool (Set (Set (Var "F")) ($#k12_supinf_2 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k1_supinf_2 :::"0."::: ) )) ")" ")" ) ")" )) "holds" (Bool (Set ($#k19_supinf_2 :::"SUM"::: ) (Set (Var "F"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k19_supinf_2 :::"SUM"::: ) (Set (Var "G"))))))) ; definitionlet "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ); mode :::"Interval_Covering"::: "of" "A" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) means :: MEASURE7:def 2 (Bool "(" (Bool "A" ($#r1_tarski :::"c="::: ) (Set ($#k5_setfam_1 :::"union"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) it ")" ))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set it ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) "is" ($#m1_subset_1 :::"Interval":::)) ")" ) ")" ); end; :: deftheorem defines :::"Interval_Covering"::: MEASURE7:def 2 : (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m1_measure7 :::"Interval_Covering"::: ) "of" (Set (Var "A"))) "iff" (Bool "(" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set ($#k5_setfam_1 :::"union"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "b2")) ")" ))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "b2")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) "is" ($#m1_subset_1 :::"Interval":::)) ")" ) ")" ) ")" ))); definitionlet "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ); let "F" be ($#m1_measure7 :::"Interval_Covering"::: ) "of" (Set (Const "A")); let "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); :: original: :::"."::: redefine func "F" :::"."::: "n" -> ($#m1_subset_1 :::"Interval":::); end; definitionlet "F" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) ")" ); mode :::"Interval_Covering"::: "of" "F" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) ")" ")" ) means :: MEASURE7:def 3 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set it ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) "is" ($#m1_measure7 :::"Interval_Covering"::: ) "of" (Set "F" ($#k8_nat_1 :::"."::: ) (Set (Var "n"))))); end; :: deftheorem defines :::"Interval_Covering"::: MEASURE7:def 3 : (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) ")" ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m2_measure7 :::"Interval_Covering"::: ) "of" (Set (Var "F"))) "iff" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "b2")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) "is" ($#m1_measure7 :::"Interval_Covering"::: ) "of" (Set (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))))) ")" ))); definitionlet "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ); let "F" be ($#m1_measure7 :::"Interval_Covering"::: ) "of" (Set (Const "A")); func "F" :::"vol"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) means :: MEASURE7:def 4 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set it ($#k12_supinf_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k2_measure5 :::"diameter"::: ) (Set "(" "F" ($#k2_measure7 :::"."::: ) (Set (Var "n")) ")" )))); end; :: deftheorem defines :::"vol"::: MEASURE7:def 4 : (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_measure7 :::"Interval_Covering"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_measure7 :::"vol"::: ) )) "iff" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "b3")) ($#k12_supinf_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k2_measure5 :::"diameter"::: ) (Set "(" (Set (Var "F")) ($#k2_measure7 :::"."::: ) (Set (Var "n")) ")" )))) ")" )))); theorem :: MEASURE7:12 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_measure7 :::"Interval_Covering"::: ) "of" (Set (Var "A")) "holds" (Bool (Set (Set (Var "F")) ($#k3_measure7 :::"vol"::: ) ) "is" bbbadV6_SUPINF_2()))) ; definitionlet "F" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) ")" ); let "H" be ($#m2_measure7 :::"Interval_Covering"::: ) "of" (Set (Const "F")); let "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); :: original: :::"."::: redefine func "H" :::"."::: "n" -> ($#m1_measure7 :::"Interval_Covering"::: ) "of" (Set "F" ($#k8_nat_1 :::"."::: ) "n"); end; definitionlet "F" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) ")" ); let "G" be ($#m2_measure7 :::"Interval_Covering"::: ) "of" (Set (Const "F")); func "G" :::"vol"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) ")" ")" ) means :: MEASURE7:def 5 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set it ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "G" ($#k4_measure7 :::"."::: ) (Set (Var "n")) ")" ) ($#k3_measure7 :::"vol"::: ) ))); end; :: deftheorem defines :::"vol"::: MEASURE7:def 5 : (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) (Bool "for" (Set (Var "G")) "being" ($#m2_measure7 :::"Interval_Covering"::: ) "of" (Set (Var "F")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) ")" ")" ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k5_measure7 :::"vol"::: ) )) "iff" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "b3")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "G")) ($#k4_measure7 :::"."::: ) (Set (Var "n")) ")" ) ($#k3_measure7 :::"vol"::: ) ))) ")" )))); definitionlet "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ); let "F" be ($#m1_measure7 :::"Interval_Covering"::: ) "of" (Set (Const "A")); func :::"vol"::: "F" -> ($#m1_subset_1 :::"R_eal":::) equals :: MEASURE7:def 6 (Set ($#k19_supinf_2 :::"SUM"::: ) (Set "(" "F" ($#k3_measure7 :::"vol"::: ) ")" )); end; :: deftheorem defines :::"vol"::: MEASURE7:def 6 : (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_measure7 :::"Interval_Covering"::: ) "of" (Set (Var "A")) "holds" (Bool (Set ($#k6_measure7 :::"vol"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k19_supinf_2 :::"SUM"::: ) (Set "(" (Set (Var "F")) ($#k3_measure7 :::"vol"::: ) ")" ))))); definitionlet "F" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) ")" ); let "G" be ($#m2_measure7 :::"Interval_Covering"::: ) "of" (Set (Const "F")); func :::"vol"::: "G" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) means :: MEASURE7:def 7 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set it ($#k12_supinf_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k6_measure7 :::"vol"::: ) (Set "(" "G" ($#k4_measure7 :::"."::: ) (Set (Var "n")) ")" )))); end; :: deftheorem defines :::"vol"::: MEASURE7:def 7 : (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) (Bool "for" (Set (Var "G")) "being" ($#m2_measure7 :::"Interval_Covering"::: ) "of" (Set (Var "F")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k7_measure7 :::"vol"::: ) (Set (Var "G")))) "iff" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "b3")) ($#k12_supinf_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k6_measure7 :::"vol"::: ) (Set "(" (Set (Var "G")) ($#k4_measure7 :::"."::: ) (Set (Var "n")) ")" )))) ")" )))); theorem :: MEASURE7:13 (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) (Bool "for" (Set (Var "G")) "being" ($#m2_measure7 :::"Interval_Covering"::: ) "of" (Set (Var "F")) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k1_supinf_2 :::"0."::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k7_measure7 :::"vol"::: ) (Set (Var "G")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "n"))))))) ; definitionlet "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ); func :::"Svc"::: "A" -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) means :: MEASURE7:def 8 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"R_eal":::) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "F")) "being" ($#m1_measure7 :::"Interval_Covering"::: ) "of" "A" "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k6_measure7 :::"vol"::: ) (Set (Var "F"))))) ")" )); end; :: deftheorem defines :::"Svc"::: MEASURE7:def 8 : (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k8_measure7 :::"Svc"::: ) (Set (Var "A")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"R_eal":::) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "iff" (Bool "ex" (Set (Var "F")) "being" ($#m1_measure7 :::"Interval_Covering"::: ) "of" (Set (Var "A")) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k6_measure7 :::"vol"::: ) (Set (Var "F"))))) ")" )) ")" ))); registrationlet "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set ($#k8_measure7 :::"Svc"::: ) "A") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definitionlet "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ); func :::"COMPLEX"::: "A" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) equals :: MEASURE7:def 9 (Set ($#k7_supinf_2 :::"inf"::: ) (Set "(" ($#k8_measure7 :::"Svc"::: ) "A" ")" )); end; :: deftheorem defines :::"COMPLEX"::: MEASURE7:def 9 : (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k9_measure7 :::"COMPLEX"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k7_supinf_2 :::"inf"::: ) (Set "(" ($#k8_measure7 :::"Svc"::: ) (Set (Var "A")) ")" )))); definitionfunc :::"OS_Meas"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) means :: MEASURE7:def 10 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set it ($#k12_supinf_2 :::"."::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k7_supinf_2 :::"inf"::: ) (Set "(" ($#k8_measure7 :::"Svc"::: ) (Set (Var "A")) ")" )))); end; :: deftheorem defines :::"OS_Meas"::: MEASURE7:def 10 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k10_measure7 :::"OS_Meas"::: ) )) "iff" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set (Var "b1")) ($#k12_supinf_2 :::"."::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k7_supinf_2 :::"inf"::: ) (Set "(" ($#k8_measure7 :::"Svc"::: ) (Set (Var "A")) ")" )))) ")" )); definitionlet "F" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) ")" ); let "G" be ($#m2_measure7 :::"Interval_Covering"::: ) "of" (Set (Const "F")); let "H" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k5_numbers :::"NAT"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ); assume (Bool (Set ($#k11_funcop_1 :::"rng"::: ) (Set (Const "H"))) ($#r1_hidden :::"="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k5_numbers :::"NAT"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )) ; func :::"On"::: "(" "G" "," "H" ")" -> ($#m1_measure7 :::"Interval_Covering"::: ) "of" (Set ($#k5_setfam_1 :::"union"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) "F" ")" )) means :: MEASURE7:def 11 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set it ($#k2_measure7 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "G" ($#k4_measure7 :::"."::: ) (Set "(" (Set "(" ($#k4_funct_2 :::"pr1"::: ) "H" ")" ) ($#k1_recdef_1 :::"."::: ) (Set (Var "n")) ")" ) ")" ) ($#k2_measure7 :::"."::: ) (Set "(" (Set "(" ($#k5_funct_2 :::"pr2"::: ) "H" ")" ) ($#k1_recdef_1 :::"."::: ) (Set (Var "n")) ")" )))); end; :: deftheorem defines :::"On"::: MEASURE7:def 11 : (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) (Bool "for" (Set (Var "G")) "being" ($#m2_measure7 :::"Interval_Covering"::: ) "of" (Set (Var "F")) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k5_numbers :::"NAT"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool (Set ($#k11_funcop_1 :::"rng"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k5_numbers :::"NAT"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ))) "holds" (Bool "for" (Set (Var "b4")) "being" ($#m1_measure7 :::"Interval_Covering"::: ) "of" (Set ($#k5_setfam_1 :::"union"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "F")) ")" )) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k11_measure7 :::"On"::: ) "(" (Set (Var "G")) "," (Set (Var "H")) ")" )) "iff" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "b4")) ($#k2_measure7 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "G")) ($#k4_measure7 :::"."::: ) (Set "(" (Set "(" ($#k4_funct_2 :::"pr1"::: ) (Set (Var "H")) ")" ) ($#k1_recdef_1 :::"."::: ) (Set (Var "n")) ")" ) ")" ) ($#k2_measure7 :::"."::: ) (Set "(" (Set "(" ($#k5_funct_2 :::"pr2"::: ) (Set (Var "H")) ")" ) ($#k1_recdef_1 :::"."::: ) (Set (Var "n")) ")" )))) ")" ))))); theorem :: MEASURE7:14 (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k5_numbers :::"NAT"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "H")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set ($#k11_funcop_1 :::"rng"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k5_numbers :::"NAT"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ))) "holds" (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "ex" (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) (Bool "for" (Set (Var "G")) "being" ($#m2_measure7 :::"Interval_Covering"::: ) "of" (Set (Var "F")) "holds" (Bool (Set (Set "(" ($#k18_supinf_2 :::"Ser"::: ) (Set "(" (Set "(" ($#k11_measure7 :::"On"::: ) "(" (Set (Var "G")) "," (Set (Var "H")) ")" ")" ) ($#k3_measure7 :::"vol"::: ) ")" ) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "k"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k18_supinf_2 :::"Ser"::: ) (Set "(" ($#k7_measure7 :::"vol"::: ) (Set (Var "G")) ")" ) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "m"))))))))) ; theorem :: MEASURE7:15 (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) (Bool "for" (Set (Var "G")) "being" ($#m2_measure7 :::"Interval_Covering"::: ) "of" (Set (Var "F")) "holds" (Bool (Set ($#k7_supinf_2 :::"inf"::: ) (Set "(" ($#k8_measure7 :::"Svc"::: ) (Set "(" ($#k5_setfam_1 :::"union"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "F")) ")" ) ")" ) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k19_supinf_2 :::"SUM"::: ) (Set "(" ($#k7_measure7 :::"vol"::: ) (Set (Var "G")) ")" ))))) ; theorem :: MEASURE7:16 (Bool (Set ($#k10_measure7 :::"OS_Meas"::: ) ) "is" ($#m1_measure4 :::"C_Measure"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) )) ; definition:: original: :::"OS_Meas"::: redefine func :::"OS_Meas"::: -> ($#m1_measure4 :::"C_Measure"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ); end; definitionfunc :::"Lmi_sigmaFIELD"::: -> ($#m1_subset_1 :::"SigmaField":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) equals :: MEASURE7:def 12 (Set ($#k1_measure4 :::"sigma_Field"::: ) (Set ($#k12_measure7 :::"OS_Meas"::: ) )); end; :: deftheorem defines :::"Lmi_sigmaFIELD"::: MEASURE7:def 12 : (Bool (Set ($#k13_measure7 :::"Lmi_sigmaFIELD"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_measure4 :::"sigma_Field"::: ) (Set ($#k12_measure7 :::"OS_Meas"::: ) ))); definitionfunc :::"L_mi"::: -> ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set ($#k13_measure7 :::"Lmi_sigmaFIELD"::: ) ) equals :: MEASURE7:def 13 (Set ($#k3_measure4 :::"sigma_Meas"::: ) (Set ($#k12_measure7 :::"OS_Meas"::: ) )); end; :: deftheorem defines :::"L_mi"::: MEASURE7:def 13 : (Bool (Set ($#k14_measure7 :::"L_mi"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k3_measure4 :::"sigma_Meas"::: ) (Set ($#k12_measure7 :::"OS_Meas"::: ) )));