let F be Field; :: thesis: for E being FieldExtension of F
for a being Element of E
for n being Element of 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 Element of NAT holds a |^ n in the carrier of (FAdj (F,{a}))
let a be Element of E; :: thesis: for n being Element of NAT holds a |^ n in the carrier of (FAdj (F,{a}))
let n be Element of NAT ; :: thesis: a |^ n in the carrier of (FAdj (F,{a}))
defpred S₁[ Nat] means a |^ $1 in the carrier of (FAdj (F,{a}));
set K = FAdj (F,{a});
H: {a} is Subset of (FAdj (F,{a})) by FAt;
a in {a} by TARSKI:def 1;
then reconsider a1 = a as Element of (FAdj (F,{a})) by H;
a |^ 0 = 1_ E by BINOM:8
.= 1. (FAdj (F,{a})) by dFA ;
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 S₁[k] ; :: thesis: S₁[k + 1]
then reconsider ak = a |^ k as Element of (FAdj (F,{a})) ;
carrierFA {a} = the carrier of (FAdj (F,{a})) by dFA;
then I: [ak,a1] in [:(carrierFA {a}),(carrierFA {a}):] by ZFMISC_1:def 2;
a |^ (k + 1) = (a |^ k) * (a |^ 1) by BINOM:10
.= the multF of E . (ak,a1) by BINOM:8
.= ( the multF of E || (carrierFA {a})) . (ak,a1) by I, FUNCT_1:49
.= ak * a1 by dFA ;
hence S₁[k + 1] ; :: thesis: verum

end;

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