theorem Th14: :: FIELD_3:14

ex K being Field st ([#] K) /\ ([#] (Polynom-Ring K)) <> {}