Common algebraically closed D-algebra receiving two field extensions

Let $D$ be a commutative ring which is a domain, and let $E_1$ and $E_2$ be fields equipped with $D$-algebra structures whose structure maps $\mathrm{algebraMap}\,D\,E_1$ and $\mathrm{algebraMap}\,D\,E_2$ are injective (hypotheses $h_1$, $h_2$); all three types are taken in the lowest universe. The conclusion asserts the existence of a type $\Omega'$ together with a field structure on it, a proof that $\Omega'$ is algebraically closed, and a $D$-algebra structure on $\Omega'$, such that the type of $D$-algebra homomorphisms $E_1 \to_D \Omega'$ is nonempty and likewise the type of $D$-algebra homomorphisms $E_2 \to_D \Omega'$ is nonempty. Thus both $E_1$ and $E_2$ embed into one algebraically closed field in a way compatible with their $D$-algebra structures; the field structure, the algebraic closedness and the $D$-algebra structure on $\Omega'$ are all part of the existential data, and the two homomorphisms are produced only as nonemptiness assertions, not as explicitly named maps.

This is the standard statement that two field extensions of a domain with injective structure maps can be amalgamated inside a single algebraically closed $D$-algebra. It serves as an infrastructure step used when comparing the residue field of a place, or a field of definition, with a fixed algebraically closed field; it is invoked in the computations of $j$-invariants of Tate-type points on modular curves and in the Drinfeld-type global argument.