set RVO = (Omega --> K) - RV;
set g2 = chi ((((Omega --> K) - RV) " [.0,+infty.[),Omega);
set PO = Put-Option (RV,K);
reconsider K = K as Element of REAL by XREAL_0:def 1;
Omega --> K is random_variable of F, Borel_Sets by FINANCE3:10;
then ((Omega --> K) - RV) " [.0,+infty.[ is Element of F by Lemma00;
then reconsider g2 = chi ((((Omega --> K) - RV) " [.0,+infty.[),Omega) as random_variable of F, Borel_Sets by ZZZ;
reconsider RVO = (Omega --> K) - RV as random_variable of F, Borel_Sets by TH1;
Put-Option (RV,K) = g2 (#) RVO by JA3;
hence Put-Option (RV,K) is random_variable of F, Borel_Sets by FINANCE2:25; :: thesis: verum