reconsider MyFunc = RV - (Omega --> K) 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 = (RV - (Omega --> K)) . w ) & ( MyFunc . w < 0 implies f . w = 0 ) )

proof

let w be Element of Omega; :: thesis: ( ( MyFunc . w >= 0 implies f . w = (RV - (Omega --> K)) . w ) & ( MyFunc . w < 0 implies f . w = 0 ) )
thus ( MyFunc . w >= 0 implies f . w = (RV - (Omega --> K)) . w ) :: thesis: ( MyFunc . w < 0 implies f . w = 0 )

proof

assume B1: MyFunc . w >= 0 ; :: thesis: f . w = (RV - (Omega --> K)) . w
f . w = SetForCall-Option (MyFunc,w) by A1;
hence f . w = (RV - (Omega --> K)) . w by Def89, B1; :: thesis: verum

end;

assume B1: MyFunc . w < 0 ; :: thesis: f . w = 0
f . w = SetForCall-Option (MyFunc,w) by A1;
hence f . w = 0 by Def89, B1; :: thesis: verum

end;

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