deffunc H₁( Nat) -> Element of COMPLEX = Sum (c (#) (seq_a^ ($1,1,0)));
consider h being Real_Sequence such that
A1: for x being Nat holds h . x = H₁(x) from SEQ_1:sch 1();
take h ; :: thesis: for x being Nat holds h . x = Sum (c (#) (seq_a^ (x,1,0)))
thus for x being Nat holds h . x = Sum (c (#) (seq_a^ (x,1,0))) by A1; :: thesis: verum