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
set X = [#] Sigma;
A2: f is [#] Sigma -measurable ;
A3: R_EAL f is [#] Sigma -measurable by A2;
( dom (R_EAL f) = [#] Sigma & dom (R_EAL g) = [#] Sigma ) by FUNCT_2:def 1;
then A4: (dom (R_EAL f)) /\ (dom (R_EAL g)) = [#] Sigma ;
g is [#] Sigma -measurable ;
then R_EAL g is [#] Sigma -measurable ;
then (R_EAL f) (#) (R_EAL g) is [#] Sigma -measurable by A3, A4, MESFUNC7:15;
then R_EAL (f (#) g) is [#] Sigma -measurable by Th21;
then f (#) g is [#] Sigma -measurable ;
hence f (#) g is Real-Valued-Random-Variable of Sigma ; :: thesis: verum