set RVO = (Omega --> K) - RV;
reconsider g2 = chi ((((Omega --> K) - RV) " [.0,+infty.[),Omega) as Function of Omega,REAL by JA2;
set PO = Put-Option (RV,K);
g2 is random_variable of F, Borel_Sets

proof

for x being set st x in Borel_Sets holds
g2 " x in F

proof

let x be set ; :: thesis: ( x in Borel_Sets implies g2 " x in F )
assume x in Borel_Sets ; :: thesis: g2 " x in F
then reconsider x = x as Element of Borel_Sets ;
g2 " x in F

proof

per cases ( ( 1 in x & 0 in x ) or ( 1 in x & not 0 in x ) or ( not 1 in x & 0 in x ) or ( not 1 in x & not 0 in x ) ) ;

suppose SB1: ( 1 in x & 0 in x ) ; :: thesis: g2 " x in F

g2 " x = Omega

proof

for x2 being object holds
( x2 in g2 " x iff x2 in Omega )

proof

let x2 be object ; :: thesis: ( x2 in g2 " x iff x2 in Omega )
( x2 in Omega implies x2 in g2 " x )

proof

assume ASSI: x2 in Omega ; :: thesis: x2 in g2 " x

per cases ( x2 in ((Omega --> K) - RV) " [.0,+infty.[ or not x2 in ((Omega --> K) - RV) " [.0,+infty.[ ) ;

suppose x2 in ((Omega --> K) - RV) " [.0,+infty.[ ; :: thesis: x2 in g2 " x

then L0: g2 . x2 in x by SB1, FUNCT_3:def 3;
reconsider x2 = x2 as Element of Omega by ASSI;
x2 in dom g2 by ASSI, FUNCT_2:def 1;
hence x2 in g2 " x by L0, FUNCT_1:def 7; :: thesis: verum

end;

suppose SP1: not x2 in ((Omega --> K) - RV) " [.0,+infty.[ ; :: thesis: x2 in g2 " x

reconsider x2 = x2 as Element of Omega by ASSI;
L0: g2 . x2 in x by SB1, SP1, FUNCT_3:def 3;
x2 in dom g2 by ASSI, FUNCT_2:def 1;
hence x2 in g2 " x by L0, FUNCT_1:def 7; :: thesis: verum

end;

end;

end;

hence ( x2 in g2 " x iff x2 in Omega ) ; :: thesis: verum

end;

hence g2 " x = Omega by TARSKI:2; :: thesis: verum

end;

hence g2 " x in F by PROB_1:5; :: thesis: verum

end;

suppose SB1: ( 1 in x & not 0 in x ) ; :: thesis: g2 " x in F

for x2 being object holds
( x2 in g2 " x iff x2 in ((Omega --> K) - RV) " [.0,+infty.[ )

proof

let x2 be object ; :: thesis: ( x2 in g2 " x iff x2 in ((Omega --> K) - RV) " [.0,+infty.[ )
thus ( x2 in g2 " x implies x2 in ((Omega --> K) - RV) " [.0,+infty.[ ) :: thesis: ( x2 in ((Omega --> K) - RV) " [.0,+infty.[ implies x2 in g2 " x )

proof

assume x2 in g2 " x ; :: thesis: x2 in ((Omega --> K) - RV) " [.0,+infty.[
then ( x2 in dom g2 & g2 . x2 in x ) by FUNCT_1:def 7;
hence x2 in ((Omega --> K) - RV) " [.0,+infty.[ by SB1, FUNCT_3:def 3; :: thesis: verum

end;

assume ASH: x2 in ((Omega --> K) - RV) " [.0,+infty.[ ; :: thesis: x2 in g2 " x
then reconsider x2 = x2 as Element of Omega ;
l0: dom g2 = Omega by FUNCT_2:def 1;
g2 . x2 in x by SB1, ASH, FUNCT_3:def 3;
hence x2 in g2 " x by l0, FUNCT_1:def 7; :: thesis: verum

end;

then L00: g2 " x = ((Omega --> K) - RV) " [.0,+infty.[ by TARSKI:2;
L0: [.0,+infty.[ is Event of Borel_Sets by FINANCE1:3;
(Omega --> K) - RV is random_variable of F, Borel_Sets by TH1;
then (Omega --> K) - RV is_random_variable_on F, Borel_Sets by RANDOM_3:def 1;
hence g2 " x in F by L00, L0; :: thesis: verum

end;

suppose SB1: ( not 1 in x & 0 in x ) ; :: thesis: g2 " x in F

for x2 being object holds
( x2 in g2 " x iff x2 in Omega \ (((Omega --> K) - RV) " [.0,+infty.[) )

proof

let x2 be object ; :: thesis: ( x2 in g2 " x iff x2 in Omega \ (((Omega --> K) - RV) " [.0,+infty.[) )
thus ( x2 in g2 " x implies x2 in Omega \ (((Omega --> K) - RV) " [.0,+infty.[) ) :: thesis: ( x2 in Omega \ (((Omega --> K) - RV) " [.0,+infty.[) implies x2 in g2 " x )

proof

assume ASSK: x2 in g2 " x ; :: thesis: x2 in Omega \ (((Omega --> K) - RV) " [.0,+infty.[)
then reconsider x2 = x2 as Element of Omega ;
g2 . x2 in x by ASSK, FUNCT_1:def 7;
then not x2 in ((Omega --> K) - RV) " [.0,+infty.[ by FUNCT_3:def 3, SB1;
hence x2 in Omega \ (((Omega --> K) - RV) " [.0,+infty.[) by XBOOLE_0:def 5; :: thesis: verum

end;

assume l0: x2 in Omega \ (((Omega --> K) - RV) " [.0,+infty.[) ; :: thesis: x2 in g2 " x
then L0: ( x2 in Omega & not x2 in ((Omega --> K) - RV) " [.0,+infty.[ ) by XBOOLE_0:def 5;
reconsider x2 = x2 as Element of Omega by XBOOLE_0:def 5, l0;
l1: Omega = dom g2 by FUNCT_2:def 1;
g2 . x2 = 0 by L0, FUNCT_3:def 3;
hence x2 in g2 " x by l1, FUNCT_1:def 7, SB1; :: thesis: verum

end;

then P1: g2 " x = Omega \ (((Omega --> K) - RV) " [.0,+infty.[) by TARSKI:2;
reconsider Omega = Omega as Event of F by PROB_1:5;
P3: [.0,+infty.[ is Event of Borel_Sets by FINANCE1:3;
(Omega --> K) - RV is random_variable of F, Borel_Sets by TH1;
then (Omega --> K) - RV is_random_variable_on F, Borel_Sets by RANDOM_3:def 1;
then ((Omega --> K) - RV) " [.0,+infty.[ is Event of F by P3;
then Omega \ (((Omega --> K) - RV) " [.0,+infty.[) is Event of F by PROB_1:24;
hence g2 " x in F by P1; :: thesis: verum

end;

suppose SB1: ( not 1 in x & not 0 in x ) ; :: thesis: g2 " x in F

g2 " x c= {}

proof

let w3 be object ; :: according to TARSKI:def 3 :: thesis: ( not w3 in g2 " x or w3 in {} )
assume L1: w3 in g2 " x ; :: thesis: w3 in {}
then reconsider w3 = w3 as Element of Omega ;

per cases ( w3 in ((Omega --> K) - RV) " [.0,+infty.[ or not w3 in ((Omega --> K) - RV) " [.0,+infty.[ ) ;

suppose w3 in ((Omega --> K) - RV) " [.0,+infty.[ ; :: thesis: w3 in {}

then g2 . w3 = 1 by FUNCT_3:def 3;
hence w3 in {} by L1, FUNCT_1:def 7, SB1; :: thesis: verum

end;

suppose not w3 in ((Omega --> K) - RV) " [.0,+infty.[ ; :: thesis: w3 in {}

then g2 . w3 = 0 by FUNCT_3:def 3;
hence w3 in {} by L1, FUNCT_1:def 7, SB1; :: thesis: verum

end;

end;

end;

then g2 " x = {} ;
hence g2 " x in F by PROB_1:4; :: thesis: verum

end;

end;

end;

hence g2 " x in F ; :: thesis: verum

end;

then g2 is_random_variable_on F, Borel_Sets ;
hence g2 is random_variable of F, Borel_Sets by RANDOM_3:def 1; :: thesis: verum

end;

then reconsider g2 = g2 as random_variable of F, Borel_Sets ;
reconsider RVO = (Omega --> K) - RV as random_variable of F, Borel_Sets by TH1;
Put-Option (RV,K) = g2 (#) RVO by JA3;
hence Put-Option (RV,K) is random_variable of F, Borel_Sets by FINANCE2:25; :: thesis: verum