ex f being Complex_Sequence st
for n being Nat holds f . n = H₁(n) from COMSEQ_1:sch 1();
hence ex b₁ being Complex_Sequence st
for n being Nat holds b₁ . n = (Polynom (a,b,n)) / (Polynom (c,d,n)) ; :: thesis: verum