set S = Roots (E,(X^ ((p |^ n),(PrimeField F))));
set q = X^ ((p |^ n),(PrimeField F));
H: Roots (E,(X^ ((p |^ n),(PrimeField F)))) = { a where a is Element of E : a is_a_root_of X^ ((p |^ n),(PrimeField F)),E } by FIELD_4:def 4;
( (0. E) |^ (p |^ n) = 0. E & (1. E) |^ (p |^ n) = 1. E ) ;
then B: ( 0. E is_a_root_of X^ ((p |^ n),(PrimeField F)),E & 1. E is_a_root_of X^ ((p |^ n),(PrimeField F)),E ) by thXXe;

C: now :: thesis: for a, b being Element of E st a in Roots (E,(X^ ((p |^ n),(PrimeField F)))) & b in Roots (E,(X^ ((p |^ n),(PrimeField F)))) holds
( a + b in Roots (E,(X^ ((p |^ n),(PrimeField F)))) & a * b in Roots (E,(X^ ((p |^ n),(PrimeField F)))) & - a in Roots (E,(X^ ((p |^ n),(PrimeField F)))) )

let a, b be Element of E; :: thesis: ( a in Roots (E,(X^ ((p |^ n),(PrimeField F)))) & b in Roots (E,(X^ ((p |^ n),(PrimeField F)))) implies ( a + b in Roots (E,(X^ ((p |^ n),(PrimeField F)))) & a * b in Roots (E,(X^ ((p |^ n),(PrimeField F)))) & - a in Roots (E,(X^ ((p |^ n),(PrimeField F)))) ) )
assume D0: ( a in Roots (E,(X^ ((p |^ n),(PrimeField F)))) & b in Roots (E,(X^ ((p |^ n),(PrimeField F)))) ) ; :: thesis: ( a + b in Roots (E,(X^ ((p |^ n),(PrimeField F)))) & a * b in Roots (E,(X^ ((p |^ n),(PrimeField F)))) & - a in Roots (E,(X^ ((p |^ n),(PrimeField F)))) )
then consider a1 being Element of E such that
D1: ( a1 = a & a1 is_a_root_of X^ ((p |^ n),(PrimeField F)),E ) by H;
consider b1 being Element of E such that
D2: ( b1 = b & b1 is_a_root_of X^ ((p |^ n),(PrimeField F)),E ) by H, D0;
(a + b) |^ (p |^ n) = (a |^ (p |^ n)) + (b |^ (p |^ n)) by FIELD_15:41
.= a + (b |^ (p |^ n)) by D1, thXXe
.= a + b by D2, thXXe ;
then a + b is_a_root_of X^ ((p |^ n),(PrimeField F)),E by thXXe;
hence a + b in Roots (E,(X^ ((p |^ n),(PrimeField F)))) by H; :: thesis: ( a * b in Roots (E,(X^ ((p |^ n),(PrimeField F)))) & - a in Roots (E,(X^ ((p |^ n),(PrimeField F)))) )
(a * b) |^ (p |^ n) = (a |^ (p |^ n)) * (b |^ (p |^ n)) by BINOM:9
.= a * (b |^ (p |^ n)) by D1, thXXe
.= a * b by D2, thXXe ;
then a * b is_a_root_of X^ ((p |^ n),(PrimeField F)),E by thXXe;
hence a * b in Roots (E,(X^ ((p |^ n),(PrimeField F)))) by H; :: thesis: - a in Roots (E,(X^ ((p |^ n),(PrimeField F))))
0. E = (0. E) |^ (p |^ n)
.= (a + (- a)) |^ (p |^ n) by RLVECT_1:5
.= (a |^ (p |^ n)) + ((- a) |^ (p |^ n)) by FIELD_15:41
.= a + ((- a) |^ (p |^ n)) by D1, thXXe ;
then - a is_a_root_of X^ ((p |^ n),(PrimeField F)),E by thXXe, RLVECT_1:6;
hence - a in Roots (E,(X^ ((p |^ n),(PrimeField F)))) by H; :: thesis: verum

end;

now :: thesis: for a being non zero Element of E st a in Roots (E,(X^ ((p |^ n),(PrimeField F)))) holds
a " in Roots (E,(X^ ((p |^ n),(PrimeField F))))

let a be non zero Element of E; :: thesis: ( a in Roots (E,(X^ ((p |^ n),(PrimeField F)))) implies a " in Roots (E,(X^ ((p |^ n),(PrimeField F)))) )
assume a in Roots (E,(X^ ((p |^ n),(PrimeField F)))) ; :: thesis: a " in Roots (E,(X^ ((p |^ n),(PrimeField F))))
then consider a1 being Element of E such that
D: ( a1 = a & a1 is_a_root_of X^ ((p |^ n),(PrimeField F)),E ) by H;
(a ") |^ (p |^ n) = (a |^ (p |^ n)) " by F16
.= a " by D, thXXe ;
then a " is_a_root_of X^ ((p |^ n),(PrimeField F)),E by thXXe;
hence a " in Roots (E,(X^ ((p |^ n),(PrimeField F)))) by H; :: thesis: verum

end;

hence Roots (E,(X^ ((p |^ n),(PrimeField F)))) is inducing_subfield by B, H, C; :: thesis: verum