let Omega be non empty set ; :: thesis: for F being SigmaField of Omega
for RV being random_variable of F, Borel_Sets
for K being Element of REAL
for g2 being Function of Omega,REAL st g2 = chi (((RV - (Omega --> K)) " [.0,+infty.[),Omega) holds
Call-Option (RV,K) = g2 (#) (RV - (Omega --> K))
let F be SigmaField of Omega; :: thesis: for RV being random_variable of F, Borel_Sets
for K being Element of REAL
for g2 being Function of Omega,REAL st g2 = chi (((RV - (Omega --> K)) " [.0,+infty.[),Omega) holds
Call-Option (RV,K) = g2 (#) (RV - (Omega --> K))
let RV be random_variable of F, Borel_Sets ; :: thesis: for K being Element of REAL
for g2 being Function of Omega,REAL st g2 = chi (((RV - (Omega --> K)) " [.0,+infty.[),Omega) holds
Call-Option (RV,K) = g2 (#) (RV - (Omega --> K))
let K be Element of REAL ; :: thesis: for g2 being Function of Omega,REAL st g2 = chi (((RV - (Omega --> K)) " [.0,+infty.[),Omega) holds
Call-Option (RV,K) = g2 (#) (RV - (Omega --> K))
let g2 be Function of Omega,REAL; :: thesis: ( g2 = chi (((RV - (Omega --> K)) " [.0,+infty.[),Omega) implies Call-Option (RV,K) = g2 (#) (RV - (Omega --> K)) )
assume A2: g2 = chi (((RV - (Omega --> K)) " [.0,+infty.[),Omega) ; :: thesis: Call-Option (RV,K) = g2 (#) (RV - (Omega --> K))
set RVO = RV - (Omega --> K);
set CO = Call-Option (RV,K);
QQ: ( dom g2 = Omega & dom (RV - (Omega --> K)) = Omega & dom (Call-Option (RV,K)) = Omega ) by FUNCT_2:def 1;
q1: for c being object st c in dom (Call-Option (RV,K)) holds
(Call-Option (RV,K)) . c = (g2 . c) * ((RV - (Omega --> K)) . c)

proof

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

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

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

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

end;

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

ASSJJ0: c in (RV - (Omega --> K)) " ].-infty,0.[

proof

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

end;

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

end;

end;

end;

for x being object st x in dom (Call-Option (RV,K)) holds
(Call-Option (RV,K)) . x = (g2 (#) (RV - (Omega --> K))) . x

proof

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

end;

hence Call-Option (RV,K) = g2 (#) (RV - (Omega --> K)) by QQ; :: thesis: verum