theorem :: FIELD_16:54

for p being Prime
for n being non zero Nat
for F being b₁ -characteristic Field
for E being SplittingField of X^ ((p |^ n),(PrimeField F)) holds E == InducedSubfield (Roots (E,(X^ ((p |^ n),(PrimeField F)))))