deffunc H₁( Nat) -> set = 1 / (($1 ^2) - (1 / 4));
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 / ((n ^2) - (1 / 4)) ; :: thesis: verum