deffunc H₁( Element of COMPLEX ) -> Element of COMPLEX = Sum ($1 ExpSeq );
consider f being Function of COMPLEX ,COMPLEX such that
A1: for x being Element of COMPLEX holds f . x = H₁(x) from FUNCT_2:sch 4();
take f ; :: thesis: for z being complex number holds f . z = Sum (z ExpSeq )
let z be complex number ; :: thesis: f . z = Sum (z ExpSeq )
z in COMPLEX by XCMPLX_0:def 2;
hence f . z = Sum (z ExpSeq ) by A1; :: thesis: verum