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

( 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

hence
k = l
by A4, A6, A7, A9, AFINSQ_1:8; :: thesis: verumk9 . 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;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