let F be finite Field; :: thesis: Roots (X^ ((Char F),F)) = the carrier of (PrimeField F)
consider p being Prime, n being non zero Nat such that
A: ( Char F = p & order F = p |^ n ) by finex2;
thus Roots (X^ ((Char F),F)) = the carrier of (PrimeField F) by A, FF; :: thesis: verum