let p be Prime; :: thesis: for n being non zero Nat
for F being p -characteristic Field st card F = p |^ n holds
for a being Element of F holds eval ((X^ ((p |^ n),F)),a) = 0. F
let n be non zero Nat; :: thesis: for F being p -characteristic Field st card F = p |^ n holds
for a being Element of F holds eval ((X^ ((p |^ n),F)),a) = 0. F
let F be p -characteristic Field; :: thesis: ( card F = p |^ n implies for a being Element of F holds eval ((X^ ((p |^ n),F)),a) = 0. F )
assume A: card F = p |^ n ; :: thesis: for a being Element of F holds eval ((X^ ((p |^ n),F)),a) = 0. F
let a be Element of F; :: thesis: eval ((X^ ((p |^ n),F)),a) = 0. F
a |^ (p |^ n) = a by A, thX0;
then a is_a_root_of X^ ((p |^ n),F) by thXX;
hence eval ((X^ ((p |^ n),F)),a) = 0. F ; :: thesis: verum