per cases ( n = 0 or n <> 0 ) ;
suppose n = 0 ; :: thesis: ex b1 being comRing st b1 is n -characteristic
hence ex b1 being comRing st b1 is n -characteristic by Th75; :: thesis: verum
end;
suppose n <> 0 ; :: thesis: ex b1 being comRing st b1 is n -characteristic
then reconsider k = n as positive Nat ;
Char (Z/ k) = k by Th76;
hence ex b1 being comRing st b1 is n -characteristic ; :: thesis: verum
end;
end;