set S = Roots (X^ ((p |^ n),F));
set q = X^ ((p |^ n),F);
( (0. F) |^ (p |^ n) = 0. F & (1. F) |^ (p |^ n) = 1. F ) ;
then B: ( 0. F is_a_root_of X^ ((p |^ n),F) & 1. F is_a_root_of X^ ((p |^ n),F) ) by thXX;

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

let a, b be Element of F; :: thesis: ( a in Roots (X^ ((p |^ n),F)) & b in Roots (X^ ((p |^ n),F)) implies ( a + b in Roots (X^ ((p |^ n),F)) & a * b in Roots (X^ ((p |^ n),F)) & - a in Roots (X^ ((p |^ n),F)) ) )
assume ( a in Roots (X^ ((p |^ n),F)) & b in Roots (X^ ((p |^ n),F)) ) ; :: thesis: ( a + b in Roots (X^ ((p |^ n),F)) & a * b in Roots (X^ ((p |^ n),F)) & - a in Roots (X^ ((p |^ n),F)) )
then D: ( a is_a_root_of X^ ((p |^ n),F) & b is_a_root_of X^ ((p |^ n),F) ) by POLYNOM5:def 10;
(a + b) |^ (p |^ n) = (a |^ (p |^ n)) + (b |^ (p |^ n)) by FIELD_15:41
.= a + (b |^ (p |^ n)) by D, thXX
.= a + b by D, thXX ;
then a + b is_a_root_of X^ ((p |^ n),F) by thXX;
hence a + b in Roots (X^ ((p |^ n),F)) by POLYNOM5:def 10; :: thesis: ( a * b in Roots (X^ ((p |^ n),F)) & - a in Roots (X^ ((p |^ n),F)) )
(a * b) |^ (p |^ n) = (a |^ (p |^ n)) * (b |^ (p |^ n)) by BINOM:9
.= a * (b |^ (p |^ n)) by D, thXX
.= a * b by D, thXX ;
then a * b is_a_root_of X^ ((p |^ n),F) by thXX;
hence a * b in Roots (X^ ((p |^ n),F)) by POLYNOM5:def 10; :: thesis: - a in Roots (X^ ((p |^ n),F))
0. F = (0. F) |^ (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 D, thXX ;
then - a is_a_root_of X^ ((p |^ n),F) by thXX, RLVECT_1:6;
hence - a in Roots (X^ ((p |^ n),F)) by POLYNOM5:def 10; :: thesis: verum

end;

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

let a be non zero Element of F; :: thesis: ( a in Roots (X^ ((p |^ n),F)) implies a " in Roots (X^ ((p |^ n),F)) )
assume a in Roots (X^ ((p |^ n),F)) ; :: thesis: a " in Roots (X^ ((p |^ n),F))
then D: a is_a_root_of X^ ((p |^ n),F) by POLYNOM5:def 10;
(a ") |^ (p |^ n) = (a |^ (p |^ n)) " by F16
.= a " by D, thXX ;
then a " is_a_root_of X^ ((p |^ n),F) by thXX;
hence a " in Roots (X^ ((p |^ n),F)) by POLYNOM5:def 10; :: thesis: verum

end;

hence Roots (X^ ((p |^ n),F)) is inducing_subfield by B, C, POLYNOM5:def 10; :: thesis: verum