let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for f being Real-Valued-Random-Variable of Sigma
for r being Real st 0 <= r & f is nonnegative holds
f to_power r is Real-Valued-Random-Variable of Sigma
let Sigma be SigmaField of Omega; :: thesis: for f being Real-Valued-Random-Variable of Sigma
for r being Real st 0 <= r & f is nonnegative holds
f to_power r is Real-Valued-Random-Variable of Sigma
let f be Real-Valued-Random-Variable of Sigma; :: thesis: for r being Real st 0 <= r & f is nonnegative holds
f to_power r is Real-Valued-Random-Variable of Sigma
let r be Real; :: thesis: ( 0 <= r & f is nonnegative implies f to_power r is Real-Valued-Random-Variable of Sigma )
assume A1: ( 0 <= r & f is nonnegative ) ; :: thesis: f to_power r is Real-Valued-Random-Variable of Sigma
A2: dom f = Omega by FUNCT_2:def 1;
( rng (f to_power r) c= REAL & dom (f to_power r) = dom f ) by MESFUN6C:def 4;
then A3: f to_power r is Function of Omega,REAL by A2, FUNCT_2:2;
dom f = [#] Sigma by FUNCT_2:def 1;
then f to_power r is [#] Sigma -measurable by A1, MESFUN6C:29;
hence f to_power r is Real-Valued-Random-Variable of Sigma by A3; :: thesis: verum