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.[ 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