for F being non almost_trivial Field
for x being non trivial Element of F
for P being Ring st P = ExField (x,<%(0. F),(1. F)%>) holds
<%(0. F),(1. F)%> in ([#] P) /\ ([#] (Polynom-Ring P))