theorem thX3: :: FIELD_16:40

for p being Prime
for n being non zero Nat
for F being b₁ -characteristic Field holds (Deriv F) . (X^ ((p |^ n),F)) = - (1_. F)