thus ex G being Function of NAT,ExtREAL st
for n being Element of NAT holds G . n = H₁(n) from FUNCT_2:sch 4(); :: thesis: verum