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

A1: now :: thesis: for x being Element of R holds H₁(x) in bool R

let x be Element of R; :: thesis: H₁(x) in bool R
{x} c= R ;
hence H₁(x) in bool R ; :: thesis: verum

end;

thus ex f being Function of R,(bool R) st
for x being Element of R holds f . x = H₁(x) from FUNCT_2:sch 8(A1); :: thesis: verum