let Omega be non empty set ; :: thesis: for F being SigmaField of Omega
for phi being Real_Sequence
for n being Nat
for r being Real
for G being sequence of (set_of_random_variables_on (F,Borel_Sets)) holds { w where w is Element of Omega : PortfolioValueFutExt (n,phi,F,G,w) >= 0 } = (RVPortfolioValueFutExt (phi,F,G,n)) " [.0,+infty.[
let F be SigmaField of Omega; :: thesis: for phi being Real_Sequence
for n being Nat
for r being Real
for G being sequence of (set_of_random_variables_on (F,Borel_Sets)) holds { w where w is Element of Omega : PortfolioValueFutExt (n,phi,F,G,w) >= 0 } = (RVPortfolioValueFutExt (phi,F,G,n)) " [.0,+infty.[
let phi be Real_Sequence; :: thesis: for n being Nat
for r being Real
for G being sequence of (set_of_random_variables_on (F,Borel_Sets)) holds { w where w is Element of Omega : PortfolioValueFutExt (n,phi,F,G,w) >= 0 } = (RVPortfolioValueFutExt (phi,F,G,n)) " [.0,+infty.[
let d be Nat; :: thesis: for r being Real
for G being sequence of (set_of_random_variables_on (F,Borel_Sets)) holds { w where w is Element of Omega : PortfolioValueFutExt (d,phi,F,G,w) >= 0 } = (RVPortfolioValueFutExt (phi,F,G,d)) " [.0,+infty.[
let r be Real; :: thesis: for G being sequence of (set_of_random_variables_on (F,Borel_Sets)) holds { w where w is Element of Omega : PortfolioValueFutExt (d,phi,F,G,w) >= 0 } = (RVPortfolioValueFutExt (phi,F,G,d)) " [.0,+infty.[
let G be sequence of (set_of_random_variables_on (F,Borel_Sets)); :: thesis: { w where w is Element of Omega : PortfolioValueFutExt (d,phi,F,G,w) >= 0 } = (RVPortfolioValueFutExt (phi,F,G,d)) " [.0,+infty.[
set Set1 = { w where w is Element of Omega : PortfolioValueFutExt (d,phi,F,G,w) >= 0 } ;
set Set2 = (RVPortfolioValueFutExt (phi,F,G,d)) " [.0,+infty.[;
for x being object holds
( x in { w where w is Element of Omega : PortfolioValueFutExt (d,phi,F,G,w) >= 0 } iff x in (RVPortfolioValueFutExt (phi,F,G,d)) " [.0,+infty.[ )

proof

let x be object ; :: thesis: ( x in { w where w is Element of Omega : PortfolioValueFutExt (d,phi,F,G,w) >= 0 } iff x in (RVPortfolioValueFutExt (phi,F,G,d)) " [.0,+infty.[ )
thus ( x in { w where w is Element of Omega : PortfolioValueFutExt (d,phi,F,G,w) >= 0 } implies x in (RVPortfolioValueFutExt (phi,F,G,d)) " [.0,+infty.[ ) :: thesis: ( x in (RVPortfolioValueFutExt (phi,F,G,d)) " [.0,+infty.[ implies x in { w where w is Element of Omega : PortfolioValueFutExt (d,phi,F,G,w) >= 0 } )

proof

assume x in { w where w is Element of Omega : PortfolioValueFutExt (d,phi,F,G,w) >= 0 } ; :: thesis: x in (RVPortfolioValueFutExt (phi,F,G,d)) " [.0,+infty.[
then consider w being Element of Omega such that
A1: ( w = x & PortfolioValueFutExt (d,phi,F,G,w) >= 0 ) ;
PortfolioValueFutExt (d,phi,F,G,w) = (RVPortfolioValueFutExt (phi,F,G,d)) . w by FINANCE3:def 1;
then A2: (RVPortfolioValueFutExt (phi,F,G,d)) . w in [.0,+infty.[ by XXREAL_1:3, A1, XXREAL_0:9;
dom (RVPortfolioValueFutExt (phi,F,G,d)) = Omega by FUNCT_2:def 1;
hence x in (RVPortfolioValueFutExt (phi,F,G,d)) " [.0,+infty.[ by A1, A2, FUNCT_1:def 7; :: thesis: verum

end;

assume a1: x in (RVPortfolioValueFutExt (phi,F,G,d)) " [.0,+infty.[ ; :: thesis: x in { w where w is Element of Omega : PortfolioValueFutExt (d,phi,F,G,w) >= 0 }
then A1: ( x in dom (RVPortfolioValueFutExt (phi,F,G,d)) & (RVPortfolioValueFutExt (phi,F,G,d)) . x in [.0,+infty.[ ) by FUNCT_1:def 7;
reconsider x = x as Element of Omega by a1;
( 0 <= (RVPortfolioValueFutExt (phi,F,G,d)) . x & (RVPortfolioValueFutExt (phi,F,G,d)) . x < +infty ) by A1, XXREAL_1:3;
then 0 <= PortfolioValueFutExt (d,phi,F,G,x) by FINANCE3:def 1;
hence x in { w where w is Element of Omega : PortfolioValueFutExt (d,phi,F,G,w) >= 0 } ; :: thesis: verum

end;

hence { w where w is Element of Omega : PortfolioValueFutExt (d,phi,F,G,w) >= 0 } = (RVPortfolioValueFutExt (phi,F,G,d)) " [.0,+infty.[ by TARSKI:2; :: thesis: verum