let f be Polynomial of F_Complex; :: thesis: deg (f *') = deg f
A1: for k being Nat holds
( f . k = 0. F_Complex iff (f *') . k = 0. F_Complex )
proof
let k be Nat; :: thesis: ( f . k = 0. F_Complex iff (f *') . k = 0. F_Complex )
reconsider k1 = k as Element of NAT by ORDINAL1:def 12;
hereby :: thesis: ( (f *') . k = 0. F_Complex implies f . k = 0. F_Complex )
assume f . k = 0. F_Complex ; :: thesis: (f *') . k = 0. F_Complex
hence (f *') . k = ((power F_Complex) . ((- (1_ F_Complex)),k1)) * (0. F_Complex) by Def9, COMPLFLD:47
.= 0. F_Complex ;
:: thesis: verum
end;
assume (f *') . k = 0. F_Complex ; :: thesis: f . k = 0. F_Complex
then A2: 0. F_Complex = ((power F_Complex) . ((- (1_ F_Complex)),k1)) * ((f . k) *') by Def9;
(power F_Complex) . ((- (1_ F_Complex)),k1) <> 0. F_Complex by Th2;
then (f . k) *' = 0. F_Complex by A2, VECTSP_1:12;
hence f . k = 0. F_Complex by COMPLEX1:28, COMPLFLD:7; :: thesis: verum
end;
A3: now :: thesis: not len f > len (f *')
assume A4: len f > len (f *') ; :: thesis: contradiction
then (len f) + 1 > 0 + 1 by XREAL_1:6;
then len f >= 1 by NAT_1:13;
then reconsider l = (len f) - 1 as Element of NAT by INT_1:5;
l + 1 > len (f *') by A4;
then l >= len (f *') by NAT_1:13;
then A5: (f *') . l = 0. F_Complex by ALGSEQ_1:8;
len f = l + 1 ;
then f . l <> 0. F_Complex by ALGSEQ_1:10;
hence contradiction by A1, A5; :: thesis: verum
end;
now :: thesis: for i being Nat st i >= len f holds
(f *') . i = 0. F_Complex
let i be Nat; :: thesis: ( i >= len f implies (f *') . i = 0. F_Complex )
assume i >= len f ; :: thesis: (f *') . i = 0. F_Complex
then f . i = 0. F_Complex by ALGSEQ_1:8;
hence (f *') . i = 0. F_Complex by A1; :: thesis: verum
end;
then len f is_at_least_length_of f *' by ALGSEQ_1:def 2;
then len f >= len (f *') by ALGSEQ_1:def 3;
hence deg (f *') = deg f by A3, XXREAL_0:1; :: thesis: verum