let n be Nat; :: thesis: for k being Nat holds exp (n,k) = n |^ k
defpred S₁[ Nat] means exp (n,$1) = n |^ $1;
exp (n,0) = 1 by ORDINAL2:43;
then A1: S₁[ 0 ] by NEWTON:4;

A2: now :: thesis: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: S₁[k] ; :: thesis: S₁[k + 1]
reconsider n9 = n, nk = n |^ k as Element of NAT by ORDINAL1:def 12;
Segm (k + 1) = succ (Segm k) by NAT_1:38;
then exp (n,(k + 1)) = n *^ (exp (n,k)) by ORDINAL2:44
.= n9 * nk by A3, CARD_2:37 ;
hence S₁[k + 1] by NEWTON:6; :: thesis: verum

end;

thus for k being Nat holds S₁[k] from NAT_1:sch 2(A1, A2); :: thesis: verum