deffunc H₁( Element of REAL ) -> Element of REAL = Im (Sum (($1 * <i> ) ExpSeq ));
consider f being Function of REAL ,REAL such that
A1: for x being Element of REAL holds f . x = H₁(x) from FUNCT_2:sch 4();
take f ; :: thesis: for d being Element of REAL holds f . d = Im (Sum ((d * <i> ) ExpSeq ))
thus for d being Element of REAL holds f . d = Im (Sum ((d * <i> ) ExpSeq )) by A1; :: thesis: verum