deffunc H₁( Element of NAT ) -> Element of REAL = (H . $1) . x;
thus ex f being Real_Sequence st
for n being Element of NAT holds f . n = H₁(n) from SEQ_1:sch 1(); :: thesis: verum