reconsider MyFunc = (Omega --> K) - RV as Function of Omega,REAL ;
deffunc H₁( Element of Omega) -> Element of REAL = SetForCall-Option (MyFunc,$1);
consider f being Function of Omega,REAL such that
A1: for d being Element of Omega holds f . d = H₁(d) from FUNCT_2:sch 4();
for w being Element of Omega holds
( ( MyFunc . w >= 0 implies f . w = ((Omega --> K) - RV) . w ) & ( MyFunc . w < 0 implies f . w = 0 ) )

proof

let w be Element of Omega; :: thesis: ( ( MyFunc . w >= 0 implies f . w = ((Omega --> K) - RV) . w ) & ( MyFunc . w < 0 implies f . w = 0 ) )
f . w = SetForCall-Option (MyFunc,w) by A1;
hence ( ( MyFunc . w >= 0 implies f . w = ((Omega --> K) - RV) . w ) & ( MyFunc . w < 0 implies f . w = 0 ) ) by FINANCE3:def 4; :: thesis: verum

end;

hence ex b₁ being Function of Omega,REAL st
for w being Element of Omega holds
( ( ((Omega --> K) - RV) . w >= 0 implies b₁ . w = ((Omega --> K) - RV) . w ) & ( ((Omega --> K) - RV) . w < 0 implies b₁ . w = 0 ) ) ; :: thesis: verum