let Prob be Probability of Special_SigmaField2 ; :: thesis: for r being Real st r > 0 holds
for jpi being pricefunction ex 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 )
let r be Real; :: thesis: ( r > 0 implies for jpi being pricefunction ex 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 ) )
assume A1: r > 0 ; :: thesis: for jpi being pricefunction ex 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 )
let jpi be pricefunction ; :: thesis: ex 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 )
deffunc H₁( Nat) -> Element of set_of_random_variables_on (Special_SigmaField2,Borel_Sets) = RVfourth (jpi,r,$1);
consider g being sequence of (set_of_random_variables_on (Special_SigmaField2,Borel_Sets)) such that
A2: for d being Element of NAT holds g . d = H₁(d) from FUNCT_2:sch 4();
take g ; :: thesis: 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 )
let d be Nat; :: thesis: ( 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 )
d in NAT by ORDINAL1:def 12;
then b1: Change_Element_to_Func (g,d) = RVfourth (jpi,r,d) by A2;
ex RV being Real-Valued-Random-Variable of Special_SigmaField2 st
( RV = {1,2,3,4} --> (In (((jpi . d) * (1 + r)),REAL)) & RV is_integrable_on P2M Prob & RV is_simple_func_in Special_SigmaField2 ) by A1, ThArbPrel;
hence ( 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 ) by b1; :: thesis: verum