theorem :: FIELD_3:16

ex K being Field ex x being object st
( not x in rng (canHom K) & x in ([#] K) /\ ([#] (Polynom-Ring K)) )