let n be prime Nat; :: thesis: n divides (2 |^ n) - 2
reconsider h = Newton_Coeff n as FinSequence of NAT by Th1;
reconsider f = ((Newton_Coeff n) | n) /^ 1 as FinSequence of NAT by Th1;
A2: for k being Nat st k in dom f holds
n divides f . k by Th39;
Sum h = (Sum f) + 2 by Th35;
then 2 |^ n = (Sum f) + 2 by NEWTON:32;
hence n divides (2 |^ n) - 2 by A2, INT_4:36; :: thesis: verum