let Prob be Probability of Special_SigmaField2 ; :: thesis: 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 )
set F2 = Special_SigmaField2 ;
set Omega2 = {1,2,3,4};
let r be Real; :: thesis: ( r > 0 implies 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 ) )
assume ASSJ: r > 0 ; :: thesis: 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 )
let jpi be pricefunction ; :: thesis: 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 )
let d be Nat; :: thesis: 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 )
deffunc H₁( Element of {1,2,3,4}) -> Element of REAL = In (((jpi . d) * (1 + r)),REAL);
consider f being Function of {1,2,3,4},REAL such that
A1: for d being Element of {1,2,3,4} holds f . d = H₁(d) from FUNCT_2:sch 4();
set g = {1,2,3,4} --> (In (((jpi . d) * (1 + r)),REAL));
b1: ( dom f = {1,2,3,4} & dom ({1,2,3,4} --> (In (((jpi . d) * (1 + r)),REAL))) = {1,2,3,4} ) by FUNCT_2:def 1;
AA: d in NAT by ORDINAL1:def 12;
for x being object st x in dom f holds
f . x = ({1,2,3,4} --> (In (((jpi . d) * (1 + r)),REAL))) . x

proof

let x be object ; :: thesis: ( x in dom f implies f . x = ({1,2,3,4} --> (In (((jpi . d) * (1 + r)),REAL))) . x )
assume x in dom f ; :: thesis: f . x = ({1,2,3,4} --> (In (((jpi . d) * (1 + r)),REAL))) . x
then reconsider x = x as Element of {1,2,3,4} ;
f . x = In (((jpi . d) * (1 + r)),REAL) by A1;
hence f . x = ({1,2,3,4} --> (In (((jpi . d) * (1 + r)),REAL))) . x ; :: thesis: verum

end;

then ff: f = {1,2,3,4} --> (In (((jpi . d) * (1 + r)),REAL)) by b1;
then reconsider f = f as Real-Valued-Random-Variable of Special_SigmaField2 by FINANCE3:10, RANDOM_3:7;
zz: ( {1,2,3,4} in Special_SigmaField2 & dom (R_EAL f) = {1,2,3,4} ) by PROB_1:5, FUNCT_2:def 1;
for x being object st x in dom f holds
(R_EAL f) . x = In (((jpi . d) * (1 + r)),REAL) by ff, FUNCOP_1:7;
then Fin3: f is_simple_func_in Special_SigmaField2 by MESFUNC6:2, zz, MESFUNC6:49;
reconsider g = f as random_variable of Special_SigmaField2 , Borel_Sets by ff, FINANCE3:10;
reconsider fREAL = R_EAL f as random_variable of Special_SigmaField2 , Borel_Sets by ff, FINANCE3:10;
reconsider FOmega = {1,2,3,4} as Element of Special_SigmaField2 by PROB_1:5;
Q1: FOmega = dom (R_EAL f) by FUNCT_2:def 1;
f is_integrable_on P2M Prob

proof

R_EAL f is_integrable_on P2M Prob

proof

( R_EAL f is FOmega -measurable & integral+ ((P2M Prob),(max+ (R_EAL f))) < +infty & integral+ ((P2M Prob),(max- (R_EAL f))) < +infty )

proof

Q2: R_EAL f is FOmega -measurable

proof

for r being Real holds FOmega /\ (less_dom ((R_EAL f),r)) in Special_SigmaField2

proof

let r be Real; :: thesis: FOmega /\ (less_dom ((R_EAL f),r)) in Special_SigmaField2
set WX = { w where w is Element of {1,2,3,4} : fREAL . w < r } ;
W1: FOmega /\ (less_dom (fREAL,r)) = { w where w is Element of {1,2,3,4} : fREAL . w < r }

proof

for x being object holds
( x in FOmega /\ (less_dom (fREAL,r)) iff x in { w where w is Element of {1,2,3,4} : fREAL . w < r } )

proof

let x be object ; :: thesis: ( x in FOmega /\ (less_dom (fREAL,r)) iff x in { w where w is Element of {1,2,3,4} : fREAL . w < r } )
thus ( x in FOmega /\ (less_dom (fREAL,r)) implies x in { w where w is Element of {1,2,3,4} : fREAL . w < r } ) :: thesis: ( x in { w where w is Element of {1,2,3,4} : fREAL . w < r } implies x in FOmega /\ (less_dom (fREAL,r)) )

proof

assume x in FOmega /\ (less_dom (fREAL,r)) ; :: thesis: x in { w where w is Element of {1,2,3,4} : fREAL . w < r }
then ( x in FOmega & x in less_dom (fREAL,r) ) by XBOOLE_0:def 4;
then ( x in FOmega & x in dom fREAL & fREAL . x < r ) by MESFUNC1:def 11;
hence x in { w where w is Element of {1,2,3,4} : fREAL . w < r } ; :: thesis: verum

end;

assume x in { w where w is Element of {1,2,3,4} : fREAL . w < r } ; :: thesis: x in FOmega /\ (less_dom (fREAL,r))
then x in less_dom (fREAL,r) by FINANCE1:9;
then ( x in dom fREAL & fREAL . x < r ) by MESFUNC1:def 11;
then ( x in FOmega & x in less_dom (fREAL,r) ) by MESFUNC1:def 11;
hence x in FOmega /\ (less_dom (fREAL,r)) by XBOOLE_0:def 4; :: thesis: verum

end;

hence FOmega /\ (less_dom (fREAL,r)) = { w where w is Element of {1,2,3,4} : fREAL . w < r } by TARSKI:2; :: thesis: verum

end;

( { w where w is Element of {1,2,3,4} : fREAL . w < r } = g " ].-infty,r.[ & g " ].-infty,r.[ in Special_SigmaField2 )

proof

qq1: for x being object holds
( x in { w where w is Element of {1,2,3,4} : fREAL . w < r } iff x in g " ].-infty,r.[ )

proof

let x be object ; :: thesis: ( x in { w where w is Element of {1,2,3,4} : fREAL . w < r } iff x in g " ].-infty,r.[ )
thus ( x in { w where w is Element of {1,2,3,4} : fREAL . w < r } implies x in g " ].-infty,r.[ ) :: thesis: ( x in g " ].-infty,r.[ implies x in { w where w is Element of {1,2,3,4} : fREAL . w < r } )

proof

assume x in { w where w is Element of {1,2,3,4} : fREAL . w < r } ; :: thesis: x in g " ].-infty,r.[
then consider w being Element of {1,2,3,4} such that
YA1: ( w = x & fREAL . w < r ) ;
reconsider x = x as Element of {1,2,3,4} by YA1;
( -infty < fREAL . x & fREAL . x < r ) by XXREAL_0:12, YA1;
then ( g . x in ].-infty,r.[ & dom g = {1,2,3,4} ) by FUNCT_2:def 1, XXREAL_1:4;
hence x in g " ].-infty,r.[ by FUNCT_1:def 7; :: thesis: verum

end;

assume c0: x in g " ].-infty,r.[ ; :: thesis: x in { w where w is Element of {1,2,3,4} : fREAL . w < r }
then C0: ( x in dom g & g . x in ].-infty,r.[ ) by FUNCT_1:def 7;
reconsider x = x as Element of {1,2,3,4} by c0;
( -infty < g . x & g . x < r & g . x = fREAL . x ) by C0, XXREAL_1:4;
hence x in { w where w is Element of {1,2,3,4} : fREAL . w < r } ; :: thesis: verum

end;

ZZ: ( ].-infty,r.[ is Element of Borel_Sets & g is random_variable of Special_SigmaField2 , Borel_Sets ) by FINANCE1:3;
g is Special_SigmaField2 , Borel_Sets -random_variable-like ;
hence ( { w where w is Element of {1,2,3,4} : fREAL . w < r } = g " ].-infty,r.[ & g " ].-infty,r.[ in Special_SigmaField2 ) by qq1, TARSKI:2, ZZ; :: thesis: verum

end;

hence FOmega /\ (less_dom ((R_EAL f),r)) in Special_SigmaField2 by W1; :: thesis: verum

end;

hence R_EAL f is FOmega -measurable by MESFUNC1:def 16; :: thesis: verum

end;

set fREAL = R_EAL f;
set maxfREAL = max+ (R_EAL f);
U0: ( dom (max+ (R_EAL f)) = dom (R_EAL f) & dom (R_EAL f) = {1,2,3,4} ) by MESFUNC2:def 2, FUNCT_2:def 1;
Fin30: max+ (R_EAL f) is nonnegative

proof

for x being ExtReal st x in rng (max+ (R_EAL f)) holds
0. <= x

proof

let x be ExtReal; :: thesis: ( x in rng (max+ (R_EAL f)) implies 0. <= x )
assume CASS0: x in rng (max+ (R_EAL f)) ; :: thesis: 0. <= x
consider w being object such that
W1: ( w in dom (max+ (R_EAL f)) & (max+ (R_EAL f)) . w = x ) by CASS0, FUNCT_1:def 3;
thus 0. <= x by W1, MESFUNC2:12; :: thesis: verum

end;

hence max+ (R_EAL f) is nonnegative by SUPINF_2:def 12, SUPINF_2:def 9; :: thesis: verum

end;

( integral+ ((P2M Prob),(max+ (R_EAL f))) < +infty & integral+ ((P2M Prob),(max- (R_EAL f))) < +infty )

proof

max+ (R_EAL f) is_simple_func_in Special_SigmaField2

proof

for x being object st x in dom (max+ (R_EAL f)) holds
(max+ (R_EAL f)) . x = In (((jpi . d) * (1 + r)),REAL)

proof

let x be object ; :: thesis: ( x in dom (max+ (R_EAL f)) implies (max+ (R_EAL f)) . x = In (((jpi . d) * (1 + r)),REAL) )
assume x in dom (max+ (R_EAL f)) ; :: thesis: (max+ (R_EAL f)) . x = In (((jpi . d) * (1 + r)),REAL)
then reconsider x = x as Element of {1,2,3,4} ;

per cases ( 0 <= (R_EAL f) . x or 0 > (R_EAL f) . x ) ;

suppose 0 <= (R_EAL f) . x ; :: thesis: (max+ (R_EAL f)) . x = In (((jpi . d) * (1 + r)),REAL)

then S2: max (((R_EAL f) . x),0) = (R_EAL f) . x by XXREAL_0:def 10;
(R_EAL f) . x = In (((jpi . d) * (1 + r)),REAL) by ff;
hence (max+ (R_EAL f)) . x = In (((jpi . d) * (1 + r)),REAL) by U0, MESFUNC2:def 2, S2; :: thesis: verum

end;

suppose S1: 0 > (R_EAL f) . x ; :: thesis: (max+ (R_EAL f)) . x = In (((jpi . d) * (1 + r)),REAL)

( 0 < 1 + r & 0 <= jpi . d ) by AA, FINANCE1:def 2, ASSJ;
hence (max+ (R_EAL f)) . x = In (((jpi . d) * (1 + r)),REAL) by S1, ff; :: thesis: verum

end;

end;

end;

hence max+ (R_EAL f) is_simple_func_in Special_SigmaField2 by MESFUNC6:2, U0; :: thesis: verum

end;

then Schritt1: integral+ ((P2M Prob),(max+ (R_EAL f))) = integral' ((P2M Prob),(max+ (R_EAL f))) by MESFUNC5:77, Fin30;
reconsider myr = (jpi . d) * (1 + r) as Element of REAL by XREAL_0:def 1;
dom (max+ (R_EAL f)) = dom (R_EAL f) by MESFUNC2:def 2;
then y1: dom (max+ (R_EAL f)) = [#] Special_SigmaField2 by FUNCT_2:def 1;
y2: ( 0 < 1 + r & 0 <= jpi . d ) by AA, FINANCE1:def 2, ASSJ;
zz1: for x being object st x in dom (max+ (R_EAL f)) holds
(max+ (R_EAL f)) . x = myr

proof

let x be object ; :: thesis: ( x in dom (max+ (R_EAL f)) implies (max+ (R_EAL f)) . x = myr )
assume S: x in dom (max+ (R_EAL f)) ; :: thesis: (max+ (R_EAL f)) . x = myr
then reconsider x = x as Element of {1,2,3,4} ;
YY1: (max+ (R_EAL f)) . x = max (((R_EAL f) . x),0) by MESFUNC2:def 2, S;

per cases ( (R_EAL f) . x >= 0 or (R_EAL f) . x < 0 ) ;

suppose (R_EAL f) . x >= 0 ; :: thesis: (max+ (R_EAL f)) . x = myr

then (max+ (R_EAL f)) . x = (R_EAL f) . x by YY1, XXREAL_0:def 10;
hence (max+ (R_EAL f)) . x = myr by A1; :: thesis: verum

end;

suppose (R_EAL f) . x < 0 ; :: thesis: (max+ (R_EAL f)) . x = myr

hence (max+ (R_EAL f)) . x = myr by A1, y2; :: thesis: verum

end;

end;

end;

(P2M Prob) . (dom (max+ (R_EAL f))) = 1

proof

dom (max+ (R_EAL f)) = dom (R_EAL f) by MESFUNC2:def 2;
then dom (max+ (R_EAL f)) = [#] Special_SigmaField2 by FUNCT_2:def 1;
hence (P2M Prob) . (dom (max+ (R_EAL f))) = 1 by PROB_1:30; :: thesis: verum

end;

then fin1: integral+ ((P2M Prob),(max+ (R_EAL f))) = myr * 1 by zz1, Schritt1, MESFUNC5:104, y2, y1;
set maxmfREAL = max- (R_EAL f);
YY: ( dom (max- (R_EAL f)) = dom (R_EAL f) & dom (R_EAL f) = {1,2,3,4} ) by MESFUNC2:def 3, FUNCT_2:def 1;
JFin1: max- (R_EAL f) is nonnegative

proof

for x being ExtReal st x in rng (max- (R_EAL f)) holds
0. <= x

proof

let x be ExtReal; :: thesis: ( x in rng (max- (R_EAL f)) implies 0. <= x )
assume x in rng (max- (R_EAL f)) ; :: thesis: 0. <= x
then ex w being object st
( w in dom (max- (R_EAL f)) & (max- (R_EAL f)) . w = x ) by FUNCT_1:def 3;
hence 0. <= x by MESFUNC2:13; :: thesis: verum

end;

hence max- (R_EAL f) is nonnegative by SUPINF_2:def 12, SUPINF_2:def 9; :: thesis: verum

end;

U1: dom (max- (R_EAL f)) in Special_SigmaField2 by YY;
integral+ ((P2M Prob),(max- (R_EAL f))) < +infty

proof

FFF: for x being object st x in dom (max- (R_EAL f)) holds
(max- (R_EAL f)) . x = 0

proof

let x be object ; :: thesis: ( x in dom (max- (R_EAL f)) implies (max- (R_EAL f)) . x = 0 )
assume x in dom (max- (R_EAL f)) ; :: thesis: (max- (R_EAL f)) . x = 0
then reconsider x = x as Element of {1,2,3,4} ;
QQQ1: - ((R_EAL f) . x) = - ((jpi . d) * (1 + r)) by A1;
set mfREAL = - ((R_EAL f) . x);
( 0 < 1 + r & 0 <= jpi . d ) by AA, FINANCE1:def 2, ASSJ;
then QQQ3: max ((- ((R_EAL f) . x)),0) = 0 by XXREAL_0:def 10, QQQ1;
( dom (max- (R_EAL f)) = dom (R_EAL f) & dom (R_EAL f) = {1,2,3,4} ) by MESFUNC2:def 3, FUNCT_2:def 1;
hence (max- (R_EAL f)) . x = 0 by QQQ3, MESFUNC2:def 3; :: thesis: verum

end;

then Schritt1: integral+ ((P2M Prob),(max- (R_EAL f))) = integral' ((P2M Prob),(max- (R_EAL f))) by MESFUNC5:77, JFin1, MESFUNC6:2, U1;
aq2: ( dom (max- (R_EAL f)) = dom (R_EAL f) & dom (R_EAL f) = {1,2,3,4} ) by MESFUNC2:def 3, FUNCT_2:def 1;
integral+ ((P2M Prob),(max- (R_EAL f))) = 0 * ((P2M Prob) . (dom (max- (R_EAL f)))) by Schritt1, MESFUNC5:104, aq2, FFF;
hence integral+ ((P2M Prob),(max- (R_EAL f))) < +infty ; :: thesis: verum

end;

hence ( integral+ ((P2M Prob),(max+ (R_EAL f))) < +infty & integral+ ((P2M Prob),(max- (R_EAL f))) < +infty ) by fin1, XXREAL_0:9; :: thesis: verum

end;

hence ( R_EAL f is FOmega -measurable & integral+ ((P2M Prob),(max+ (R_EAL f))) < +infty & integral+ ((P2M Prob),(max- (R_EAL f))) < +infty ) by Q2; :: thesis: verum

end;

hence R_EAL f is_integrable_on P2M Prob by Q1; :: thesis: verum

end;

hence f is_integrable_on P2M Prob ; :: thesis: verum

end;

hence 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 ) by ff, Fin3; :: thesis: verum