theorem thX1: :: FIELD_16:35

for p being Prime
for n being non zero Nat
for F being b₁ -characteristic Field st card F = p |^ n holds
for a being Element of F holds eval ((X^ ((p |^ n),F)),a) = 0. F