theorem ThArbPrel: :: FINANCE6:18

for Prob being Probability of Special_SigmaField2
for r being Real st r > 0 holds
for jpi being pricefunction
for d being Nat ex f being Real-Valued-Random-Variable of Special_SigmaField2 st
( f = {1,2,3,4} --> ((jpi . d) * (1 + r)) & f is_integrable_on P2M Prob & f is_simple_func_in Special_SigmaField2 )