set RVO = RV - (Omega --> K);
consider g2 being Function such that
A2: g2 = chi (((RV - (Omega --> K)) " [.0,+infty.[),Omega) ;
g2 is random_variable of F, Borel_Sets

proof

rng g2 c= {0,1} by RELAT_1:def 19, A2;
then rng g2 c= REAL by H0;
then ( g2 is Function of (dom g2),REAL & dom g2 = Omega ) by FUNCT_2:2, FUNCT_2:def 1, A2;
then reconsider g2 = g2 as Function of Omega,REAL ;
for x being set st x in Borel_Sets holds
g2 " x in F

proof

let x be set ; :: thesis:
assume x in Borel_Sets ; :: thesis:
then reconsider x = x as Element of Borel_Sets ;

per cases ;

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

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 Omega implies x2 in g2 " x )

proof

assume ASSI: x2 in Omega ; :: thesis:

per cases ;

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

then L0: g2 . x2 in x by SB1, A2, 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:

end;

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

then L0: g2 . x2 in x by SB1, A2, FUNCT_3:def 3, ASSI;
x2 in dom g2 by ASSI, FUNCT_2:def 1;
hence x2 in g2 " x by L0, FUNCT_1:def 7; :: thesis:

end;

end;

end;

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

end;

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

end;

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

end;

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

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

proof

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

proof

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

end;

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

end;

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

end;

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

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

proof

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

proof

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

end;

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

end;

then P1: g2 " x = Omega \ ((RV - (Omega --> K)) " [.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;
RV - (Omega --> K) is random_variable of F, Borel_Sets by FINANCE3:11;
then RV - (Omega --> K) is_random_variable_on F, Borel_Sets by RANDOM_3:def 1;
then (RV - (Omega --> K)) " [.0,+infty.[ is Event of F by P3;
then Omega \ ((RV - (Omega --> K)) " [.0,+infty.[) is Event of F by PROB_1:24;
hence g2 " x in F by P1; :: thesis:

end;

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

g2 " x c= {}

proof

let w3 be object ; :: according to TARSKI:def 3 :: thesis:
assume L1: w3 in g2 " x ; :: thesis:
reconsider w3 = w3 as Element of Omega by L1;

per cases ;

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

then not g2 . w3 in x by SB1, A2, FUNCT_3:def 3;
hence w3 in {} by L1, FUNCT_1:def 7; :: thesis:

end;

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

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

end;

end;

end;

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

end;

end;

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:

end;

then reconsider g2 = g2 as random_variable of F, Borel_Sets ;
set RVO = RV - (Omega --> K);
reconsider RVO = RV - (Omega --> K) as random_variable of F, Borel_Sets by FINANCE3:11;
set CO = Call-Option (RV,K);
Call-Option (RV,K) = g2 (#) RVO

proof

q1: for c being object st c in dom (Call-Option (RV,K)) holds
(Call-Option (RV,K)) . c = (g2 . c) * (RVO . c)

proof

let c be object ; :: thesis:
assume c in dom (Call-Option (RV,K)) ; :: thesis:
then reconsider c = c as Element of Omega ;
(Call-Option (RV,K)) . c = (g2 . c) * (RVO . c)

proof

per cases ;

suppose ASSJJ0: c in RVO " [.0,+infty.[ ; :: thesis:

then ZW0: g2 . c = 1 by A2, FUNCT_3:def 3;
( c in dom RVO & RVO . c in [.0,+infty.[ ) by ASSJJ0, FUNCT_1:def 7;
then ( 0 <= RVO . c & RVO . c < +infty ) by XXREAL_1:3;
hence (Call-Option (RV,K)) . c = (g2 . c) * (RVO . c) by ZW0, FINANCE3:def 5; :: thesis:

end;

suppose ASSJJ00: not c in RVO " [.0,+infty.[ ; :: thesis:

K1: ( c in Omega & not c in RVO " [.0,+infty.[ ) by ASSJJ00;
ASSJJ0: c in RVO " ].-infty,0.[

proof

( not c in dom RVO or not RVO . c in [.0,+infty.[ ) by ASSJJ00, FUNCT_1:def 7;
then ( not c in Omega or not RVO . c in [.0,+infty.[ ) by FUNCT_2:def 1;
then ( RV . c in ].-infty,+infty.[ & -infty < RVO . c & RVO . c < 0 ) by XXREAL_1:224, XXREAL_0:12, XXREAL_0:9, XXREAL_1:3;
then ( c in dom RVO & RVO . c in ].-infty,0.[ ) by K1, FUNCT_2:def 1, XXREAL_1:4;
hence c in RVO " ].-infty,0.[ by FUNCT_1:def 7; :: thesis:

end;

ZW0: g2 . c = 0 by A2, ASSJJ00, FUNCT_3:def 3;
( c in dom RVO & RVO . c in ].-infty,0.[ ) by ASSJJ0, FUNCT_1:def 7;
then ( -infty < RVO . c & RVO . c < 0 ) by XXREAL_1:4;
hence (Call-Option (RV,K)) . c = (g2 . c) * (RVO . c) by ZW0, FINANCE3:def 5; :: thesis:

end;

end;

end;

hence (Call-Option (RV,K)) . c = (g2 . c) * (RVO . c) ; :: thesis:

end;

W1: ( dom (Call-Option (RV,K)) = Omega & dom g2 = Omega & dom RVO = Omega ) by FUNCT_2:def 1;
for x being object st x in dom (Call-Option (RV,K)) holds
(Call-Option (RV,K)) . x = (g2 (#) RVO) . x

proof

let x be object ; :: thesis:
assume x in dom (Call-Option (RV,K)) ; :: thesis:
then (Call-Option (RV,K)) . x = (g2 . x) * (RVO . x) by q1;
hence (Call-Option (RV,K)) . x = (g2 (#) RVO) . x by VALUED_1:5; :: thesis:

end;

hence Call-Option (RV,K) = g2 (#) RVO by W1; :: thesis:

end;

hence Call-Option (RV,K) is random_variable of F, Borel_Sets by FINANCE2:25; :: thesis: