let p be Prime; :: thesis: for n being non zero Nat
for F being p -characteristic Field
for E being FieldExtension of F st card E = p |^ n holds
for a being Element of E holds Ext_eval ((X^ ((p |^ n),F)),a) = 0. E
let n be non zero Nat; :: thesis: for F being p -characteristic Field
for E being FieldExtension of F st card E = p |^ n holds
for a being Element of E holds Ext_eval ((X^ ((p |^ n),F)),a) = 0. E
let F be p -characteristic Field; :: thesis: for E being FieldExtension of F st card E = p |^ n holds
for a being Element of E holds Ext_eval ((X^ ((p |^ n),F)),a) = 0. E
let E be FieldExtension of F; :: thesis: ( card E = p |^ n implies for a being Element of E holds Ext_eval ((X^ ((p |^ n),F)),a) = 0. E )
assume A: card E = p |^ n ; :: thesis: for a being Element of E holds Ext_eval ((X^ ((p |^ n),F)),a) = 0. E
let a be Element of E; :: thesis: Ext_eval ((X^ ((p |^ n),F)),a) = 0. E
a |^ (p |^ n) = a by A, thX0;
hence Ext_eval ((X^ ((p |^ n),F)),a) = 0. E by thXXe, FIELD_4:def 2; :: thesis: verum