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:60;
then A0: S₁[ 0 ] by NEWTON:9;

A1: now

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A2: S₁[k] ; :: thesis: S₁[k + 1]
reconsider n9 = n, nk = n |^ k as Element of NAT by ORDINAL1:def 13;
k + 1 = succ k by NAT_1:39;
then exp n,(k + 1) = n *^ (exp n,k) by ORDINAL2:61
.= n9 * nk by A2, CARD_2:50 ;
hence S₁[k + 1] by NEWTON:11; :: thesis: verum

end;

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