deffunc H_{1}( Nat) -> set = (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_{1}(i) ) )
from AFINSQ_1:sch 2();

rng d9 c= NAT

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

consider d9 being XFinSequence such that

A1: ( len d9 = len d & ( for i being Nat st i in len d holds

d9 . i = H

rng d9 c= NAT

proof

then reconsider d9 = d9 as XFinSequence of NAT by RELAT_1:def 19;
let a be object ; :: 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 object 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_{1}(i)
by A1, A2, A3;

hence a in NAT by ORDINAL1:def 12; :: thesis: verum

end;assume a in rng d9 ; :: thesis: a in NAT

then consider i being object 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

hence a in NAT by ORDINAL1:def 12; :: thesis: verum

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