let R be domRing; :: thesis: R is reduced

now :: thesis: R is reduced

assume not R is reduced ; :: thesis: contradiction
then consider a being nilpotent Element of R such that
A: a <> 0. R ;
defpred S₁[ Nat] means ( a |^ c₁ = 0. R & c₁ <> 0 );
ex k being non zero Nat st a |^ k = 0. R by TOPZARI1:def 2;
then B: ex k being Nat st S₁[k] ;
consider k being Nat such that
C: ( S₁[k] & ( for n being Nat st S₁[n] holds
k <= n ) ) from NAT_1:sch 5(B);
reconsider k1 = k - 1 as Nat by C;
E: k1 + 0 < k1 + 1 by XREAL_1:39;
k = 1 + k1 ;
then F: 0. R = (a |^ 1) * (a |^ k1) by C, BINOM:10
.= a * (a |^ k1) by BINOM:8 ;

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

suppose k1 = 0 ; :: thesis: contradiction

then a |^ k1 = 1_ R by BINOM:8;
hence contradiction by A, F; :: thesis: verum

end;

suppose k1 <> 0 ; :: thesis: contradiction

then a |^ k1 <> 0. R by C, E;
hence contradiction by A, F, VECTSP_2:def 1; :: thesis: verum

end;

end;

end;

hence R is reduced ; :: thesis: verum