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