deffunc H₁( Nat) -> Element of REAL = In ((Sum ((- (s . $1)) rExpSeq)),REAL);
consider f being Real_Sequence such that
A1: for d being Element of NAT holds f . d = H₁(d) from FUNCT_2:sch 4();
take f ; :: thesis: for d being Nat holds f . d = Sum ((- (s . d)) rExpSeq)
let d be Nat; :: thesis: f . d = Sum ((- (s . d)) rExpSeq)
d in NAT by ORDINAL1:def 12;
then f . d = H₁(d) by A1;
hence f . d = Sum ((- (s . d)) rExpSeq) ; :: thesis: verum