It instantly stroke a chord with our debate here. "0.999... = 1" is an unprovable axiom in my view. It can however be demonstrated as being consistent within R.
Your view is correct. 0.999... is by definition (or: unprovable axiom) equal to lim(n->oo)sum(k=1...N) 9/10^(-k).
I'd be interested in such a demonstration, however. What did you have in mind?