deffunc H₁( Nat) -> set = 1 + (1 / (primenumber $1));
ex f being Real_Sequence st
for n being Nat holds f . n = H₁(n) from SEQ_1:sch 1();
hence ex b₁ being Real_Sequence st
for n being Nat holds b₁ . n = 1 + (1 / (primenumber n)) ; :: thesis: verum