deffunc H₁( Nat) -> Element of NAT = (d . $1) * (b |^ $1);
consider d9 being XFinSequence such that
A1: ( len d9 = len d & ( for i being Nat st i in len d holds
d9 . i = H₁(i) ) ) from AFINSQ_1:sch 2();
rng d9 c= NAT

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in rng d9 or a in NAT )
assume a in rng d9 ; :: thesis: a in NAT
then consider i being set such that
A2: i in dom d9 and
A3: d9 . i = a by FUNCT_1:def 3;
reconsider i = i as Element of NAT by A2;
a = H₁(i) by A1, A2, A3;
hence a in NAT ; :: thesis: verum

end;

then reconsider d9 = d9 as XFinSequence of NAT by RELAT_1:def 19;
take Sum d9 ; :: thesis: ex d9 being XFinSequence of NAT st
( dom d9 = dom d & ( for i being Nat st i in dom d9 holds
d9 . i = (d . i) * (b |^ i) ) & Sum d9 = Sum d9 )
thus ex d9 being XFinSequence of NAT st
( dom d9 = dom d & ( for i being Nat st i in dom d9 holds
d9 . i = (d . i) * (b |^ i) ) & Sum d9 = Sum d9 ) by A1; :: thesis: verum