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

now

let i be Element of NAT ; :: thesis: ( i in dom d implies k' . i = l' . i )
assume A10: i in dom d ; :: thesis: k' . i = l' . i
hence k' . i = (d . i) * (b |^ i) by A4, A5
.= l' . i by A7, A8, A10 ;
:: thesis: verum

end;

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