src/HOL/Algebra/UnivPoly.thy

   assumes R: "p \<in> carrier P"
   shows "\<zero>\<^bsub>P\<^esub> \<oplus>\<^bsub>P\<^esub> p = p" by (rule up_eqI, simp_all add: R)
 
 lemma UP_l_neg_ex:
   assumes R: "p \<in> carrier P"
-  shows "EX q : carrier P. q \<oplus>\<^bsub>P\<^esub> p = \<zero>\<^bsub>P\<^esub>"
+  shows "\<exists>q \<in> carrier P. q \<oplus>\<^bsub>P\<^esub> p = \<zero>\<^bsub>P\<^esub>"
 proof -
   let ?q = "\<lambda>i. \<ominus> (p i)"
   from R have closed: "?q \<in> carrier P"
     by (simp add: UP_def P_def up_a_inv_closed)
   from R have coeff: "!!n. coeff P ?q n = \<ominus> (coeff P p n)"