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
A1: X = Omega and
A2: f is_measurable_on X by Def2;
A3: R_EAL f is_measurable_on X by A2, MESFUNC6:def 1;
( dom (R_EAL f) = X & dom (R_EAL g) = X ) by A1, FUNCT_2:def 1;
then A4: (dom (R_EAL f)) /\ (dom (R_EAL g)) = X ;
ex Y being Element of Sigma st
( Y = Omega & g is_measurable_on Y ) by Def2;
then R_EAL g is_measurable_on X by A1, MESFUNC6:def 1;
then (R_EAL f) (#) (R_EAL g) is_measurable_on X by A3, A4, MESFUNC7:15;
then R_EAL (f (#) g) is_measurable_on X by Th21;
then f (#) g is_measurable_on X by MESFUNC6:def 1;
hence f (#) g is Real-Valued-Random-Variable of Sigma by A1, Def2; :: thesis: verum