let n be Nat; :: thesis: ex k being Nat st 3 |^ (2 * n) = (4 * k) + 1
defpred S₁[ Nat] means ex k being Nat st 3 |^ (2 * $1) = (4 * k) + 1;
3 |^ (2 * 0) = (4 * 0) + 1 by NEWTON:4;
then A1: S₁[ 0 ] ;
A2: for x being Nat st S₁[x] holds
S₁[x + 1]

proof

let x be Nat; :: thesis: ( S₁[x] implies S₁[x + 1] )
given k being Nat such that A3: (4 * k) + 1 = 3 |^ (2 * x) ; :: thesis: S₁[x + 1]
take (9 * k) + 2 ; :: thesis: 3 |^ (2 * (x + 1)) = (4 * ((9 * k) + 2)) + 1
3 |^ (2 * (x + 1)) = 3 |^ ((2 * x) + 2)
.= (3 |^ (2 * x)) * (3 |^ 2) by NEWTON:8 ;
hence 3 |^ (2 * (x + 1)) = (4 * ((9 * k) + 2)) + 1 by A3, Lm2; :: thesis: verum

end;

for x being Nat holds S₁[x] from NAT_1:sch 2(A1, A2);
hence ex k being Nat st 3 |^ (2 * n) = (4 * k) + 1 ; :: thesis: verum