set a = 1. A;
for n being Nat holds (1. A) |^ n = 1. A

proof

defpred S₁[ Nat] means (1. A) |^ A = 1. A;

A1: now :: thesis: for n being Nat st S₁[n] holds
S₁[n + 1]

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A2: S₁[n] ; :: thesis: S₁[n + 1]
(1. A) |^ (n + 1) = ((1. A) |^ n) * ((1. A) |^ 1) by BINOM:10
.= 1. A by BINOM:8, A2 ;
hence S₁[n + 1] ; :: thesis: verum

end;

(1. A) |^ 0 = 1_ A by BINOM:8
.= 1. A ;
then A3: S₁[ 0 ] ;
thus for n being Nat holds S₁[n] from NAT_1:sch 2(A3, A1); :: thesis: verum

end;

hence not 1. A is nilpotent ; :: thesis: verum