let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for f, g being Real-Valued-Random-Variable of Sigma holds f (#) g is Real-Valued-Random-Variable of Sigma
let Sigma be SigmaField of Omega; :: thesis: for f, g being Real-Valued-Random-Variable of Sigma holds f (#) g is Real-Valued-Random-Variable of Sigma
let f, g be Real-Valued-Random-Variable of Sigma; :: thesis: f (#) g is Real-Valued-Random-Variable of Sigma
consider X being Element of Sigma such that
P1: ( X = Omega & f is_measurable_on X ) by def1;
consider Y being Element of Sigma such that
P2: ( Y = Omega & g is_measurable_on Y ) by def1;
P3: ( R_EAL f is_measurable_on X & R_EAL g is_measurable_on X ) by P1, P2, MESFUNC6:def 6;
( dom (R_EAL f) = X & dom (R_EAL g) = X ) by P1, FUNCT_2:def 1;
then (dom (R_EAL f)) /\ (dom (R_EAL g)) = X ;
then (R_EAL f) (#) (R_EAL g) is_measurable_on X by P3, MESFUNC7:15;
then R_EAL (f (#) g) is_measurable_on X by Cor1;
then f (#) g is_measurable_on X by MESFUNC6:def 6;
hence f (#) g is Real-Valued-Random-Variable of Sigma by P1, def1; :: thesis: verum