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 holds f . z = Sum (z ExpSeq)
let z be Complex; :: thesis: f . z = Sum (z ExpSeq)
z in COMPLEX by XCMPLX_0:def 2;
hence f . z = Sum (z ExpSeq) by A1; :: thesis: verum