set RVO = RV - (Omega --> K);
set g2 = chi (((RV - (Omega --> K)) " [.0,+infty.[),Omega);
reconsider g2 = chi (((RV - (Omega --> K)) " [.0,+infty.[),Omega) as random_variable of F, Borel_Sets by LemmaRandom;
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: ( c in dom (Call-Option (RV,K)) implies (Call-Option (RV,K)) . c = (g2 . c) * (RVO . c) )
assume c in dom (Call-Option (RV,K)) ; :: thesis: (Call-Option (RV,K)) . c = (g2 . c) * (RVO . c)
then reconsider c = c as Element of Omega ;
(Call-Option (RV,K)) . c = (g2 . c) * (RVO . c)

proof

per cases ( c in RVO " [.0,+infty.[ or not c in RVO " [.0,+infty.[ ) ;

suppose ASSJJ0: c in RVO " [.0,+infty.[ ; :: thesis: (Call-Option (RV,K)) . c = (g2 . c) * (RVO . c)

then ZW0: g2 . c = 1 by 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: verum

end;

suppose ASSJJ00: not c in RVO " [.0,+infty.[ ; :: thesis: (Call-Option (RV,K)) . c = (g2 . c) * (RVO . c)

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: verum

end;

ZW0: g2 . c = 0 by 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: verum

end;

end;

end;

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

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: ( x in dom (Call-Option (RV,K)) implies (Call-Option (RV,K)) . x = (g2 (#) RVO) . x )
assume x in dom (Call-Option (RV,K)) ; :: thesis: (Call-Option (RV,K)) . x = (g2 (#) RVO) . x
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: verum

end;

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

end;

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