thus ex s being Complex_Sequence st
for n being Nat holds s . n = H₂(n) from COMSEQ_1:sch 1(); :: thesis: verum