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 13;

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:83
.= 0. F_Complex by VECTSP_1:36 ;
:: 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:44;
hence f . k = 0. F_Complex by COMPLEX1:113, COMPLFLD:9; :: thesis: verum

end;

now

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:22;
hence (f *' ) . i = 0. F_Complex by A1; :: thesis: verum

end;

then len f is_at_least_length_of f *' by ALGSEQ_1:def 3;
then A3: len f >= len (f *' ) by ALGSEQ_1:def 4;

now

assume A4: len f > len (f *' ) ; :: thesis: contradiction
then (len f) + 1 > 0 + 1 by XREAL_1:8;
then len f >= 1 by NAT_1:13;
then reconsider l = (len f) - 1 as Element of NAT by INT_1:18;
l + 1 > len (f *' ) by A4;
then l >= len (f *' ) by NAT_1:13;
then A5: (f *' ) . l = 0. F_Complex by ALGSEQ_1:22;
len f = l + 1 ;
then f . l <> 0. F_Complex by ALGSEQ_1:25;
hence contradiction by A1, A5; :: thesis: verum

end;

hence deg (f *' ) = deg f by A3, XXREAL_0:1; :: thesis: verum