deffunc H_{1}( Element of Omega) -> Element of REAL = (Change_Element_to_Func (F,Borel_Sets,k)) . $1;

ex f being Function of Omega,REAL st

for d being Element of Omega holds f . d = H_{1}(d)
from FUNCT_2:sch 4();

hence ex b_{1} being Function of Omega,REAL st

for w being Element of Omega holds b_{1} . w = (Change_Element_to_Func (F,Borel_Sets,k)) . w
; :: thesis: verum

ex f being Function of Omega,REAL st

for d being Element of Omega holds f . d = H

hence ex b

for w being Element of Omega holds b