let n be even Nat; :: thesis: ( n divides (2 |^ n) + 2 implies ex k being non zero odd Nat st (2 |^ n) + 2 = n * k )
assume A1: n divides (2 |^ n) + 2 ; :: thesis: ex k being non zero odd Nat st (2 |^ n) + 2 = n * k
then consider k being Nat such that
A2: (2 |^ n) + 2 = n * k by NAT_D:def 3;
reconsider n = n as non zero Nat by A1;

now :: thesis: not k is even

assume k is even ; :: thesis: contradiction
then consider a being Nat such that
A3: k = 2 * a ;
A4: (2 |^ n) + 2 = 2 * (a * n) by A2, A3;
(2 |^ ((n - 1) + 1)) + 2 = (2 * (2 |^ (n - 1))) + 2 by NEWTON:6
.= 2 * ((2 |^ (n - 1)) + 1) ;
hence contradiction by A4, XCMPLX_1:5; :: thesis: verum

end;

then reconsider k = k as non zero odd Nat ;
take k ; :: thesis: (2 |^ n) + 2 = n * k
thus (2 |^ n) + 2 = n * k by A2; :: thesis: verum