theorem Th12: :: HILB10_1:9

for n being Nat
for a being non trivial Nat ex Fy, Fx being FinSequence of NAT st
( Sum Fy = Py (a,n) & len Fy = [\((n + 1) / 2)/] & ( for i being Nat st 1 <= i & i <= (n + 1) / 2 holds
Fy . i = ((n choose ((2 * i) -' 1)) * (a |^ ((n + 1) -' (2 * i)))) * (((a ^2) -' 1) |^ (i -' 1)) ) & (a |^ n) + (Sum Fx) = Px (a,n) & len Fx = [\(n / 2)/] & ( for i being Nat st 1 <= i & i <= n / 2 holds
Fx . i = ((n choose (2 * i)) * (a |^ (n -' (2 * i)))) * (((a ^2) -' 1) |^ i) ) )