theorem :: NUMPOLY1:32

for n being Nat
for s being non zero Nat
for x being non zero b₂ -gonal number st x = Polygon (s,n) holds
(((8 * s) - 16) * x) + ((s - 4) ^2) = (((2 * n) * (s - 2)) - (s - 4)) ^2 ;