for Omega being non empty set
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