let F be Field; :: thesis: for a being Element of F
for n being non zero Nat holds Roots ((X- a) `^ n) = {a}
let a be Element of F; :: thesis: for n being non zero Nat holds Roots ((X- a) `^ n) = {a}
let n be non zero Nat; :: thesis: Roots ((X- a) `^ n) = {a}
defpred S<sub>1</sub>[ Nat] means Roots ((X- a) `^ $1) = {a};
(X- a) `^ 1 = X- a by POLYNOM5:16;
then IA: S₁[1] by RING_5:18;

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: ( Roots ((X- a) `^ k) = {a} & Roots (X- a) = {a} ) by RING_5:18;
(X- a) `^ (k + 1) = ((X- a) `^ k) *' (X- a) by POLYNOM5:19;
then Roots ((X- a) `^ (k + 1)) = (Roots ((X- a) `^ k)) \/ (Roots (X- a)) by UPROOTS:23;
hence S₁[k + 1] by H2; :: 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 Roots ((X- a) `^ n) = {a} by I; :: thesis: verum