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