deffunc H₁( real number ) -> Element of REAL = 1 / ($1 + r);
ex seq being Complex_Sequence st
for n being Element of NAT holds seq . n = H₁(n) from COMSEQ_1:sch 1();
hence ex b₁ being Complex_Sequence st
for n being Element of NAT holds b₁ . n = 1 / (n + r) ; :: thesis: verum