let F be Field; :: thesis: for E being FieldExtension of F
for a being Element of E
for n being Nat holds a |^ n in the carrier of (FAdj (F,{a}))
let E be FieldExtension of F; :: thesis: for a being Element of E
for n being Nat holds a |^ n in the carrier of (FAdj (F,{a}))
let a be Element of E; :: thesis: for n being Nat holds a |^ n in the carrier of (FAdj (F,{a}))
let n be Nat; :: thesis: a |^ n in the carrier of (FAdj (F,{a}))
H: {a} is Subset of (FAdj (F,{a})) by FIELD_6:35;
defpred S₁[ Nat] means a |^ $1 in the carrier of (FAdj (F,{a}));
a |^ 0 = 1_ E by BINOM:8
.= 1. (FAdj (F,{a})) by FIELD_6:def 6 ;
then IA: S₁[ 0 ] ;

IS: now :: thesis: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume IV: S₁[k] ; :: thesis: S₁[k + 1]
I: FAdj (F,{a}) is Subring of E by FIELD_5:12;
a in {a} by TARSKI:def 1;
then reconsider b1 = a, b2 = a |^ k as Element of (FAdj (F,{a})) by IV, H;
a |^ (k + 1) = (a |^ k) * (a |^ 1) by BINOM:10
.= (a |^ k) * a by BINOM:8
.= b2 * b1 by I, FIELD_6:16 ;
hence S₁[k + 1] ; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(IA, IS);
hence a |^ n in the carrier of (FAdj (F,{a})) ; :: thesis: verum