deffunc H₁( set ) -> set = [:(f . $1),{$1}:];
thus ex g being Function st
( dom g = dom f & ( for x being set st x in dom f holds
g . x = H₁(x) ) ) from FUNCT_1:sch 3(); :: thesis: verum