:: MESFUNC8 semantic presentation begin theorem :: MESFUNC8:1 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set (Var "S")) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "{" (Set (Var "x")) where x "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) : (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k")))) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set (Var "k"))))) "}" "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")))))))) ; theorem :: MESFUNC8:2 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k4_setlim_1 :::"superior_setsequence"::: ) (Set (Var "F")) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k5_setfam_1 :::"union"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set "(" (Set (Var "F")) ($#k10_nat_1 :::"^\"::: ) (Set (Var "n")) ")" ) ")" ))) & (Bool (Set (Set "(" ($#k2_setlim_1 :::"inferior_setsequence"::: ) (Set (Var "F")) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k6_setfam_1 :::"meet"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set "(" (Set (Var "F")) ($#k10_nat_1 :::"^\"::: ) (Set (Var "n")) ")" ) ")" ))) ")" )))) ; theorem :: MESFUNC8:3 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "S")) (Bool "ex" (Set (Var "G")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set (Var "S")) "st" (Bool "(" (Bool (Set (Var "G")) ($#r1_funct_2 :::"="::: ) (Set ($#k5_setlim_1 :::"inferior_setsequence"::: ) (Set (Var "F")))) & (Bool (Set (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set "(" ($#k3_kurato_0 :::"lim_inf"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k8_supinf_2 :::"sup"::: ) (Set "(" ($#k17_supinf_2 :::"rng"::: ) (Set "(" (Set (Var "M")) ($#k1_partfun1 :::"*"::: ) (Set (Var "G")) ")" ) ")" ))) ")" )))))) ; theorem :: MESFUNC8:4 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set "(" ($#k3_card_3 :::"Union"::: ) (Set (Var "F")) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_xxreal_0 :::"+infty"::: ) ))) "holds" (Bool "ex" (Set (Var "G")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set (Var "S")) "st" (Bool "(" (Bool (Set (Var "G")) ($#r1_funct_2 :::"="::: ) (Set ($#k6_setlim_1 :::"superior_setsequence"::: ) (Set (Var "F")))) & (Bool (Set (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set "(" ($#k4_kurato_0 :::"lim_sup"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k7_supinf_2 :::"inf"::: ) (Set "(" ($#k17_supinf_2 :::"rng"::: ) (Set "(" (Set (Var "M")) ($#k1_partfun1 :::"*"::: ) (Set (Var "G")) ")" ) ")" ))) ")" )))))) ; theorem :: MESFUNC8:5 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v3_kurato_0 :::"convergent"::: ) )) "holds" (Bool "ex" (Set (Var "G")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set (Var "S")) "st" (Bool "(" (Bool (Set (Var "G")) ($#r1_funct_2 :::"="::: ) (Set ($#k5_setlim_1 :::"inferior_setsequence"::: ) (Set (Var "F")))) & (Bool (Set (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set "(" ($#k4_kurato_0 :::"lim"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k8_supinf_2 :::"sup"::: ) (Set "(" ($#k17_supinf_2 :::"rng"::: ) (Set "(" (Set (Var "M")) ($#k1_partfun1 :::"*"::: ) (Set (Var "G")) ")" ) ")" ))) ")" )))))) ; theorem :: MESFUNC8:6 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v3_kurato_0 :::"convergent"::: ) ) & (Bool (Set (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set "(" ($#k3_card_3 :::"Union"::: ) (Set (Var "F")) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_xxreal_0 :::"+infty"::: ) ))) "holds" (Bool "ex" (Set (Var "G")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set (Var "S")) "st" (Bool "(" (Bool (Set (Var "G")) ($#r1_funct_2 :::"="::: ) (Set ($#k6_setlim_1 :::"superior_setsequence"::: ) (Set (Var "F")))) & (Bool (Set (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set "(" ($#k4_kurato_0 :::"lim"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k7_supinf_2 :::"inf"::: ) (Set "(" ($#k17_supinf_2 :::"rng"::: ) (Set "(" (Set (Var "M")) ($#k1_partfun1 :::"*"::: ) (Set (Var "G")) ")" ) ")" ))) ")" )))))) ; definitionlet "X", "Y" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Const "X")) "," (Set (Const "Y")); attr "F" is :::"with_the_same_dom"::: means :: MESFUNC8:def 1 (Bool (Set ($#k2_relset_1 :::"rng"::: ) "F") "is" ($#v2_card_3 :::"with_common_domain"::: ) ); end; :: deftheorem defines :::"with_the_same_dom"::: MESFUNC8:def 1 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ) "iff" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "F"))) "is" ($#v2_card_3 :::"with_common_domain"::: ) ) ")" ))); definitionlet "X", "Y" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Const "X")) "," (Set (Const "Y")); redefine attr "F" is :::"with_the_same_dom"::: means :: MESFUNC8:def 2 (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" "F" ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" "F" ($#k4_mesfunc5 :::"."::: ) (Set (Var "m")) ")" )))); end; :: deftheorem defines :::"with_the_same_dom"::: MESFUNC8:def 2 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ) "iff" (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "m")) ")" )))) ")" ))); registrationlet "X", "Y" be ($#m1_hidden :::"set"::: ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set ($#k4_partfun1 :::"PFuncs"::: ) "(" "X" "," "Y" ")" ) ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_partfun1 :::"total"::: ) bbbadV1_FUNCT_2((Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k4_partfun1 :::"PFuncs"::: ) "(" "X" "," "Y" ")" )) ($#v1_mesfunc8 :::"with_the_same_dom"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k4_partfun1 :::"PFuncs"::: ) "(" "X" "," "Y" ")" ")" ) ($#k2_zfmisc_1 :::":]"::: ) )); end; definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Const "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ); func :::"inf"::: "f" -> ($#m1_subset_1 :::"PartFunc":::) "of" "X" "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) means :: MESFUNC8:def 3 (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" "f" ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "X" "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) it))) "holds" (Bool (Set it ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k2_rinfsup2 :::"inf"::: ) (Set "(" "f" ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x")) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"inf"::: MESFUNC8:def 3 : (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k1_mesfunc8 :::"inf"::: ) (Set (Var "f")))) "iff" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "b3"))))) "holds" (Bool (Set (Set (Var "b3")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k2_rinfsup2 :::"inf"::: ) (Set "(" (Set (Var "f")) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x")) ")" ))) ")" ) ")" ) ")" )))); definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Const "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ); func :::"sup"::: "f" -> ($#m1_subset_1 :::"PartFunc":::) "of" "X" "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) means :: MESFUNC8:def 4 (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" "f" ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "X" "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) it))) "holds" (Bool (Set it ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_rinfsup2 :::"sup"::: ) (Set "(" "f" ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x")) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"sup"::: MESFUNC8:def 4 : (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k2_mesfunc8 :::"sup"::: ) (Set (Var "f")))) "iff" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "b3"))))) "holds" (Bool (Set (Set (Var "b3")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_rinfsup2 :::"sup"::: ) (Set "(" (Set (Var "f")) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x")) ")" ))) ")" ) ")" ) ")" )))); definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Const "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ); func :::"inferior_realsequence"::: "f" -> ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ($#m1_subset_1 :::"Functional_Sequence":::) "of" "X" "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) means :: MESFUNC8:def 5 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" it ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" "f" ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "X" "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" it ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" )))) "holds" (Bool (Set (Set "(" it ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_rinfsup2 :::"inferior_realsequence"::: ) (Set "(" "f" ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x")) ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n")))) ")" ) ")" )); end; :: deftheorem defines :::"inferior_realsequence"::: MESFUNC8:def 5 : (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "b3")) "being" ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k3_mesfunc8 :::"inferior_realsequence"::: ) (Set (Var "f")))) "iff" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "b3")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "b3")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" )))) "holds" (Bool (Set (Set "(" (Set (Var "b3")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_rinfsup2 :::"inferior_realsequence"::: ) (Set "(" (Set (Var "f")) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x")) ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n")))) ")" ) ")" )) ")" )))); definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Const "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ); func :::"superior_realsequence"::: "f" -> ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ($#m1_subset_1 :::"Functional_Sequence":::) "of" "X" "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) means :: MESFUNC8:def 6 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" it ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" "f" ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "X" "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" it ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" )))) "holds" (Bool (Set (Set "(" it ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_rinfsup2 :::"superior_realsequence"::: ) (Set "(" "f" ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x")) ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n")))) ")" ) ")" )); end; :: deftheorem defines :::"superior_realsequence"::: MESFUNC8:def 6 : (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "b3")) "being" ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k4_mesfunc8 :::"superior_realsequence"::: ) (Set (Var "f")))) "iff" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "b3")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "b3")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" )))) "holds" (Bool (Set (Set "(" (Set (Var "b3")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_rinfsup2 :::"superior_realsequence"::: ) (Set "(" (Set (Var "f")) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x")) ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n")))) ")" ) ")" )) ")" )))); theorem :: MESFUNC8:7 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )))) "holds" (Bool (Set (Set "(" ($#k3_mesfunc8 :::"inferior_realsequence"::: ) (Set (Var "f")) ")" ) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x"))) ($#r2_funct_2 :::"="::: ) (Set ($#k3_rinfsup2 :::"inferior_realsequence"::: ) (Set "(" (Set (Var "f")) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x")) ")" )))))) ; registrationlet "X", "Y" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Const "X")) "," (Set (Const "Y")); let "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster (Set "f" ($#k9_nat_1 :::"^\"::: ) "n") -> ($#v1_mesfunc8 :::"with_the_same_dom"::: ) for ($#m1_subset_1 :::"Functional_Sequence":::) "of" "X" "," "Y"; end; theorem :: MESFUNC8:8 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" ($#k3_mesfunc8 :::"inferior_realsequence"::: ) (Set (Var "f")) ")" ) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n"))) ($#r2_relset_1 :::"="::: ) (Set ($#k1_mesfunc8 :::"inf"::: ) (Set "(" (Set (Var "f")) ($#k10_nat_1 :::"^\"::: ) (Set (Var "n")) ")" )))))) ; theorem :: MESFUNC8:9 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" ($#k4_mesfunc8 :::"superior_realsequence"::: ) (Set (Var "f")) ")" ) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n"))) ($#r2_relset_1 :::"="::: ) (Set ($#k2_mesfunc8 :::"sup"::: ) (Set "(" (Set (Var "f")) ($#k10_nat_1 :::"^\"::: ) (Set (Var "n")) ")" )))))) ; theorem :: MESFUNC8:10 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )))) "holds" (Bool (Set (Set "(" ($#k4_mesfunc8 :::"superior_realsequence"::: ) (Set (Var "f")) ")" ) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x"))) ($#r2_funct_2 :::"="::: ) (Set ($#k4_rinfsup2 :::"superior_realsequence"::: ) (Set "(" (Set (Var "f")) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x")) ")" )))))) ; definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Const "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ); func :::"lim_inf"::: "f" -> ($#m1_subset_1 :::"PartFunc":::) "of" "X" "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) means :: MESFUNC8:def 7 (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" "f" ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "X" "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) it))) "holds" (Bool (Set it ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k6_rinfsup2 :::"lim_inf"::: ) (Set "(" "f" ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x")) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"lim_inf"::: MESFUNC8:def 7 : (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k5_mesfunc8 :::"lim_inf"::: ) (Set (Var "f")))) "iff" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "b3"))))) "holds" (Bool (Set (Set (Var "b3")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k6_rinfsup2 :::"lim_inf"::: ) (Set "(" (Set (Var "f")) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x")) ")" ))) ")" ) ")" ) ")" )))); definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Const "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ); func :::"lim_sup"::: "f" -> ($#m1_subset_1 :::"PartFunc":::) "of" "X" "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) means :: MESFUNC8:def 8 (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" "f" ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "X" "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) it))) "holds" (Bool (Set it ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k5_rinfsup2 :::"lim_sup"::: ) (Set "(" "f" ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x")) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"lim_sup"::: MESFUNC8:def 8 : (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k6_mesfunc8 :::"lim_sup"::: ) (Set (Var "f")))) "iff" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "b3"))))) "holds" (Bool (Set (Set (Var "b3")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k5_rinfsup2 :::"lim_sup"::: ) (Set "(" (Set (Var "f")) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x")) ")" ))) ")" ) ")" ) ")" )))); theorem :: MESFUNC8:11 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "holds" (Bool "(" (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k5_mesfunc8 :::"lim_inf"::: ) (Set (Var "f")) ")" )))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k5_mesfunc8 :::"lim_inf"::: ) (Set (Var "f")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_rinfsup2 :::"sup"::: ) (Set "(" ($#k3_rinfsup2 :::"inferior_realsequence"::: ) (Set "(" (Set (Var "f")) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x")) ")" ) ")" ))) & (Bool (Set (Set "(" ($#k5_mesfunc8 :::"lim_inf"::: ) (Set (Var "f")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_rinfsup2 :::"sup"::: ) (Set "(" (Set "(" ($#k3_mesfunc8 :::"inferior_realsequence"::: ) (Set (Var "f")) ")" ) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x")) ")" ))) & (Bool (Set (Set "(" ($#k5_mesfunc8 :::"lim_inf"::: ) (Set (Var "f")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_mesfunc8 :::"sup"::: ) (Set "(" ($#k3_mesfunc8 :::"inferior_realsequence"::: ) (Set (Var "f")) ")" ) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "x")))) ")" ) ")" ) & (Bool (Set ($#k5_mesfunc8 :::"lim_inf"::: ) (Set (Var "f"))) ($#r2_relset_1 :::"="::: ) (Set ($#k2_mesfunc8 :::"sup"::: ) (Set "(" ($#k3_mesfunc8 :::"inferior_realsequence"::: ) (Set (Var "f")) ")" ))) ")" ))) ; theorem :: MESFUNC8:12 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "holds" (Bool "(" (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k6_mesfunc8 :::"lim_sup"::: ) (Set (Var "f")) ")" )))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k6_mesfunc8 :::"lim_sup"::: ) (Set (Var "f")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k2_rinfsup2 :::"inf"::: ) (Set "(" ($#k4_rinfsup2 :::"superior_realsequence"::: ) (Set "(" (Set (Var "f")) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x")) ")" ) ")" ))) & (Bool (Set (Set "(" ($#k6_mesfunc8 :::"lim_sup"::: ) (Set (Var "f")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k2_rinfsup2 :::"inf"::: ) (Set "(" (Set "(" ($#k4_mesfunc8 :::"superior_realsequence"::: ) (Set (Var "f")) ")" ) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x")) ")" ))) & (Bool (Set (Set "(" ($#k6_mesfunc8 :::"lim_sup"::: ) (Set (Var "f")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_mesfunc8 :::"inf"::: ) (Set "(" ($#k4_mesfunc8 :::"superior_realsequence"::: ) (Set (Var "f")) ")" ) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "x")))) ")" ) ")" ) & (Bool (Set ($#k6_mesfunc8 :::"lim_sup"::: ) (Set (Var "f"))) ($#r2_relset_1 :::"="::: ) (Set ($#k1_mesfunc8 :::"inf"::: ) (Set "(" ($#k4_mesfunc8 :::"superior_realsequence"::: ) (Set (Var "f")) ")" ))) ")" ))) ; theorem :: MESFUNC8:13 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x"))) "is" ($#v10_mesfunc5 :::"convergent"::: ) ) "iff" (Bool (Set (Set "(" ($#k6_mesfunc8 :::"lim_sup"::: ) (Set (Var "f")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_mesfunc8 :::"lim_inf"::: ) (Set (Var "f")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "x")))) ")" )))) ; definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Const "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ); func :::"lim"::: "f" -> ($#m1_subset_1 :::"PartFunc":::) "of" "X" "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) means :: MESFUNC8:def 9 (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" "f" ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "X" "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) it))) "holds" (Bool (Set it ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k2_mesfunc5 :::"lim"::: ) (Set "(" "f" ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x")) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"lim"::: MESFUNC8:def 9 : (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k7_mesfunc8 :::"lim"::: ) (Set (Var "f")))) "iff" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "b3"))))) "holds" (Bool (Set (Set (Var "b3")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k2_mesfunc5 :::"lim"::: ) (Set "(" (Set (Var "f")) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x")) ")" ))) ")" ) ")" ) ")" )))); theorem :: MESFUNC8:14 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k7_mesfunc8 :::"lim"::: ) (Set (Var "f")) ")" ))) & (Bool (Set (Set (Var "f")) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x"))) "is" ($#v10_mesfunc5 :::"convergent"::: ) )) "holds" (Bool "(" (Bool (Set (Set "(" ($#k7_mesfunc8 :::"lim"::: ) (Set (Var "f")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_mesfunc8 :::"lim_sup"::: ) (Set (Var "f")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "x")))) & (Bool (Set (Set "(" ($#k7_mesfunc8 :::"lim"::: ) (Set (Var "f")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_mesfunc8 :::"lim_inf"::: ) (Set (Var "f")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "x")))) ")" )))) ; theorem :: MESFUNC8:15 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "f")) "being" ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k17_mesfunc1 :::"great_dom"::: ) "(" (Set "(" (Set (Var "f")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) "," (Set "(" ($#k1_measure6 :::"R_EAL"::: ) (Set (Var "r")) ")" ) ")" ")" ))) ")" )) "holds" (Bool (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k17_mesfunc1 :::"great_dom"::: ) "(" (Set "(" ($#k2_mesfunc8 :::"sup"::: ) (Set (Var "f")) ")" ) "," (Set "(" ($#k1_measure6 :::"R_EAL"::: ) (Set (Var "r")) ")" ) ")" ")" )))))))) ; theorem :: MESFUNC8:16 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "f")) "being" ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k18_mesfunc1 :::"great_eq_dom"::: ) "(" (Set "(" (Set (Var "f")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) "," (Set "(" ($#k1_measure6 :::"R_EAL"::: ) (Set (Var "r")) ")" ) ")" ")" ))) ")" )) "holds" (Bool (Set ($#k1_setfam_1 :::"meet"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k18_mesfunc1 :::"great_eq_dom"::: ) "(" (Set "(" ($#k1_mesfunc8 :::"inf"::: ) (Set (Var "f")) ")" ) "," (Set "(" ($#k1_measure6 :::"R_EAL"::: ) (Set (Var "r")) ")" ) ")" ")" )))))))) ; theorem :: MESFUNC8:17 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "f")) "being" ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k17_mesfunc1 :::"great_dom"::: ) "(" (Set "(" (Set (Var "f")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) "," (Set "(" ($#k1_measure6 :::"R_EAL"::: ) (Set (Var "r")) ")" ) ")" ")" ))) ")" )) "holds" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" ($#k6_setlim_1 :::"superior_setsequence"::: ) (Set (Var "F")) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k17_mesfunc1 :::"great_dom"::: ) "(" (Set "(" (Set "(" ($#k4_mesfunc8 :::"superior_realsequence"::: ) (Set (Var "f")) ")" ) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) "," (Set "(" ($#k1_measure6 :::"R_EAL"::: ) (Set (Var "r")) ")" ) ")" ")" ))))))))) ; theorem :: MESFUNC8:18 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "f")) "being" ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k18_mesfunc1 :::"great_eq_dom"::: ) "(" (Set "(" (Set (Var "f")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) "," (Set "(" ($#k1_measure6 :::"R_EAL"::: ) (Set (Var "r")) ")" ) ")" ")" ))) ")" )) "holds" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" ($#k5_setlim_1 :::"inferior_setsequence"::: ) (Set (Var "F")) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k18_mesfunc1 :::"great_eq_dom"::: ) "(" (Set "(" (Set "(" ($#k3_mesfunc8 :::"inferior_realsequence"::: ) (Set (Var "f")) ")" ) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) "," (Set "(" ($#k1_measure6 :::"R_EAL"::: ) (Set (Var "r")) ")" ) ")" ")" ))))))))) ; theorem :: MESFUNC8:19 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "f")) "being" ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "E")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "E"))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "f")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n"))) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "E"))) ")" )) "holds" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" ($#k4_mesfunc8 :::"superior_realsequence"::: ) (Set (Var "f")) ")" ) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n"))) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "E")))))))) ; theorem :: MESFUNC8:20 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "f")) "being" ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "E")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "E"))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "f")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n"))) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "E"))) ")" )) "holds" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" ($#k3_mesfunc8 :::"inferior_realsequence"::: ) (Set (Var "f")) ")" ) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n"))) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "E")))))))) ; theorem :: MESFUNC8:21 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k18_mesfunc1 :::"great_eq_dom"::: ) "(" (Set "(" (Set "(" ($#k4_mesfunc8 :::"superior_realsequence"::: ) (Set (Var "f")) ")" ) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) "," (Set "(" ($#k1_measure6 :::"R_EAL"::: ) (Set (Var "r")) ")" ) ")" ")" ))) ")" )) "holds" (Bool (Set ($#k2_kurato_0 :::"meet"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k18_mesfunc1 :::"great_eq_dom"::: ) "(" (Set "(" ($#k6_mesfunc8 :::"lim_sup"::: ) (Set (Var "f")) ")" ) "," (Set "(" ($#k1_measure6 :::"R_EAL"::: ) (Set (Var "r")) ")" ) ")" ")" )))))))) ; theorem :: MESFUNC8:22 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "F")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k17_mesfunc1 :::"great_dom"::: ) "(" (Set "(" (Set "(" ($#k3_mesfunc8 :::"inferior_realsequence"::: ) (Set (Var "f")) ")" ) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) "," (Set "(" ($#k1_measure6 :::"R_EAL"::: ) (Set (Var "r")) ")" ) ")" ")" ))) ")" )) "holds" (Bool (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k17_mesfunc1 :::"great_dom"::: ) "(" (Set "(" ($#k5_mesfunc8 :::"lim_inf"::: ) (Set (Var "f")) ")" ) "," (Set "(" ($#k1_measure6 :::"R_EAL"::: ) (Set (Var "r")) ")" ) ")" ")" )))))))) ; theorem :: MESFUNC8:23 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "f")) "being" ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "E")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "E"))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "f")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n"))) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "E"))) ")" )) "holds" (Bool (Set ($#k6_mesfunc8 :::"lim_sup"::: ) (Set (Var "f"))) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "E"))))))) ; theorem :: MESFUNC8:24 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "f")) "being" ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "E")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "E"))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "f")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n"))) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "E"))) ")" )) "holds" (Bool (Set ($#k5_mesfunc8 :::"lim_inf"::: ) (Set (Var "f"))) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "E"))))))) ; theorem :: MESFUNC8:25 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "f")) "being" ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "E")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "E"))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "f")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n"))) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "E"))) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "E")))) "holds" (Bool (Set (Set (Var "f")) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x"))) "is" ($#v10_mesfunc5 :::"convergent"::: ) ) ")" )) "holds" (Bool (Set ($#k7_mesfunc8 :::"lim"::: ) (Set (Var "f"))) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "E"))))))) ; theorem :: MESFUNC8:26 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "f")) "being" ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "E")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "E"))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "f")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n"))) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "E"))) ")" ) & (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Var "E"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "E")))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x"))) "is" ($#v10_mesfunc5 :::"convergent"::: ) ) & (Bool (Set (Set (Var "g")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k2_mesfunc5 :::"lim"::: ) (Set "(" (Set (Var "f")) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x")) ")" ))) ")" ) ")" )) "holds" (Bool (Set (Var "g")) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "E")))))))) ; theorem :: MESFUNC8:27 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "g"))))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x"))) "is" ($#v7_mesfunc5 :::"convergent_to_finite_number"::: ) ) & (Bool (Set (Set (Var "g")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k2_mesfunc5 :::"lim"::: ) (Set "(" (Set (Var "f")) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x")) ")" ))) ")" ) ")" )) "holds" (Bool (Set (Var "g")) "is" ($#v3_valued_0 :::"real-valued"::: ) )))) ; begin theorem :: MESFUNC8: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 "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "f")) "being" ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "E")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set (Var "E"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_xxreal_0 :::"+infty"::: ) )) & (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "E"))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n"))) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "E"))) & (Bool (Set (Set (Var "f")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n"))) "is" ($#v3_valued_0 :::"real-valued"::: ) ) ")" ) ")" ) & (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Var "E"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "E")))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x"))) "is" ($#v7_mesfunc5 :::"convergent_to_finite_number"::: ) ) & (Bool (Set (Set (Var "g")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k2_mesfunc5 :::"lim"::: ) (Set "(" (Set (Var "f")) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x")) ")" ))) ")" ) ")" )) "holds" (Bool "for" (Set (Var "r")) "," (Set (Var "e")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "e")))) "holds" (Bool "ex" (Set (Var "H")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S"))(Bool "ex" (Set (Var "N")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "(" (Bool (Set (Var "H")) ($#r1_tarski :::"c="::: ) (Set (Var "E"))) & (Bool (Set (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set (Var "H"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "N")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "k")))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "E")) ($#k7_prob_1 :::"\"::: ) (Set (Var "H"))))) "holds" (Bool (Set ($#k3_extreal1 :::"|."::: ) (Set "(" (Set "(" (Set "(" (Set (Var "f")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "k")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k4_supinf_2 :::"-"::: ) (Set "(" (Set (Var "g")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x")) ")" ) ")" ) ($#k3_extreal1 :::".|"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "e")))) ")" ) ")" )))))))))) ; theorem :: MESFUNC8:29 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "G")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "E")) ($#k6_subset_1 :::"\"::: ) (Set "(" (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ))) ")" )) "holds" (Bool (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "E")) ($#k6_subset_1 :::"\"::: ) (Set "(" ($#k1_setfam_1 :::"meet"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "F")) ")" ) ")" )))))) ; theorem :: MESFUNC8: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 "M")) "being" ($#m1_subset_1 :::"sigma_Measure":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "f")) "being" ($#v1_mesfunc8 :::"with_the_same_dom"::: ) ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "E")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k4_mesfunc5 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "E"))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "f")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n"))) ($#r1_mesfunc1 :::"is_measurable_on"::: ) (Set (Var "E"))) ")" ) & (Bool (Set (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set (Var "E"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_xxreal_0 :::"+infty"::: ) )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "ex" (Set (Var "L")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool "(" (Bool (Set (Var "L")) ($#r1_tarski :::"c="::: ) (Set (Var "E"))) & (Bool (Set (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set "(" (Set (Var "E")) ($#k7_prob_1 :::"\"::: ) (Set (Var "L")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "L")))) "holds" (Bool (Set ($#k3_extreal1 :::"|."::: ) (Set "(" (Set "(" (Set (Var "f")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k3_extreal1 :::".|"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_xxreal_0 :::"+infty"::: ) )) ")" ) ")" )) ")" ) & (Bool "ex" (Set (Var "G")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool "(" (Bool (Set (Var "G")) ($#r1_tarski :::"c="::: ) (Set (Var "E"))) & (Bool (Set (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set "(" (Set (Var "E")) ($#k7_prob_1 :::"\"::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "E")))) "holds" (Bool (Set (Set (Var "f")) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x"))) "is" ($#v7_mesfunc5 :::"convergent_to_finite_number"::: ) ) ")" ) & (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Var "E"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "G")))) "holds" (Bool (Set (Set (Var "g")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k2_mesfunc5 :::"lim"::: ) (Set "(" (Set (Var "f")) ($#k3_mesfunc5 :::"#"::: ) (Set (Var "x")) ")" ))) ")" ) ")" ))) "holds" (Bool "for" (Set (Var "e")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "e")))) "holds" (Bool "ex" (Set (Var "F")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool "(" (Bool (Set (Var "F")) ($#r1_tarski :::"c="::: ) (Set (Var "E"))) & (Bool (Set (Set (Var "M")) ($#k12_supinf_2 :::"."::: ) (Set "(" (Set (Var "E")) ($#k7_prob_1 :::"\"::: ) (Set (Var "F")) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "e"))) & (Bool "(" "for" (Set (Var "p")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "p")))) "holds" (Bool "ex" (Set (Var "N")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "N")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n")))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) "holds" (Bool (Set ($#k3_extreal1 :::"|."::: ) (Set "(" (Set "(" (Set "(" (Set (Var "f")) ($#k4_mesfunc5 :::"."::: ) (Set (Var "n")) ")" ) ($#k12_supinf_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k4_supinf_2 :::"-"::: ) (Set "(" (Set (Var "g")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x")) ")" ) ")" ) ($#k3_extreal1 :::".|"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "p")))))) ")" ) ")" ))))))))) ;