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