let a be Element of R; :: thesis: ( a is nilpotent implies not a is unital )
assume a is nilpotent ; :: thesis: not a is unital
then consider k being non zero Nat such that
A: a |^ k = 0. R by TOPZARI1:def 2;

now :: thesis: not a is unital

assume a is unital ; :: thesis: contradiction
then a divides 1. R ;
then consider b being Element of R such that
B: a * b = 1. R ;
1. R = (a * b) |^ k by B
.= (0. R) * (b |^ k) by A, BINOM:9 ;
hence contradiction ; :: thesis: verum

end;

hence not a is unital ; :: thesis: verum