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 S1[ Nat] means ( n <> 0 & $1 <> 0 implies n |^ $1 = n * (n |^ ($1 -' 1)) );
A2: for m being Nat st S1[m] holds
S1[m + 1]
proof
let m be Nat; :: thesis: ( S1[m] implies S1[m + 1] )
assume S1[m] ; :: thesis: S1[m + 1]
now :: thesis: S1[m + 1]
per cases ( m = 0 or m <> 0 ) ;
suppose A3: m = 0 ; :: thesis: S1[m + 1]
n * (n |^ ((0 + 1) -' 1)) = n * (n |^ 0) by XREAL_1:232
.= n * 1 by NEWTON:4 ;
hence S1[m + 1] by A3; :: thesis: verum
end;
suppose A4: m <> 0 ; :: thesis: S1[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 S1[m + 1] ; :: thesis: verum
end;
end;
end;
hence S1[m + 1] ; :: thesis: verum
end;
A5: S1[ 0 ] ;
for m being Nat holds S1[m] from NAT_1:sch 2(A5, A2);
 hence n |^ p = n * (n |^ (p -' 1)) by A1; :: thesis: verum