theorem :: RANDOM_1:25

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 holds
(abs f) to_power r is Real-Valued-Random-Variable of Sigma