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