deffunc H₁( Element of NAT ) -> Element of the carrier of Y = (H . $1) . x;
thus ex f being Function of NAT, the carrier of Y st
for n being Element of NAT holds f . n = H₁(n) from FUNCT_2:sch 4(); :: thesis: verum