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 number 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 number 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 number st 0 <= r & f is nonnegative holds
f to_power r is Real-Valued-Random-Variable of Sigma
let r be real number ; :: thesis: ( 0 <= r & f is nonnegative implies f to_power r is Real-Valued-Random-Variable of Sigma )
assume AS: ( 0 <= r & f is nonnegative ) ; :: thesis: f to_power r 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;
P4: rng (f to_power r) c= REAL ;
P3: dom (f to_power r) = dom f by MESFUN6C:def 6;
dom f = Omega by FUNCT_2:def 1;
then P2: f to_power r is Function of Omega,REAL by P3, P4, FUNCT_2:4;
dom f = X by FUNCT_2:def 1, P1;
hence f to_power r is Real-Valued-Random-Variable of Sigma by def1, P1, P2, AS, MESFUN6C:29; :: thesis: verum