deffunc H₁( Real) -> Element of REAL = Re (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 Real holds f . d = Re (Sum ((d * <i>) ExpSeq))
let d be Real; :: thesis: f . d = Re (Sum ((d * <i>) ExpSeq))
reconsider d = d as Element of REAL by XREAL_0:def 1;
f . d = H₁(d) by A1;
hence f . d = Re (Sum ((d * <i>) ExpSeq)) ; :: thesis: verum