deffunc H_{1}( object ) -> set = {$1};

for x being Element of R holds f . x = H_{1}(x)
from FUNCT_2:sch 8(A1); :: thesis: verum

A1: now :: thesis: for x being Element of R holds H_{1}(x) in bool R

thus
ex f being Function of R,(bool R) st let x be Element of R; :: thesis: H_{1}(x) in bool R

{x} c= R ;

hence H_{1}(x) in bool R
; :: thesis: verum

end;{x} c= R ;

hence H

for x being Element of R holds f . x = H