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 )
A2: z in COMPLEX by XCMPLX_0:def 2;
thus f . z = Sum (z ExpSeq ) by A1, A2; :: thesis: verum