theorem Fpp1: :: FIELD_15:93

for p being Prime
for F being finite b₁ -characteristic Field
for a being Element of F ex b being Element of F st b |^ p = a