let n be Nat; :: thesis: exp (2,n) = 2 |^ n

defpred S_{1}[ Nat] means exp (2,$1) = 2 |^ $1;

IA: S_{1}[ 0 ]
_{1}[k]
from NAT_1:sch 2(IA, IS);

hence exp (2,n) = 2 |^ n ; :: thesis: verum

defpred S

IA: S

IS: now :: thesis: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]

for k being Nat holds SS

let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume IV: S_{1}[k]
; :: thesis: S_{1}[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_{1}[k + 1]
; :: thesis: verum

end;assume IV: S

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

hence exp (2,n) = 2 |^ n ; :: thesis: verum