let n be Nat; :: thesis: ex k being Nat st 3 |^ ((2 * n) + 1) = (4 * k) + 3
defpred S₁[ Nat] means ex k being Nat st 3 |^ ((2 * $1) + 1) = (4 * k) + 3;
3 |^ ((2 * 0) + 1) = (4 * 0) + 3 ;
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) + 3 = 3 |^ ((2 * x) + 1) ; :: thesis: S₁[x + 1]
take (9 * k) + 6 ; :: thesis: 3 |^ ((2 * (x + 1)) + 1) = (4 * ((9 * k) + 6)) + 3
3 |^ ((2 * (x + 1)) + 1) = 3 |^ (((2 * x) + 1) + 2)
.= (3 |^ ((2 * x) + 1)) * (3 |^ 2) by NEWTON:8 ;
hence 3 |^ ((2 * (x + 1)) + 1) = (4 * ((9 * k) + 6)) + 3 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) + 1) = (4 * k) + 3 ; :: thesis: verum