let Prob be Probability of Special_SigmaField2 ; :: thesis: for n being Nat
for r being Real st r > 0 holds
for jpi being pricefunction
for d being Nat
for RV being Real-Valued-Random-Variable of Special_SigmaField2 st RV = {1,2,3,4} --> ((jpi . d) * (1 + r)) & RV is_integrable_on P2M Prob & RV is_simple_func_in Special_SigmaField2 holds
jpi . d = expect ((Real_RV (r,RV)),Prob)
let n be Nat; :: thesis: for r being Real st r > 0 holds
for jpi being pricefunction
for d being Nat
for RV being Real-Valued-Random-Variable of Special_SigmaField2 st RV = {1,2,3,4} --> ((jpi . d) * (1 + r)) & RV is_integrable_on P2M Prob & RV is_simple_func_in Special_SigmaField2 holds
jpi . d = expect ((Real_RV (r,RV)),Prob)
set Omega2 = {1,2,3,4};
set F2 = Special_SigmaField2 ;
let r be Real; :: thesis: ( r > 0 implies for jpi being pricefunction
for d being Nat
for RV being Real-Valued-Random-Variable of Special_SigmaField2 st RV = {1,2,3,4} --> ((jpi . d) * (1 + r)) & RV is_integrable_on P2M Prob & RV is_simple_func_in Special_SigmaField2 holds
jpi . d = expect ((Real_RV (r,RV)),Prob) )
assume A00: r > 0 ; :: thesis: for jpi being pricefunction
for d being Nat
for RV being Real-Valued-Random-Variable of Special_SigmaField2 st RV = {1,2,3,4} --> ((jpi . d) * (1 + r)) & RV is_integrable_on P2M Prob & RV is_simple_func_in Special_SigmaField2 holds
jpi . d = expect ((Real_RV (r,RV)),Prob)
let jpi be pricefunction ; :: thesis: for d being Nat
for RV being Real-Valued-Random-Variable of Special_SigmaField2 st RV = {1,2,3,4} --> ((jpi . d) * (1 + r)) & RV is_integrable_on P2M Prob & RV is_simple_func_in Special_SigmaField2 holds
jpi . d = expect ((Real_RV (r,RV)),Prob)
let d be Nat; :: thesis: for RV being Real-Valued-Random-Variable of Special_SigmaField2 st RV = {1,2,3,4} --> ((jpi . d) * (1 + r)) & RV is_integrable_on P2M Prob & RV is_simple_func_in Special_SigmaField2 holds
jpi . d = expect ((Real_RV (r,RV)),Prob)
let RV be Real-Valued-Random-Variable of Special_SigmaField2; :: thesis: ( RV = {1,2,3,4} --> ((jpi . d) * (1 + r)) & RV is_integrable_on P2M Prob & RV is_simple_func_in Special_SigmaField2 implies jpi . d = expect ((Real_RV (r,RV)),Prob) )
assume ASS0: ( RV = {1,2,3,4} --> ((jpi . d) * (1 + r)) & RV is_integrable_on P2M Prob & RV is_simple_func_in Special_SigmaField2 ) ; :: thesis: jpi . d = expect ((Real_RV (r,RV)),Prob)
set myconst = 1 / (1 + r);
Z1: expect ((Real_RV (r,RV)),Prob) = (1 / (1 + r)) * (expect (RV,Prob)) by ASS0, RANDOM_1:def 2, RANDOM_1:27;
B1: expect (RV,Prob) = Integral ((P2M Prob),RV) by ASS0, RANDOM_1:def 2, RANDOM_1:def 3;
reconsider FOmega = {1,2,3,4} as Element of Special_SigmaField2 by PROB_1:5;
D1: FOmega = dom RV by FUNCT_2:def 1;
SS: ( R_EAL RV = RV & RV is nonnegative )

proof

for x being ExtReal st x in rng RV holds
0. <= x

proof

let x be ExtReal; :: thesis: ( x in rng RV implies 0. <= x )
assume CASS0: x in rng RV ; :: thesis: 0. <= x
consider w being object such that
W1: ( w in dom RV & RV . w = x ) by CASS0, FUNCT_1:def 3;
reconsider w = w as Element of {1,2,3,4} by W1;
0 <= RV . w

proof

d in NAT by ORDINAL1:def 12;
then 0 <= jpi . d by FINANCE1:def 2;
hence 0 <= RV . w by ASS0, A00; :: thesis: verum

end;

hence 0. <= x by W1; :: thesis: verum

end;

hence ( R_EAL RV = RV & RV is nonnegative ) by SUPINF_2:def 12, SUPINF_2:def 9; :: thesis: verum

end;

then expect (RV,Prob) = integral+ ((P2M Prob),(R_EAL RV)) by D1, B1, MESFUNC6:82;
then Q3: expect (RV,Prob) = integral' ((P2M Prob),(R_EAL RV)) by MESFUNC5:77, MESFUNC6:49, ASS0, SS;
set myr = (jpi . d) * (1 + r);
d in NAT by ORDINAL1:def 12;
then TT: 0 <= jpi . d by FINANCE1:def 2;
( ( for x being object st x in dom (R_EAL RV) holds
(R_EAL RV) . x = (jpi . d) * (1 + r) ) & dom (R_EAL RV) in Special_SigmaField2 & 0 <= (jpi . d) * (1 + r) ) by ASS0, FUNCOP_1:7, TT, A00;
then Q4: expect (RV,Prob) = ((jpi . d) * (1 + r)) * ((P2M Prob) . (dom (R_EAL RV))) by Q3, MESFUNC5:104;
( dom (R_EAL RV) = {1,2,3,4} & {1,2,3,4} = [#] Special_SigmaField2 ) by FUNCT_2:def 1;
then expect (RV,Prob) = ((jpi . d) * (1 + r)) * 1 by Q4, PROB_1:30;
then Spec: expect ((Real_RV (r,RV)),Prob) = (jpi . d) * ((1 / (1 + r)) * (1 + r)) by Z1;
1 = (1 * (1 + r)) * ((1 + r) ") by XCMPLX_1:203, A00;
hence jpi . d = expect ((Real_RV (r,RV)),Prob) by Spec; :: thesis: verum