let Prob be Probability of Special_SigmaField2 ; :: thesis: 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
( Change_Element_to_Func (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 (s,r,(Change_Element_to_Func (G,s)))),Prob) ) )
let r be Real; :: thesis: ( r > 0 implies for jpi being pricefunction
for G being sequence of (set_of_random_variables_on (Special_SigmaField2,Borel_Sets)) st ( for d being Nat holds
( Change_Element_to_Func (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 (s,r,(Change_Element_to_Func (G,s)))),Prob) ) ) )
assume A0: r > 0 ; :: thesis: for jpi being pricefunction
for G being sequence of (set_of_random_variables_on (Special_SigmaField2,Borel_Sets)) st ( for d being Nat holds
( Change_Element_to_Func (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 (s,r,(Change_Element_to_Func (G,s)))),Prob) ) )
let jpi be pricefunction ; :: thesis: for G being sequence of (set_of_random_variables_on (Special_SigmaField2,Borel_Sets)) st ( for d being Nat holds
( Change_Element_to_Func (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 (s,r,(Change_Element_to_Func (G,s)))),Prob) ) )
let G be sequence of (set_of_random_variables_on (Special_SigmaField2,Borel_Sets)); :: thesis: ( ( for d being Nat holds
( Change_Element_to_Func (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 ) ) implies ( Risk_neutral_measure_exists_wrt G,jpi,r & ( for s being Nat holds jpi . s = expect ((Real_RV (s,r,(Change_Element_to_Func (G,s)))),Prob) ) ) )
assume A01: for d being Nat holds
( Change_Element_to_Func (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 ) ; :: thesis: ( Risk_neutral_measure_exists_wrt G,jpi,r & ( for s being Nat holds jpi . s = expect ((Real_RV (s,r,(Change_Element_to_Func (G,s)))),Prob) ) )
for s being Nat holds jpi . s = expect ((Real_RV (s,r,(Change_Element_to_Func (G,s)))),Prob)

proof

let s be Nat; :: thesis: jpi . s = expect ((Real_RV (s,r,(Change_Element_to_Func (G,s)))),Prob)
set RV = Change_Element_to_Func (G,s);
( Change_Element_to_Func (G,s) = {1,2,3,4} --> (In (((jpi . s) * (1 + r)),REAL)) & Change_Element_to_Func (G,s) is_integrable_on Prob & Change_Element_to_Func (G,s) is_simple_func_in Special_SigmaField2 ) by A01;
hence jpi . s = expect ((Real_RV (s,r,(Change_Element_to_Func (G,s)))),Prob) by A0, ThArb; :: thesis: verum

end;

hence ( Risk_neutral_measure_exists_wrt G,jpi,r & ( for s being Nat holds jpi . s = expect ((Real_RV (s,r,(Change_Element_to_Func (G,s)))),Prob) ) ) ; :: thesis: verum