formal power series

Stream: Is there code for X?

[Jireh Loreaux]

Do we know that if a a function is analytic at every point of an open ball, then it has a formal power series on that ball? For context, I'm working on proving Gelfand's formula for the spectral radius and this is an essential step in all the proofs I've seen (I've looked at several now).