deffunc H_{1}( 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_{1}(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

consider h being Real_Sequence such that

A1: for x being Nat holds h . x = H

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