theorem split: :: FIELD_16:55

for p being Prime
for n being non zero Nat
for F being Field st card F = p |^ n holds
F is SplittingField of X^ ((p |^ n),(PrimeField F))