let n be Nat; :: thesis: exp (2,n) = 2 |^ n
defpred S₁[ Nat] means exp (2,$1) = 2 |^ $1;
IA: S₁[ 0 ]

proof

thus exp (2,0) = 1 by CARD_2:25
.= 2 |^ 0 by NEWTON:4 ; :: thesis: verum

end;

IS: 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 IV: S₁[k] ; :: thesis: S₁[k + 1]
exp (2,(k + 1)) = exp (2,(k +` 1)) by th0a
.= (exp (2,k)) *` (exp (2,1)) by CARD_2:28
.= (2 |^ k) *` 2 by IV, CARD_2:27
.= (2 |^ k) * 2 by th0a
.= 2 |^ (k + 1) by NEWTON:6 ;
hence S₁[k + 1] ; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(IA, IS);
hence exp (2,n) = 2 |^ n ; :: thesis: verum