theorem Th76: :: RING_3:77

for n being positive Nat holds Char (Z/ n) = n