let F be Field; :: thesis: for a being Element of F
for n being Nat holds deg ((X- a) `^ n) = n
let a be Element of F; :: thesis: for n being Nat holds deg ((X- a) `^ n) = n
let n be Nat; :: thesis: deg ((X- a) `^ n) = n
defpred S<sub>1</sub>[ Nat] means deg ((X- a) `^ $1) = $1;
H: (X- a) `^ 0 = 1_. F by POLYNOM5:15;
IA: S₁[ 0 ] by H, RATFUNC1:def 2;

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 H2: ( deg ((X- a) `^ k) = k & deg (X- a) = 1 ) by FIELD_5:def 1;
( (X- a) `^ (k + 1) = ((X- a) `^ k) *' (X- a) & X- a <> 0_. F & (X- a) `^ k <> 0_. F ) by POLYNOM5:19;
hence S₁[k + 1] by H2, HURWITZ:23; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(IA, IS);
hence deg ((X- a) `^ n) = n ; :: thesis: verum