per cases ( n = 0 or n <> 0 ) ;

suppose n = 0 ; :: thesis: ex b₁ being comRing st b₁ is n -characteristic

hence ex b₁ being comRing st b₁ is n -characteristic by Th75; :: thesis: verum

end;

suppose n <> 0 ; :: thesis: ex b₁ being comRing st b₁ is n -characteristic

then reconsider k = n as positive Nat ;
Char (Z/ k) = k by Th76;
hence ex b₁ being comRing st b₁ is n -characteristic ; :: thesis: verum

end;

end;