deffunc H₁( 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₁(d) from FUNCT_2:sch 4();
hence ex b₁ being Function of Omega,REAL st
for w being Element of Omega holds b₁ . w = (Change_Element_to_Func (F,Borel_Sets,k)) . w ; :: thesis: verum