deffunc H₁( Real) -> set = 1 / ($1 + r);
ex seq being Complex_Sequence st
for n being Nat holds seq . n = H₁(n) from COMSEQ_1:sch 1();
hence ex b₁ being Complex_Sequence st
for n being Nat holds b₁ . n = 1 / (n + r) ; :: thesis: verum