:: deftheorem defines nonConstantPolys FIELD_11:def 7 :
for F being Field
for g being bijective Function of (nonConstantPolys F),(card (nonConstantPolys F)) holds nonConstantPolys (g,F) = { (Poly ((g . p),p)) where p is non constant Element of the carrier of (Polynom-Ring F) : verum } ;