let n, p be Nat; :: thesis: ( n <> 0 & p <> 0 implies n |^ p = n * (n |^ (p -' 1)) )
assume A1: ( n <> 0 & p <> 0 ) ; :: thesis: n |^ p = n * (n |^ (p -' 1))
defpred S₁[ Nat] means ( n <> 0 & $1 <> 0 implies n |^ $1 = n * (n |^ ($1 -' 1)) );
A2: for m being Nat st S₁[m] holds
S₁[m + 1]

proof

let m be Nat; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume S₁[m] ; :: thesis: S₁[m + 1]

now :: thesis: S₁[m + 1]

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

suppose A3: m = 0 ; :: thesis: S₁[m + 1]

n * (n |^ ((0 + 1) -' 1)) = n * (n |^ 0) by XREAL_1:232
.= n * 1 by NEWTON:4 ;
hence S₁[m + 1] by A3; :: thesis: verum

end;

suppose A4: m <> 0 ; :: thesis: S₁[m + 1]

n |^ (m + 1) = (n |^ m) * n by NEWTON:6
.= (n |^ ((m -' 1) + 1)) * n by A4, NAT_1:14, XREAL_1:235
.= n * (n |^ ((m + 1) -' 1)) by A4, Lm4 ;
hence S₁[m + 1] ; :: thesis: verum

end;

end;

end;

hence S₁[m + 1] ; :: thesis: verum

end;

A5: S₁[ 0 ] ;
for m being Nat holds S₁[m] from NAT_1:sch 2(A5, A2);
hence n |^ p = n * (n |^ (p -' 1)) by A1; :: thesis: verum