deffunc H₁( Element of omega ) -> Element of VAR = x. (card $1);
thus ex f being Function of omega,VAR st
for x being Element of omega holds f . x = H₁(x) from FUNCT_2:sch 4(); :: thesis: verum