deffunc H₁( Nat) -> object = k to_power (seq . $1);
thus ex s being Real_Sequence st
for n being Nat holds s . n = H₁(n) from SEQ_1:sch 1(); :: thesis: verum