Embedded Picard–Vessiot extensions

We prove that if T is a theory of large, bounded, fields of characteristic 0 with almost quantifier elimination, and TD is the model companion of T∪{“∂ is a derivation”}, then for any model (𝒰,∂) of TD, differential subfield K of 𝒰 such that CK⊧T, and linear differential equation ∂Y = AY over K, there is a Picard-Vessiot extension L of K for the equation with K≤L≤𝒰, i.e. L can be embedded in 𝒰 over K, as a differential field. Moreover such L is …