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 ;
assume A1: v <> 0 ; :: thesis: contradiction

A2: 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
A3: k <> 1 and
A4: S₁[k] ; :: thesis: ex t being non zero Nat st
( t < k & S₁[t] )
consider t being Nat such that
A5: k = t + 1 by NAT_1:6;
reconsider t = t as non zero Nat by A3, A5;
take t = t; :: thesis: ( t < k & S₁[t] )
thus t < k by A5, NAT_1:13; :: thesis: S₁[t]
v |^ k = (v |^ t) * v by A5, NEWTON:6;
hence S₁[t] by A1, A4; :: thesis: verum

end;

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

proof

take n ; :: thesis: S₁[n]
thus S₁[n] by Def2; :: thesis: verum

end;

S₁[1] from COMPTRIG:sch 1(A6, A2);
hence contradiction by A1; :: thesis: verum