let A be non degenerated commutative Ring; :: thesis: for n being Nat holds (1. A) |^ n = 1. A
defpred S₁[ Nat] means (1. A) |^ $1 = 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;
then A3: S₁[ 0 ] ;
thus for n being Nat holds S₁[n] from NAT_1:sch 2(A3, A1); :: thesis: verum