let k, l be Nat; :: 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) ) & k = Sum d9 ) & 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) ) & l = Sum d9 ) implies k = l )
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: ( for d9 being XFinSequence of NAT holds
( not dom d9 = dom d or ex i being Nat st
( i in dom d9 & not d9 . i = (d . i) * (b |^ i) ) or not l = Sum d9 ) or k = l )
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: k = l

now :: thesis: for i being Nat st i in dom d holds
k9 . i = l9 . i

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

end;

hence k = l by A4, A6, A7, A9, AFINSQ_1:8; :: thesis: verum