let Omega be non empty set ; for F being SigmaField of Omega
for phi being Real_Sequence
for jpi being pricefunction
for d, d2 being Nat st d2 = d - 1 holds
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 : PortfolioValueFut (d,phi,F,G,w) >= (1 + r) * (BuyPortfolio (phi,jpi,d)) } = ((RVPortfolioValueFut (phi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (phi,jpi,d))))) " [.0,+infty.[
let F be SigmaField of Omega; for phi being Real_Sequence
for jpi being pricefunction
for d, d2 being Nat st d2 = d - 1 holds
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 : PortfolioValueFut (d,phi,F,G,w) >= (1 + r) * (BuyPortfolio (phi,jpi,d)) } = ((RVPortfolioValueFut (phi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (phi,jpi,d))))) " [.0,+infty.[
let phi be Real_Sequence; for jpi being pricefunction
for d, d2 being Nat st d2 = d - 1 holds
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 : PortfolioValueFut (d,phi,F,G,w) >= (1 + r) * (BuyPortfolio (phi,jpi,d)) } = ((RVPortfolioValueFut (phi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (phi,jpi,d))))) " [.0,+infty.[
let jpi be pricefunction ; for d, d2 being Nat st d2 = d - 1 holds
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 : PortfolioValueFut (d,phi,F,G,w) >= (1 + r) * (BuyPortfolio (phi,jpi,d)) } = ((RVPortfolioValueFut (phi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (phi,jpi,d))))) " [.0,+infty.[
let d, d2 be Nat; ( d2 = d - 1 implies 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 : PortfolioValueFut (d,phi,F,G,w) >= (1 + r) * (BuyPortfolio (phi,jpi,d)) } = ((RVPortfolioValueFut (phi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (phi,jpi,d))))) " [.0,+infty.[ )
assume a10:
d2 = d - 1
; 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 : PortfolioValueFut (d,phi,F,G,w) >= (1 + r) * (BuyPortfolio (phi,jpi,d)) } = ((RVPortfolioValueFut (phi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (phi,jpi,d))))) " [.0,+infty.[
let r be Real; for G being sequence of (set_of_random_variables_on (F,Borel_Sets)) holds { w where w is Element of Omega : PortfolioValueFut (d,phi,F,G,w) >= (1 + r) * (BuyPortfolio (phi,jpi,d)) } = ((RVPortfolioValueFut (phi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (phi,jpi,d))))) " [.0,+infty.[
let G be sequence of (set_of_random_variables_on (F,Borel_Sets)); { w where w is Element of Omega : PortfolioValueFut (d,phi,F,G,w) >= (1 + r) * (BuyPortfolio (phi,jpi,d)) } = ((RVPortfolioValueFut (phi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (phi,jpi,d))))) " [.0,+infty.[
set Set1 = { w where w is Element of Omega : PortfolioValueFut (d,phi,F,G,w) >= (1 + r) * (BuyPortfolio (phi,jpi,d)) } ;
set Set2 = ((RVPortfolioValueFut (phi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (phi,jpi,d))))) " [.0,+infty.[;
for x being object holds
( x in { w where w is Element of Omega : PortfolioValueFut (d,phi,F,G,w) >= (1 + r) * (BuyPortfolio (phi,jpi,d)) } iff x in ((RVPortfolioValueFut (phi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (phi,jpi,d))))) " [.0,+infty.[ )
proof
let x be
object ;
( x in { w where w is Element of Omega : PortfolioValueFut (d,phi,F,G,w) >= (1 + r) * (BuyPortfolio (phi,jpi,d)) } iff x in ((RVPortfolioValueFut (phi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (phi,jpi,d))))) " [.0,+infty.[ )
thus
(
x in { w where w is Element of Omega : PortfolioValueFut (d,phi,F,G,w) >= (1 + r) * (BuyPortfolio (phi,jpi,d)) } implies
x in ((RVPortfolioValueFut (phi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (phi,jpi,d))))) " [.0,+infty.[ )
( x in ((RVPortfolioValueFut (phi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (phi,jpi,d))))) " [.0,+infty.[ implies x in { w where w is Element of Omega : PortfolioValueFut (d,phi,F,G,w) >= (1 + r) * (BuyPortfolio (phi,jpi,d)) } )proof
assume
x in { w where w is Element of Omega : PortfolioValueFut (d,phi,F,G,w) >= (1 + r) * (BuyPortfolio (phi,jpi,d)) }
;
x in ((RVPortfolioValueFut (phi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (phi,jpi,d))))) " [.0,+infty.[
then consider w being
Element of
Omega such that A1:
(
w = x &
PortfolioValueFut (
d,
phi,
F,
G,
w)
>= (1 + r) * (BuyPortfolio (phi,jpi,d)) )
;
reconsider x =
x as
Element of
Omega by A1;
set myel =
(1 + r) * (BuyPortfolio (phi,jpi,d));
a2:
PortfolioValueFut (
(d2 + 1),
phi,
F,
G,
w)
= (RVPortfolioValueFut (phi,F,G,d2)) . w
by FINANCE3:def 3;
((RVPortfolioValueFut (phi,F,G,d2)) . x) - ((Omega --> ((1 + r) * (BuyPortfolio (phi,jpi,d)))) . x) >= 0
by XREAL_1:48, A1, a2, a10;
then Q1:
((RVPortfolioValueFut (phi,F,G,d2)) . x) + ((- 1) * ((Omega --> ((1 + r) * (BuyPortfolio (phi,jpi,d)))) . x)) >= 0
;
x in dom (Omega --> ((1 + r) * (BuyPortfolio (phi,jpi,d))))
;
then
x in dom ((- 1) (#) (Omega --> ((1 + r) * (BuyPortfolio (phi,jpi,d)))))
by VALUED_1:def 5;
then
((RVPortfolioValueFut (phi,F,G,d2)) . x) + (((- 1) (#) (Omega --> ((1 + r) * (BuyPortfolio (phi,jpi,d))))) . x) >= 0
by Q1, VALUED_1:def 5;
then
((RVPortfolioValueFut (phi,F,G,d2)) + (- (Omega --> ((1 + r) * (BuyPortfolio (phi,jpi,d)))))) . x >= 0
by VALUED_1:1;
then T1:
((RVPortfolioValueFut (phi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (phi,jpi,d))))) . x in [.0,+infty.[
by XXREAL_1:3, XXREAL_0:9;
dom ((RVPortfolioValueFut (phi,F,G,d2)) + (- (Omega --> ((1 + r) * (BuyPortfolio (phi,jpi,d)))))) = Omega /\ Omega
by FUNCT_2:def 1;
hence
x in ((RVPortfolioValueFut (phi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (phi,jpi,d))))) " [.0,+infty.[
by T1, FUNCT_1:def 7;
verum
end;
assume a1:
x in ((RVPortfolioValueFut (phi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (phi,jpi,d))))) " [.0,+infty.[
;
x in { w where w is Element of Omega : PortfolioValueFut (d,phi,F,G,w) >= (1 + r) * (BuyPortfolio (phi,jpi,d)) }
then A1:
(
x in dom ((RVPortfolioValueFut (phi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (phi,jpi,d))))) &
((RVPortfolioValueFut (phi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (phi,jpi,d))))) . x in [.0,+infty.[ )
by FUNCT_1:def 7;
set my1 =
(1 + r) * (BuyPortfolio (phi,jpi,d));
set my2 =
(RVPortfolioValueFut (phi,F,G,d2)) . x;
reconsider x =
x as
Element of
Omega by a1;
set RVmyx =
((RVPortfolioValueFut (phi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (phi,jpi,d))))) . x;
((RVPortfolioValueFut (phi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (phi,jpi,d))))) . x = ((RVPortfolioValueFut (phi,F,G,d2)) . x) + (((- 1) (#) (Omega --> ((1 + r) * (BuyPortfolio (phi,jpi,d))))) . x)
by VALUED_1:1;
then
((RVPortfolioValueFut (phi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (phi,jpi,d))))) . x = ((RVPortfolioValueFut (phi,F,G,d2)) . x) + ((- 1) * ((Omega --> ((1 + r) * (BuyPortfolio (phi,jpi,d)))) . x))
by VALUED_1:6;
then
0 <= ((RVPortfolioValueFut (phi,F,G,d2)) . x) - ((Omega --> ((1 + r) * (BuyPortfolio (phi,jpi,d)))) . x)
by A1, XXREAL_1:3;
then
0 <= ((RVPortfolioValueFut (phi,F,G,d2)) . x) - ((1 + r) * (BuyPortfolio (phi,jpi,d)))
;
then
0 + ((1 + r) * (BuyPortfolio (phi,jpi,d))) <= (RVPortfolioValueFut (phi,F,G,d2)) . x
by XREAL_1:19;
then
(1 + r) * (BuyPortfolio (phi,jpi,d)) <= PortfolioValueFut (
(d2 + 1),
phi,
F,
G,
x)
by FINANCE3:def 3;
hence
x in { w where w is Element of Omega : PortfolioValueFut (d,phi,F,G,w) >= (1 + r) * (BuyPortfolio (phi,jpi,d)) }
by a10;
verum
end;
hence
{ w where w is Element of Omega : PortfolioValueFut (d,phi,F,G,w) >= (1 + r) * (BuyPortfolio (phi,jpi,d)) } = ((RVPortfolioValueFut (phi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (phi,jpi,d))))) " [.0,+infty.[
by TARSKI:2; verum