let F be Field; :: thesis: for a being Element of F
for n being non zero Nat holds (X- a) `^ n splits_in F
let a be Element of F; :: thesis: for n being non zero Nat holds (X- a) `^ n splits_in F
let n be non zero Nat; :: thesis: (X- a) `^ n splits_in F
defpred S<sub>1</sub>[ Nat] means (X- a) `^ $1 splits_in F;
H1: ( deg (X- a) = 1 & (X- a) `^ 1 = X- a ) by FIELD_5:def 1, POLYNOM5:16;
then IA: S₁[1] by FIELD_4:29;

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

let k be Nat; :: thesis: ( k >= 1 & S₁[k] implies S₁[k + 1] )
assume k >= 1 ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume S₁[k] ; :: thesis: S₁[k + 1]
then H2: ( (X- a) `^ k splits_in F & X- a splits_in F ) by H1, FIELD_4:29;
(X- a) `^ (k + 1) = ((X- a) `^ k) *' (X- a) by POLYNOM5:19;
hence S₁[k + 1] by H2, FIELD_8:12; :: thesis: verum

end;

I: for k being Nat st k >= 1 holds
S₁[k] from NAT_1:sch 8(IA, IS);
n >= 0 + 1 by INT_1:7;
hence (X- a) `^ n splits_in F by I; :: thesis: verum