let Omega be non empty set ; :: thesis: for F being SigmaField of Omega
for phi being Real_Sequence
for d 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 (d,phi,F,G,w) > 0 } = (RVPortfolioValueFutExt (phi,F,G,d)) " ].0,+infty.[
let F be SigmaField of Omega; :: thesis: for phi being Real_Sequence
for d 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 (d,phi,F,G,w) > 0 } = (RVPortfolioValueFutExt (phi,F,G,d)) " ].0,+infty.[
let phi be Real_Sequence; :: thesis: for d 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 (d,phi,F,G,w) > 0 } = (RVPortfolioValueFutExt (phi,F,G,d)) " ].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 ) ;
reconsider x = x as Element of Omega by A1;
( 0 < (RVPortfolioValueFutExt (phi,F,G,d)) . w & (RVPortfolioValueFutExt (phi,F,G,d)) . w < +infty ) by A1, XXREAL_0:9, FINANCE3:def 1;
then A2: (RVPortfolioValueFutExt (phi,F,G,d)) . w in ].0,+infty.[ by XXREAL_1:4;
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:4;
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