let n be non zero Element of NAT ; :: thesis: for v being CRoot of n, 0. F_Complex holds v = 0. F_Complex
let v be CRoot of n, 0. F_Complex; :: thesis: v = 0. F_Complex
defpred S₁[ Element of omega ] means (power F_Complex) . (v,$1) = 0. F_Complex;

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

let k be non zero Element of NAT ; :: thesis: ( k <> 1 & S₁[k] implies ex t being non zero Element of NAT st
( t < k & S₁[t] ) )
assume that
A2: k <> 1 and
A3: S₁[k] ; :: thesis: ex t being non zero Element of NAT st
( t < k & S₁[t] )
consider t being Nat such that
A4: k = t + 1 by NAT_1:6;
reconsider t = t as Element of NAT by ORDINAL1:def 12;
reconsider t = t as non zero Element of NAT by A2, A4;
take t = t; :: thesis: ( t < k & S₁[t] )
thus t < k by A4, NAT_1:13; :: thesis: S₁[t]
(power F_Complex) . (v,k) = ((power F_Complex) . (v,t)) * v by A4, GROUP_1:def 7;
then ( (power F_Complex) . (v,t) = 0. F_Complex or v = 0. F_Complex ) by A3, VECTSP_1:12;
hence S₁[t] by NAT_1:3, VECTSP_1:36; :: thesis: verum

end;

A5: ex n being non zero Element of NAT st S₁[n]

proof

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

end;

S₁[1] from COMPLFLD:sch 1(A5, A1);
hence v = 0. F_Complex by GROUP_1:50; :: thesis: verum