I'm having trouble proving this in S5.

◊(∃x) Fx -> (∃x) ◊Fx
| ◊(∃x) Fx (assume)
| | ~ ◊(∃x) Fx (assume)
| | | ◊ ~ (∃x) ◊Fx (possibility)
| | | □ | ◊ ~ (∃x) ◊Fx (S5 necessity intro)
| | | □◊ ~ (∃x) ◊Fx (necessity)
| | | ~◊~◊~ (∃x) ◊Fx (def of □)
| | | ~◊□ (∃x) ◊Fx (def of □)
| | | □ | (∃x) ◊Fx (assume necessity)
| | | □ | | Fx (Existential instantiation)
| | | □ | | ◊Fx (possibility)
| | | □ | | □ | ◊Fx (S5 necessity intro)
| | | □ | | □ | (∃x) ◊Fx (Existential generalization)
| | | □ | | □(∃x) ◊Fx (necessity)
| | | □(∃x) ◊Fx (necessity)
| | | ◊□(∃x) ◊Fx (possibility)

???
Therefore
◊(∃x) Fx -> (∃x) ◊Fx

I'm not sure how to eliminiate ◊□ from the last step in order to get (∃x) ◊Fx