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

proof

A2: 2 |^ 0 = 1 by NEWTON:9;
2 |^ (0 + 1) = 2 by NEWTON:10;
then 2 |^ (2 |^ (0 + 1)) = 2 to_power 2
.= 2 ^2 by POWER:53 ;
hence S₁[ 0 ] by A2, NEWTON:10; :: thesis: verum

end;

A3: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let x be Nat; :: thesis: ( S₁[x] implies S₁[x + 1] )
assume A4: (2 |^ (2 |^ x)) ^2 = 2 |^ (2 |^ (x + 1)) ; :: thesis: S₁[x + 1]
(2 |^ (2 |^ (x + 1))) ^2 = (2 |^ ((2 |^ x) * 2)) ^2 by NEWTON:11
.= ((2 |^ (2 |^ x)) |^ 2) ^2 by NEWTON:14
.= ((2 |^ (2 |^ x)) ^2 ) ^2 by Th24
.= (2 |^ (2 |^ (x + 1))) |^ 2 by A4, Th24
.= 2 |^ ((2 |^ (x + 1)) * 2) by NEWTON:14
.= 2 |^ (2 |^ ((x + 1) + 1)) by NEWTON:11 ;
hence S₁[x + 1] ; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A1, A3);
hence (2 |^ (2 |^ n)) ^2 = 2 |^ (2 |^ (n + 1)) ; :: thesis: verum