let n be Nat; :: thesis: n ^2 divides ((n + 1) |^ n) - 1
set P = (n,1) In_Power n;
A1: (n + 1) |^ n = Sum ((n,1) In_Power n) by NEWTON:30;
set c = len ((n,1) In_Power n);
set F = Del (((n,1) In_Power n),(len ((n,1) In_Power n)));
A2: len ((n,1) In_Power n) = n + 1 by NEWTON:def 4;
then A3: ((n,1) In_Power n) . (len ((n,1) In_Power n)) = 1 |^ n by NEWTON:29;
1 <= len ((n,1) In_Power n) by A2, NAT_1:11;
then A4: len ((n,1) In_Power n) in dom ((n,1) In_Power n) by FINSEQ_3:25;
then A5: (Sum (Del (((n,1) In_Power n),(len ((n,1) In_Power n))))) + (((n,1) In_Power n) . (len ((n,1) In_Power n))) = Sum ((n,1) In_Power n) by WSIERP_1:20;
A6: (len (Del (((n,1) In_Power n),(len ((n,1) In_Power n))))) + 1 = len ((n,1) In_Power n) by A4, WSIERP_1:def 1;
for b being Nat st b in dom (Del (((n,1) In_Power n),(len ((n,1) In_Power n)))) holds
n ^2 divides (Del (((n,1) In_Power n),(len ((n,1) In_Power n)))) . b

proof

let b be Nat; :: thesis: ( b in dom (Del (((n,1) In_Power n),(len ((n,1) In_Power n)))) implies n ^2 divides (Del (((n,1) In_Power n),(len ((n,1) In_Power n)))) . b )
assume A7: b in dom (Del (((n,1) In_Power n),(len ((n,1) In_Power n)))) ; :: thesis: n ^2 divides (Del (((n,1) In_Power n),(len ((n,1) In_Power n)))) . b
then A8: b <= len (Del (((n,1) In_Power n),(len ((n,1) In_Power n)))) by FINSEQ_3:25;
A9: 1 <= b by A7, FINSEQ_3:25;
A10: n < n + 1 by XREAL_1:29;
then b < len ((n,1) In_Power n) by A2, A6, A8, XXREAL_0:2;
then A11: (Del (((n,1) In_Power n),(len ((n,1) In_Power n)))) . b = ((n,1) In_Power n) . b by FINSEQ_3:110;

per cases ( b < (len ((n,1) In_Power n)) - 1 or b = (len ((n,1) In_Power n)) - 1 ) by A6, A8, XXREAL_0:1;

suppose b < (len ((n,1) In_Power n)) - 1 ; :: thesis: n ^2 divides (Del (((n,1) In_Power n),(len ((n,1) In_Power n)))) . b

then b <= ((len ((n,1) In_Power n)) - 1) - 1 by INT_1:52;
then b <= (len ((n,1) In_Power n)) - 2 ;
then n |^ 2 divides ((n,1) In_Power n) . b by A9, Th41;
hence n ^2 divides (Del (((n,1) In_Power n),(len ((n,1) In_Power n)))) . b by A11, WSIERP_1:1; :: thesis: verum

end;

suppose A12: b = (len ((n,1) In_Power n)) - 1 ; :: thesis: n ^2 divides (Del (((n,1) In_Power n),(len ((n,1) In_Power n)))) . b

reconsider M = b - 1 as Element of NAT by A9, INT_1:5;
reconsider L = n - M as Element of NAT by A2, A12;
n in dom ((n,1) In_Power n) by A2, A9, A10, A12, FINSEQ_3:25;
then ((n,1) In_Power n) . b = ((n choose M) * (n |^ L)) * (1 |^ M) by A2, A12, NEWTON:def 4;
hence n ^2 divides (Del (((n,1) In_Power n),(len ((n,1) In_Power n)))) . b by A2, A9, A11, A12, NEWTON:24; :: thesis: verum

end;

end;

end;

hence n ^2 divides ((n + 1) |^ n) - 1 by A1, A3, A5, INT_4:36; :: thesis: verum