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: 2 |^ (2 |^ (0 + 1)) = 2 to_power 2
.= 2 ^2 by POWER:46 ;
A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

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

end;

2 |^ 0 = 1 by NEWTON:4;
then A4: S₁[ 0 ] by A1;
for k being Nat holds S₁[k] from NAT_1:sch 2(A4, A2);
hence (2 |^ (2 |^ n)) ^2 = 2 |^ (2 |^ (n + 1)) ; :: thesis: verum