theorem
for
Prob being
Probability of
Special_SigmaField2 for
r being
Real st
r > 0 holds
for
jpi being
pricefunction for
G being
sequence of
(set_of_random_variables_on (Special_SigmaField2,Borel_Sets)) st ( for
d being
Nat holds
(
G . d = {1,2,3,4} --> ((jpi . d) * (1 + r)) &
Change_Element_to_Func (
G,
d)
is_integrable_on P2M Prob &
Change_Element_to_Func (
G,
d)
is_simple_func_in Special_SigmaField2 ) ) holds
(
Risk_neutral_measure_exists_wrt G,
jpi,
r & ( for
s being
Nat holds
jpi . s = expect (
(Real_RV (r,(Change_Element_to_Func (G,s)))),
Prob) ) )