let k, l be Nat; :: thesis:
given k9 being XFinSequence of NAT such that A4: dom k9 = dom d and
A5: for i being Nat st i in dom k9 holds
k9 . i = (d . i) * (b |^ i) and
A6: k = Sum k9 ; :: thesis:
given l9 being XFinSequence of NAT such that A7: dom l9 = dom d and
A8: for i being Nat st i in dom l9 holds
l9 . i = (d . i) * (b |^ i) and
A9: l = Sum l9 ; :: thesis:

let i be Nat; :: thesis:
assume A10: i in dom d ; :: thesis:
hence k9 . i = (d . i) * (b |^ i) by A4, A5
.= l9 . i by A7, A8, A10 ;
:: thesis:

end;