theorem :: RING_4:33

for n being non trivial Nat holds Char (Polynom-Ring (Z/ n)) <> 0 ;