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 S1[ 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 & S1[k] holds
ex t being non zero Element of NAT st
( t < k & S1[t] )
let k be non zero Element of NAT ; :: thesis: ( k <> 1 & S1[k] implies ex t being non zero Element of NAT st
( t < k & S1[t] ) )
assume that
A2: k <> 1 and
A3: S1[k] ; :: thesis: ex t being non zero Element of NAT st
( t < k & S1[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 & S1[t] )
thus t < k by A4, NAT_1:13; :: thesis: S1[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 S1[t] by NAT_1:3, VECTSP_1:36; :: thesis: verum
end;
A5: ex n being non zero Element of NAT st S1[n]
proof
take n ; :: thesis: S1[n]
thus S1[n] by Def2; :: thesis: verum
end;
S1[1] from COMPLFLD:sch 1(A5, A1);
hence v = 0. F_Complex by GROUP_1:50; :: thesis: verum