reconsider MyFunc = (Omega --> K) - RV as Function of Omega,REAL ;
deffunc H1( 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 = H1(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 b1 being Function of Omega,REAL st
for w being Element of Omega holds
( ( ((Omega --> K) - RV) . w >= 0 implies b1 . w = ((Omega --> K) - RV) . w ) & ( ((Omega --> K) - RV) . w < 0 implies b1 . w = 0 ) ) ; :: thesis: verum