let n be non zero Nat; :: thesis: for v being CRoot of n, 0 holds v = 0
let v be CRoot of n, 0 ; :: thesis: v = 0
defpred S₁[ Nat] means v |^ $1 = 0 ;

A1: now :: thesis: for k being non zero Nat st k <> 1 & S₁[k] holds
ex t being non zero Nat st
( t < k & S₁[t] )

let k be non zero Nat; :: thesis: ( k <> 1 & S₁[k] implies ex t being non zero Nat st
( t < k & S₁[t] ) )
assume that
A2: k <> 1 and
A3: S₁[k] ; :: thesis: ex t being non zero Nat st
( t < k & S₁[t] )
consider t being Nat such that
A4: k = t + 1 by NAT_1:6;
t <> 0 by A2, A4;
then reconsider t = t as non zero Nat ;
take t = t; :: thesis: ( t < k & S₁[t] )
thus t < k by A4, NAT_1:13; :: thesis: S₁[t]
v |^ k = (v |^ t) * v by A4, NEWTON:6;
then ( v |^ t = 0 or v = 0 ) by A3;
hence S₁[t] by Lm2; :: thesis: verum

end;

A5: ex n being non zero Nat st S₁[n]

proof

take n ; :: thesis: S₁[n]
thus S₁[n] by COMPTRIG:def 2; :: thesis: verum

end;

S₁[1] from COMPTRIG:sch 1(A5, A1);
hence v = 0 ; :: thesis: verum