let k, l be Nat; :: thesis: ( ex d' being XFinSequence of 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 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 such that A5: ( dom k' = dom d & ( for i being Nat st i in dom k' holds
k' . i = (d . i) * (b |^ i) ) & k = Sum k' ) ; :: thesis: ( for d' being XFinSequence of 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 such that A6: ( dom l' = dom d & ( for i being Nat st i in dom l' holds
l' . i = (d . i) * (b |^ i) ) & l = Sum l' ) ; :: thesis: k = l

now

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

end;

hence k = l by A5, A6, AFINSQ_1:10; :: thesis: verum