theorem :: RING_4:31

for R being Ring holds Char (Polynom-Ring R) = Char R by RING_3:88;