let F be Field; :: thesis: for p being Polynomial of F
for E being FieldExtension of F
for q being Polynomial of E
for n being Element of NAT st q = p holds
q `^ n = p `^ n
let p be Polynomial of F; :: thesis: for E being FieldExtension of F
for q being Polynomial of E
for n being Element of NAT st q = p holds
q `^ n = p `^ n
let E be FieldExtension of F; :: thesis: for q being Polynomial of E
for n being Element of NAT st q = p holds
q `^ n = p `^ n
let q be Polynomial of E; :: thesis: for n being Element of NAT st q = p holds
q `^ n = p `^ n
let n be Element of NAT ; :: thesis: ( q = p implies q `^ n = p `^ n )
assume AS: q = p ; :: thesis: q `^ n = p `^ n
defpred S₁[ Nat] means q `^ $1 = p `^ $1;
q `^ 0 = 1_. E by POLYNOM5:15
.= 1_. F by FIELD_4:14
.= p `^ 0 by POLYNOM5:15 ;
then A: S₁[ 0 ] ;

B: 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]
q `^ (k + 1) = (q `^ k) *' q by POLYNOM5:19
.= (p `^ k) *' p by AS, IV, FIELD_4:17
.= p `^ (k + 1) by POLYNOM5:19 ;
hence S₁[k + 1] ; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A, B);
hence q `^ n = p `^ n ; :: thesis: verum