deffunc H₂( Element of REAL ) -> Element of REAL = Sum ($1 rExpSeq );
consider f being Function of REAL ,REAL such that
A1: for d being Element of REAL holds f . d = H₂(d) from FUNCT_2:sch 4();
take f ; :: thesis: for d being real number holds f . d = Sum (d rExpSeq )
let d be real number ; :: thesis: f . d = Sum (d rExpSeq )
A2: d in REAL by XREAL_0:def 1;
thus f . d = Sum (d rExpSeq ) by A1, A2; :: thesis: verum