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 Real
for g2 being Function of Omega,REAL st g2 = chi ((((Omega --> K) - RV) " [.0,+infty.[),Omega) holds
Put-Option (RV,K) = g2 (#) ((Omega --> K) - RV)
let F be SigmaField of Omega; :: thesis: for RV being random_variable of F, Borel_Sets
for K being Real
for g2 being Function of Omega,REAL st g2 = chi ((((Omega --> K) - RV) " [.0,+infty.[),Omega) holds
Put-Option (RV,K) = g2 (#) ((Omega --> K) - RV)
let RV be random_variable of F, Borel_Sets ; :: thesis: for K being Real
for g2 being Function of Omega,REAL st g2 = chi ((((Omega --> K) - RV) " [.0,+infty.[),Omega) holds
Put-Option (RV,K) = g2 (#) ((Omega --> K) - RV)
let K be Real; :: thesis: for g2 being Function of Omega,REAL st g2 = chi ((((Omega --> K) - RV) " [.0,+infty.[),Omega) holds
Put-Option (RV,K) = g2 (#) ((Omega --> K) - RV)
let g2 be Function of Omega,REAL; :: thesis: ( g2 = chi ((((Omega --> K) - RV) " [.0,+infty.[),Omega) implies Put-Option (RV,K) = g2 (#) ((Omega --> K) - RV) )
assume K1: g2 = chi ((((Omega --> K) - RV) " [.0,+infty.[),Omega) ; :: thesis: Put-Option (RV,K) = g2 (#) ((Omega --> K) - RV)
set PO = Put-Option (RV,K);
set RVO = (Omega --> K) - RV;
h1: ( dom g2 = Omega & dom ((Omega --> K) - RV) = Omega & dom (Put-Option (RV,K)) = Omega ) by FUNCT_2:def 1;
q1: ( dom (Put-Option (RV,K)) = (dom g2) /\ (dom ((Omega --> K) - RV)) & ( for c being object st c in dom (Put-Option (RV,K)) holds
(Put-Option (RV,K)) . c = (g2 . c) * (((Omega --> K) - RV) . c) ) )

proof

for c being object st c in dom (Put-Option (RV,K)) holds
(Put-Option (RV,K)) . c = (g2 . c) * (((Omega --> K) - RV) . c)

proof

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

proof

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

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

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

end;

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

then k1: ( c in Omega & not c in ((Omega --> K) - RV) " [.0,+infty.[ ) ;
ASSJJ0: c in ((Omega --> K) - RV) " ].-infty,0.[

proof

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

end;

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

end;

end;

end;

hence (Put-Option (RV,K)) . c = (g2 . c) * (((Omega --> K) - RV) . c) ; :: thesis: verum

end;

hence ( dom (Put-Option (RV,K)) = (dom g2) /\ (dom ((Omega --> K) - RV)) & ( for c being object st c in dom (Put-Option (RV,K)) holds
(Put-Option (RV,K)) . c = (g2 . c) * (((Omega --> K) - RV) . c) ) ) by h1; :: thesis: verum

end;

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

proof

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

end;

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