Stack Exchange network consists of 183 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.
Belated update: I only ended up needing the special case of this where the prosystem is Mittag-Leffler (lemma 5.14 of arXiv:1603.09743v3). As mentioned in that paper, Paul Garrett later showed me a (clever and tricky) argument for its truth in general.
@Jason Starr: thanks for your comments. I will make sure to think about your specific example. I think a counterexample $Y$ can't be smooth, though: see the edit above.
Great; thanks much. Is there any way you could tell me a bit more about how the choices of $\alpha_i$ are made? I don't think I see yet how their existence follows from the assumption that the system is not pro-trivial.