:: RANDOM_2 semantic presentation begin theorem :: RANDOM_2:1 (Bool "for" (Set (Var "f")) "being" ($#v2_funct_1 :::"one-to-one"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" ) "st" (Bool (Bool (Set (Var "A")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "B")))) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set (Var "f")) ($#k5_relat_1 :::"|"::: ) (Set (Var "A")) ")" )) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set (Var "f")) ($#k5_relat_1 :::"|"::: ) (Set (Var "B")) ")" ))))) ; theorem :: RANDOM_2:2 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set (Var "f")) ($#k3_relat_1 :::"*"::: ) (Set (Var "g")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set (Var "f")) ($#k5_relat_1 :::"|"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "g")) ")" ) ")" )))) ; registrationlet "Omega" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "Sigma" be ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "Omega")); cluster ($#v1_relat_1 :::"Relation-like"::: ) "Omega" ($#v4_relat_1 :::"-defined"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_partfun1 :::"total"::: ) ($#v1_funct_2 :::"quasi_total"::: ) bbbadV1_VALUED_0() bbbadV2_VALUED_0() bbbadV3_VALUED_0() ($#v6_supinf_2 :::"nonnegative"::: ) for ($#m1_random_1 :::"Real-Valued-Random-Variable"::: ) "of" "Sigma"; end; registrationlet "Omega" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "Sigma" be ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "Omega")); let "X" be ($#m1_random_1 :::"Real-Valued-Random-Variable"::: ) "of" (Set (Const "Sigma")); cluster (Set ($#k54_valued_1 :::"|."::: ) "X" ($#k54_valued_1 :::".|"::: ) ) -> ($#v6_supinf_2 :::"nonnegative"::: ) ; end; theorem :: RANDOM_2:3 (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "Omega")) ($#k8_funcop_1 :::"-->"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k3_mesfunc2 :::"chi"::: ) "(" (Set (Var "Omega")) "," (Set (Var "Omega")) ")" ))) ; theorem :: RANDOM_2:4 (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "Sigma")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega")) "holds" (Bool (Set (Set (Var "Omega")) ($#k8_funcop_1 :::"-->"::: ) (Set (Var "r"))) "is" ($#m1_random_1 :::"Real-Valued-Random-Variable"::: ) "of" (Set (Var "Sigma")))))) ; theorem :: RANDOM_2: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 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k2_mesfun6c :::"to_power"::: ) (Num 2)) ($#r2_relset_1 :::"="::: ) (Set (Set "(" ($#k32_valued_1 :::"-"::: ) (Set (Var "f")) ")" ) ($#k2_mesfun6c :::"to_power"::: ) (Num 2))) & (Bool (Set (Set (Var "f")) ($#k2_mesfun6c :::"to_power"::: ) (Num 2)) ($#r2_relset_1 :::"="::: ) (Set (Set "(" ($#k56_valued_1 :::"abs"::: ) (Set (Var "f")) ")" ) ($#k2_mesfun6c :::"to_power"::: ) (Num 2))) ")" ))) ; theorem :: RANDOM_2:6 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "f")) ($#k3_valued_1 :::"+"::: ) (Set (Var "g")) ")" ) ($#k2_mesfun6c :::"to_power"::: ) (Num 2)) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "f")) ($#k2_mesfun6c :::"to_power"::: ) (Num 2) ")" ) ($#k3_valued_1 :::"+"::: ) (Set "(" (Num 2) ($#k26_valued_1 :::"(#)"::: ) (Set "(" (Set (Var "f")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "g")) ")" ) ")" ) ")" ) ($#k3_valued_1 :::"+"::: ) (Set "(" (Set (Var "g")) ($#k2_mesfun6c :::"to_power"::: ) (Num 2) ")" ))) & (Bool (Set (Set "(" (Set (Var "f")) ($#k47_valued_1 :::"-"::: ) (Set (Var "g")) ")" ) ($#k2_mesfun6c :::"to_power"::: ) (Num 2)) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "f")) ($#k2_mesfun6c :::"to_power"::: ) (Num 2) ")" ) ($#k47_valued_1 :::"-"::: ) (Set "(" (Num 2) ($#k26_valued_1 :::"(#)"::: ) (Set "(" (Set (Var "f")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "g")) ")" ) ")" ) ")" ) ($#k3_valued_1 :::"+"::: ) (Set "(" (Set (Var "g")) ($#k2_mesfun6c :::"to_power"::: ) (Num 2) ")" ))) ")" ))) ; definitionlet "Omega" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "Sigma" be ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "Omega")); let "P" be ($#m2_prob_1 :::"Probability"::: ) "of" (Set (Const "Sigma")); let "X" be ($#m1_random_1 :::"Real-Valued-Random-Variable"::: ) "of" (Set (Const "Sigma")); assume (Bool "(" (Bool (Set (Const "X")) ($#r1_random_1 :::"is_integrable_on"::: ) (Set (Const "P"))) & (Bool (Set (Set "(" ($#k7_random_1 :::"abs"::: ) (Set (Const "X")) ")" ) ($#k2_mesfun6c :::"to_power"::: ) (Num 2)) ($#r3_mesfunc6 :::"is_integrable_on"::: ) (Set ($#k2_prob_4 :::"P2M"::: ) (Set (Const "P")))) ")" ) ; func :::"variance"::: "(" "X" "," "P" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) means :: RANDOM_2:def 1 (Bool "ex" (Set (Var "Y")) "," (Set (Var "E")) "being" ($#m1_random_1 :::"Real-Valued-Random-Variable"::: ) "of" "Sigma" "st" (Bool "(" (Bool (Set (Var "E")) ($#r2_funct_2 :::"="::: ) (Set "Omega" ($#k8_funcop_1 :::"-->"::: ) (Set "(" ($#k8_random_1 :::"expect"::: ) "(" "X" "," "P" ")" ")" ))) & (Bool (Set (Var "Y")) ($#r2_funct_2 :::"="::: ) (Set "X" ($#k4_random_1 :::"-"::: ) (Set (Var "E")))) & (Bool (Set (Var "Y")) ($#r1_random_1 :::"is_integrable_on"::: ) "P") & (Bool (Set (Set "(" ($#k7_random_1 :::"abs"::: ) (Set (Var "Y")) ")" ) ($#k2_mesfun6c :::"to_power"::: ) (Num 2)) ($#r3_mesfunc6 :::"is_integrable_on"::: ) (Set ($#k2_prob_4 :::"P2M"::: ) "P")) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k1_mesfunc6 :::"Integral"::: ) "(" (Set "(" ($#k2_prob_4 :::"P2M"::: ) "P" ")" ) "," (Set "(" (Set "(" ($#k7_random_1 :::"abs"::: ) (Set (Var "Y")) ")" ) ($#k2_mesfun6c :::"to_power"::: ) (Num 2) ")" ) ")" )) ")" )); end; :: deftheorem defines :::"variance"::: RANDOM_2:def 1 : (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Sigma")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega")) (Bool "for" (Set (Var "P")) "being" ($#m2_prob_1 :::"Probability"::: ) "of" (Set (Var "Sigma")) (Bool "for" (Set (Var "X")) "being" ($#m1_random_1 :::"Real-Valued-Random-Variable"::: ) "of" (Set (Var "Sigma")) "st" (Bool (Bool (Set (Var "X")) ($#r1_random_1 :::"is_integrable_on"::: ) (Set (Var "P"))) & (Bool (Set (Set "(" ($#k7_random_1 :::"abs"::: ) (Set (Var "X")) ")" ) ($#k2_mesfun6c :::"to_power"::: ) (Num 2)) ($#r3_mesfunc6 :::"is_integrable_on"::: ) (Set ($#k2_prob_4 :::"P2M"::: ) (Set (Var "P"))))) "holds" (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k1_random_2 :::"variance"::: ) "(" (Set (Var "X")) "," (Set (Var "P")) ")" )) "iff" (Bool "ex" (Set (Var "Y")) "," (Set (Var "E")) "being" ($#m1_random_1 :::"Real-Valued-Random-Variable"::: ) "of" (Set (Var "Sigma")) "st" (Bool "(" (Bool (Set (Var "E")) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "Omega")) ($#k8_funcop_1 :::"-->"::: ) (Set "(" ($#k8_random_1 :::"expect"::: ) "(" (Set (Var "X")) "," (Set (Var "P")) ")" ")" ))) & (Bool (Set (Var "Y")) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "X")) ($#k4_random_1 :::"-"::: ) (Set (Var "E")))) & (Bool (Set (Var "Y")) ($#r1_random_1 :::"is_integrable_on"::: ) (Set (Var "P"))) & (Bool (Set (Set "(" ($#k7_random_1 :::"abs"::: ) (Set (Var "Y")) ")" ) ($#k2_mesfun6c :::"to_power"::: ) (Num 2)) ($#r3_mesfunc6 :::"is_integrable_on"::: ) (Set ($#k2_prob_4 :::"P2M"::: ) (Set (Var "P")))) & (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k1_mesfunc6 :::"Integral"::: ) "(" (Set "(" ($#k2_prob_4 :::"P2M"::: ) (Set (Var "P")) ")" ) "," (Set "(" (Set "(" ($#k7_random_1 :::"abs"::: ) (Set (Var "Y")) ")" ) ($#k2_mesfun6c :::"to_power"::: ) (Num 2) ")" ) ")" )) ")" )) ")" )))))); begin theorem :: RANDOM_2:7 (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Sigma")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega")) (Bool "for" (Set (Var "P")) "being" ($#m2_prob_1 :::"Probability"::: ) "of" (Set (Var "Sigma")) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "X")) "being" ($#m1_random_1 :::"Real-Valued-Random-Variable"::: ) "of" (Set (Var "Sigma")) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set (Var "X")) "is" ($#v6_supinf_2 :::"nonnegative"::: ) ) & (Bool (Set (Var "X")) ($#r1_random_1 :::"is_integrable_on"::: ) (Set (Var "P"))) & (Bool (Set (Set "(" ($#k7_random_1 :::"abs"::: ) (Set (Var "X")) ")" ) ($#k2_mesfun6c :::"to_power"::: ) (Num 2)) ($#r3_mesfunc6 :::"is_integrable_on"::: ) (Set ($#k2_prob_4 :::"P2M"::: ) (Set (Var "P"))))) "holds" (Bool (Set (Set (Var "P")) ($#k1_seq_1 :::"."::: ) "{" (Set (Var "t")) where t "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Omega")) : (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k17_complex1 :::"|."::: ) (Set "(" (Set "(" (Set (Var "X")) ($#k1_seq_1 :::"."::: ) (Set (Var "t")) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" ($#k8_random_1 :::"expect"::: ) "(" (Set (Var "X")) "," (Set (Var "P")) ")" ")" ) ")" ) ($#k17_complex1 :::".|"::: ) )) "}" ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k1_random_2 :::"variance"::: ) "(" (Set (Var "X")) "," (Set (Var "P")) ")" ")" ) ($#k12_binop_2 :::"/"::: ) (Set "(" (Set (Var "r")) ($#k4_power :::"to_power"::: ) (Num 2) ")" )))))))) ; begin theorem :: RANDOM_2:8 (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Omega")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k1_zfmisc_1 :::"bool"::: ) (Set (Var "Omega")) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r1_tarski :::"c="::: ) (Set (Var "Omega")))) "holds" (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "P")) ($#k1_seq_1 :::"."::: ) (Set (Var "x")))) & (Bool (Set (Set (Var "P")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<="::: ) (Num 1)) ")" ) ")" ) & (Bool (Set (Set (Var "P")) ($#k1_seq_1 :::"."::: ) (Set (Var "Omega"))) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool "(" "for" (Set (Var "z")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Omega")) "holds" (Bool (Set (Set (Var "P")) ($#k1_seq_1 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k5_bhsp_5 :::"setopfunc"::: ) "(" (Set (Var "z")) "," (Set (Var "Omega")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set (Var "f")) "," (Set ($#k33_binop_2 :::"addreal"::: ) ) ")" )) ")" )) "holds" (Bool (Set (Var "P")) "is" ($#m2_prob_1 :::"Probability"::: ) "of" (Set ($#k1_random_1 :::"Trivial-SigmaField"::: ) (Set (Var "Omega"))))))) ; theorem :: RANDOM_2:9 (Bool "for" (Set (Var "DX")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "DX")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "Y")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "DX")) (Bool "ex" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "DX")) "st" (Bool "(" (Bool (Set (Var "p")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Var "Y"))) & (Bool (Set ($#k5_bhsp_5 :::"setopfunc"::: ) "(" (Set (Var "Y")) "," (Set (Var "DX")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set (Var "F")) "," (Set ($#k33_binop_2 :::"addreal"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" ($#k4_bhsp_5 :::"Func_Seq"::: ) "(" (Set (Var "F")) "," (Set (Var "p")) ")" ")" ))) ")" ))))) ; theorem :: RANDOM_2:10 (Bool "for" (Set (Var "DX")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "DX")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "Y")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "DX")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "DX")) "st" (Bool (Bool (Set (Var "p")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Var "Y")))) "holds" (Bool (Set ($#k5_bhsp_5 :::"setopfunc"::: ) "(" (Set (Var "Y")) "," (Set (Var "DX")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set (Var "F")) "," (Set ($#k33_binop_2 :::"addreal"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" ($#k4_bhsp_5 :::"Func_Seq"::: ) "(" (Set (Var "F")) "," (Set (Var "p")) ")" ")" ))))))) ; theorem :: RANDOM_2:11 (Bool "for" (Set (Var "DX1")) "," (Set (Var "DX2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "DX1")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "F2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "DX2")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "DX1")) "," (Set (Var "DX2")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "Y1")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "DX1")) (Bool "for" (Set (Var "p1")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "DX1")) "st" (Bool (Bool (Set (Var "p1")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "p1"))) ($#r1_hidden :::"="::: ) (Set (Var "Y1")))) "holds" (Bool "for" (Set (Var "p2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "DX2")) (Bool "for" (Set (Var "p3")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "DX1")) "," (Set (Var "DX2")) ($#k2_zfmisc_1 :::":]"::: ) ) (Bool "for" (Set (Var "Y2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "DX2")) (Bool "for" (Set (Var "Y3")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "DX1")) "," (Set (Var "DX2")) ($#k2_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "p2")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "p2"))) ($#r1_hidden :::"="::: ) (Set (Var "Y2"))) & (Bool (Set (Var "p3")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "p3"))) ($#r2_relset_1 :::"="::: ) (Set (Var "Y3"))) & (Bool (Set (Var "Y3")) ($#r1_hidden :::"="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Y1")) "," (Set (Var "Y2")) ($#k2_zfmisc_1 :::":]"::: ) )) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Y1"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "Y2")))) "holds" (Bool (Set (Set (Var "G")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F1")) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "F2")) ($#k1_seq_1 :::"."::: ) (Set (Var "y")) ")" ))) ")" )) "holds" (Bool (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" ($#k4_bhsp_5 :::"Func_Seq"::: ) "(" (Set (Var "G")) "," (Set (Var "p3")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" ($#k4_bhsp_5 :::"Func_Seq"::: ) "(" (Set (Var "F1")) "," (Set (Var "p1")) ")" ")" ) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" ($#k4_bhsp_5 :::"Func_Seq"::: ) "(" (Set (Var "F2")) "," (Set (Var "p2")) ")" ")" ) ")" ))))))))))))) ; theorem :: RANDOM_2:12 (Bool "for" (Set (Var "DX1")) "," (Set (Var "DX2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "DX1")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "F2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "DX2")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "DX1")) "," (Set (Var "DX2")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "Y1")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "DX1")) (Bool "for" (Set (Var "Y2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "DX2")) (Bool "for" (Set (Var "Y3")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "DX1")) "," (Set (Var "DX2")) ($#k2_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "Y3")) ($#r1_hidden :::"="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Y1")) "," (Set (Var "Y2")) ($#k2_zfmisc_1 :::":]"::: ) )) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Y1"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "Y2")))) "holds" (Bool (Set (Set (Var "G")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F1")) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "F2")) ($#k1_seq_1 :::"."::: ) (Set (Var "y")) ")" ))) ")" )) "holds" (Bool (Set ($#k5_bhsp_5 :::"setopfunc"::: ) "(" (Set (Var "Y3")) "," (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "DX1")) "," (Set (Var "DX2")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set (Var "G")) "," (Set ($#k33_binop_2 :::"addreal"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_bhsp_5 :::"setopfunc"::: ) "(" (Set (Var "Y1")) "," (Set (Var "DX1")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set (Var "F1")) "," (Set ($#k33_binop_2 :::"addreal"::: ) ) ")" ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k5_bhsp_5 :::"setopfunc"::: ) "(" (Set (Var "Y2")) "," (Set (Var "DX2")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set (Var "F2")) "," (Set ($#k33_binop_2 :::"addreal"::: ) ) ")" ")" )))))))))) ; theorem :: RANDOM_2:13 (Bool "for" (Set (Var "DX")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "DX")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "Y")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "DX")) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Y")))) "holds" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "F")) ($#k1_seq_1 :::"."::: ) (Set (Var "x")))) ")" )) "holds" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k5_bhsp_5 :::"setopfunc"::: ) "(" (Set (Var "Y")) "," (Set (Var "DX")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set (Var "F")) "," (Set ($#k33_binop_2 :::"addreal"::: ) ) ")" ))))) ; theorem :: RANDOM_2:14 (Bool "for" (Set (Var "DX")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "DX")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "Y1")) "," (Set (Var "Y2")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "DX")) "st" (Bool (Bool (Set (Var "Y1")) ($#r1_tarski :::"c="::: ) (Set (Var "Y2"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Y2")))) "holds" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "F")) ($#k1_seq_1 :::"."::: ) (Set (Var "x")))) ")" )) "holds" (Bool (Set ($#k5_bhsp_5 :::"setopfunc"::: ) "(" (Set (Var "Y1")) "," (Set (Var "DX")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set (Var "F")) "," (Set ($#k33_binop_2 :::"addreal"::: ) ) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k5_bhsp_5 :::"setopfunc"::: ) "(" (Set (Var "Y2")) "," (Set (Var "DX")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set (Var "F")) "," (Set ($#k33_binop_2 :::"addreal"::: ) ) ")" ))))) ; theorem :: RANDOM_2:15 (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "P")) "being" ($#m2_prob_1 :::"Probability"::: ) "of" (Set ($#k1_random_1 :::"Trivial-SigmaField"::: ) (Set (Var "Omega"))) (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Omega")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Omega")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "ex" (Set (Var "G")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) )(Bool "ex" (Set (Var "s")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "Y")) "st" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "Y")))) & (Bool (Set (Var "s")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Var "Y"))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "Y")))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "G"))))) "holds" (Bool (Set (Set (Var "G")) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k1_seq_1 :::"."::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k1_tarski :::"}"::: ) ) ")" ))) ")" ) & (Bool (Set ($#k1_mesfunc6 :::"Integral"::: ) "(" (Set "(" ($#k2_prob_4 :::"P2M"::: ) (Set (Var "P")) ")" ) "," (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "Y")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set (Var "G")))) ")" ))))))) ; definitionlet "Omega1", "Omega2" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) ; let "P1" be ($#m2_prob_1 :::"Probability"::: ) "of" (Set ($#k1_random_1 :::"Trivial-SigmaField"::: ) (Set (Const "Omega1"))); let "P2" be ($#m2_prob_1 :::"Probability"::: ) "of" (Set ($#k1_random_1 :::"Trivial-SigmaField"::: ) (Set (Const "Omega2"))); func :::"Product-Probability"::: "(" "Omega1" "," "Omega2" "," "P1" "," "P2" ")" -> ($#m2_prob_1 :::"Probability"::: ) "of" (Set ($#k1_random_1 :::"Trivial-SigmaField"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) "Omega1" "," "Omega2" ($#k2_zfmisc_1 :::":]"::: ) )) means :: RANDOM_2:def 2 (Bool "ex" (Set (Var "Q")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) "Omega1" "," "Omega2" ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "Omega1") & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) "Omega2")) "holds" (Bool (Set (Set (Var "Q")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" "P1" ($#k1_seq_1 :::"."::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" "P2" ($#k1_seq_1 :::"."::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) ) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "z")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) "Omega1" "," "Omega2" ($#k2_zfmisc_1 :::":]"::: ) ) "holds" (Bool (Set it ($#k1_seq_1 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k5_bhsp_5 :::"setopfunc"::: ) "(" (Set (Var "z")) "," (Set ($#k2_zfmisc_1 :::"[:"::: ) "Omega1" "," "Omega2" ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set (Var "Q")) "," (Set ($#k33_binop_2 :::"addreal"::: ) ) ")" )) ")" ) ")" )); end; :: deftheorem defines :::"Product-Probability"::: RANDOM_2:def 2 : (Bool "for" (Set (Var "Omega1")) "," (Set (Var "Omega2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "P1")) "being" ($#m2_prob_1 :::"Probability"::: ) "of" (Set ($#k1_random_1 :::"Trivial-SigmaField"::: ) (Set (Var "Omega1"))) (Bool "for" (Set (Var "P2")) "being" ($#m2_prob_1 :::"Probability"::: ) "of" (Set ($#k1_random_1 :::"Trivial-SigmaField"::: ) (Set (Var "Omega2"))) (Bool "for" (Set (Var "b5")) "being" ($#m2_prob_1 :::"Probability"::: ) "of" (Set ($#k1_random_1 :::"Trivial-SigmaField"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Omega1")) "," (Set (Var "Omega2")) ($#k2_zfmisc_1 :::":]"::: ) )) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k2_random_2 :::"Product-Probability"::: ) "(" (Set (Var "Omega1")) "," (Set (Var "Omega2")) "," (Set (Var "P1")) "," (Set (Var "P2")) ")" )) "iff" (Bool "ex" (Set (Var "Q")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Omega1")) "," (Set (Var "Omega2")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Omega1"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "Omega2")))) "holds" (Bool (Set (Set (Var "Q")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "P1")) ($#k1_seq_1 :::"."::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "P2")) ($#k1_seq_1 :::"."::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) ) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "z")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Omega1")) "," (Set (Var "Omega2")) ($#k2_zfmisc_1 :::":]"::: ) ) "holds" (Bool (Set (Set (Var "b5")) ($#k1_seq_1 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k5_bhsp_5 :::"setopfunc"::: ) "(" (Set (Var "z")) "," (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Omega1")) "," (Set (Var "Omega2")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set (Var "Q")) "," (Set ($#k33_binop_2 :::"addreal"::: ) ) ")" )) ")" ) ")" )) ")" ))))); theorem :: RANDOM_2:16 (Bool "for" (Set (Var "Omega1")) "," (Set (Var "Omega2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "P1")) "being" ($#m2_prob_1 :::"Probability"::: ) "of" (Set ($#k1_random_1 :::"Trivial-SigmaField"::: ) (Set (Var "Omega1"))) (Bool "for" (Set (Var "P2")) "being" ($#m2_prob_1 :::"Probability"::: ) "of" (Set ($#k1_random_1 :::"Trivial-SigmaField"::: ) (Set (Var "Omega2"))) (Bool "for" (Set (Var "Y1")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Omega1")) (Bool "for" (Set (Var "Y2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Omega2")) "holds" (Bool (Set (Set "(" ($#k2_random_2 :::"Product-Probability"::: ) "(" (Set (Var "Omega1")) "," (Set (Var "Omega2")) "," (Set (Var "P1")) "," (Set (Var "P2")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Y1")) "," (Set (Var "Y2")) ($#k2_zfmisc_1 :::":]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "P1")) ($#k1_seq_1 :::"."::: ) (Set (Var "Y1")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "P2")) ($#k1_seq_1 :::"."::: ) (Set (Var "Y2")) ")" )))))))) ; theorem :: RANDOM_2:17 (Bool "for" (Set (Var "Omega1")) "," (Set (Var "Omega2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "P1")) "being" ($#m2_prob_1 :::"Probability"::: ) "of" (Set ($#k1_random_1 :::"Trivial-SigmaField"::: ) (Set (Var "Omega1"))) (Bool "for" (Set (Var "P2")) "being" ($#m2_prob_1 :::"Probability"::: ) "of" (Set ($#k1_random_1 :::"Trivial-SigmaField"::: ) (Set (Var "Omega2"))) (Bool "for" (Set (Var "y1")) "," (Set (Var "y2")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "y1")) ($#r2_hidden :::"in"::: ) (Set (Var "Omega1"))) & (Bool (Set (Var "y2")) ($#r2_hidden :::"in"::: ) (Set (Var "Omega2")))) "holds" (Bool (Set (Set "(" ($#k2_random_2 :::"Product-Probability"::: ) "(" (Set (Var "Omega1")) "," (Set (Var "Omega2")) "," (Set (Var "P1")) "," (Set (Var "P2")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "y1")) "," (Set (Var "y2")) ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "P1")) ($#k1_seq_1 :::"."::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "y1")) ($#k1_tarski :::"}"::: ) ) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "P2")) ($#k1_seq_1 :::"."::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "y2")) ($#k1_tarski :::"}"::: ) ) ")" ))))))) ; begin definitionlet "Omega" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "Sigma" be ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "Omega")); func :::"Real-Valued-Random-Variables-Set"::: "Sigma" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k12_funcsdom :::"RAlgebra"::: ) "Omega" ")" ) equals :: RANDOM_2:def 3 "{" (Set (Var "f")) where f "is" ($#m1_random_1 :::"Real-Valued-Random-Variable"::: ) "of" "Sigma" : (Bool verum) "}" ; end; :: deftheorem defines :::"Real-Valued-Random-Variables-Set"::: RANDOM_2:def 3 : (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Sigma")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega")) "holds" (Bool (Set ($#k3_random_2 :::"Real-Valued-Random-Variables-Set"::: ) (Set (Var "Sigma"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "f")) where f "is" ($#m1_random_1 :::"Real-Valued-Random-Variable"::: ) "of" (Set (Var "Sigma")) : (Bool verum) "}" ))); registrationlet "Omega" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "Sigma" be ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "Omega")); cluster (Set ($#k3_random_2 :::"Real-Valued-Random-Variables-Set"::: ) "Sigma") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v3_c0sp1 :::"multiplicatively-closed"::: ) ($#v4_c0sp1 :::"additively-linearly-closed"::: ) ; end; definitionlet "Omega" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "Sigma" be ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "Omega")); func :::"R_Algebra_of_Real-Valued-Random-Variables"::: "Sigma" -> ($#l1_funcsdom :::"Algebra":::) equals :: RANDOM_2:def 4 (Set ($#g1_funcsdom :::"AlgebraStr"::: ) "(#" (Set "(" ($#k3_random_2 :::"Real-Valued-Random-Variables-Set"::: ) "Sigma" ")" ) "," (Set "(" ($#k2_c0sp1 :::"mult_"::: ) "(" (Set "(" ($#k3_random_2 :::"Real-Valued-Random-Variables-Set"::: ) "Sigma" ")" ) "," (Set "(" ($#k12_funcsdom :::"RAlgebra"::: ) "Omega" ")" ) ")" ")" ) "," (Set "(" ($#k1_c0sp1 :::"Add_"::: ) "(" (Set "(" ($#k3_random_2 :::"Real-Valued-Random-Variables-Set"::: ) "Sigma" ")" ) "," (Set "(" ($#k12_funcsdom :::"RAlgebra"::: ) "Omega" ")" ) ")" ")" ) "," (Set "(" ($#k5_c0sp1 :::"Mult_"::: ) "(" (Set "(" ($#k3_random_2 :::"Real-Valued-Random-Variables-Set"::: ) "Sigma" ")" ) "," (Set "(" ($#k12_funcsdom :::"RAlgebra"::: ) "Omega" ")" ) ")" ")" ) "," (Set "(" ($#k4_c0sp1 :::"One_"::: ) "(" (Set "(" ($#k3_random_2 :::"Real-Valued-Random-Variables-Set"::: ) "Sigma" ")" ) "," (Set "(" ($#k12_funcsdom :::"RAlgebra"::: ) "Omega" ")" ) ")" ")" ) "," (Set "(" ($#k3_c0sp1 :::"Zero_"::: ) "(" (Set "(" ($#k3_random_2 :::"Real-Valued-Random-Variables-Set"::: ) "Sigma" ")" ) "," (Set "(" ($#k12_funcsdom :::"RAlgebra"::: ) "Omega" ")" ) ")" ")" ) "#)" ); end; :: deftheorem defines :::"R_Algebra_of_Real-Valued-Random-Variables"::: RANDOM_2:def 4 : (Bool "for" (Set (Var "Omega")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Sigma")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "Omega")) "holds" (Bool (Set ($#k4_random_2 :::"R_Algebra_of_Real-Valued-Random-Variables"::: ) (Set (Var "Sigma"))) ($#r1_hidden :::"="::: ) (Set ($#g1_funcsdom :::"AlgebraStr"::: ) "(#" (Set "(" ($#k3_random_2 :::"Real-Valued-Random-Variables-Set"::: ) (Set (Var "Sigma")) ")" ) "," (Set "(" ($#k2_c0sp1 :::"mult_"::: ) "(" (Set "(" ($#k3_random_2 :::"Real-Valued-Random-Variables-Set"::: ) (Set (Var "Sigma")) ")" ) "," (Set "(" ($#k12_funcsdom :::"RAlgebra"::: ) (Set (Var "Omega")) ")" ) ")" ")" ) "," (Set "(" ($#k1_c0sp1 :::"Add_"::: ) "(" (Set "(" ($#k3_random_2 :::"Real-Valued-Random-Variables-Set"::: ) (Set (Var "Sigma")) ")" ) "," (Set "(" ($#k12_funcsdom :::"RAlgebra"::: ) (Set (Var "Omega")) ")" ) ")" ")" ) "," (Set "(" ($#k5_c0sp1 :::"Mult_"::: ) "(" (Set "(" ($#k3_random_2 :::"Real-Valued-Random-Variables-Set"::: ) (Set (Var "Sigma")) ")" ) "," (Set "(" ($#k12_funcsdom :::"RAlgebra"::: ) (Set (Var "Omega")) ")" ) ")" ")" ) "," (Set "(" ($#k4_c0sp1 :::"One_"::: ) "(" (Set "(" ($#k3_random_2 :::"Real-Valued-Random-Variables-Set"::: ) (Set (Var "Sigma")) ")" ) "," (Set "(" ($#k12_funcsdom :::"RAlgebra"::: ) (Set (Var "Omega")) ")" ) ")" ")" ) "," (Set "(" ($#k3_c0sp1 :::"Zero_"::: ) "(" (Set "(" ($#k3_random_2 :::"Real-Valued-Random-Variables-Set"::: ) (Set (Var "Sigma")) ")" ) "," (Set "(" ($#k12_funcsdom :::"RAlgebra"::: ) (Set (Var "Omega")) ")" ) ")" ")" ) "#)" )))); registrationlet "Omega" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "Sigma" be ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "Omega")); cluster (Set ($#k4_random_2 :::"R_Algebra_of_Real-Valued-Random-Variables"::: ) "Sigma") -> ($#v8_rlvect_1 :::"scalar-unital"::: ) ; end;