let L be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for p being Polynomial of L holds len (- p) = len p
let p be Polynomial of L; :: thesis: len (- p) = len p
A1: len p is_at_least_length_of - p

proof

let i be Nat; :: according to ALGSEQ_1:def 3 :: thesis: ( not len p <= i or (- p) . i = 0. L )
assume A2: i >= len p ; :: thesis: (- p) . i = 0. L
i in NAT by ORDINAL1:def 13;
hence (- p) . i = - (p . i) by BHSP_1:def 10
.= - (0. L) by A2, ALGSEQ_1:22
.= 0. L by RLVECT_1:25 ;
:: thesis: verum

end;

now

let n be Nat; :: thesis: ( n is_at_least_length_of - p implies len p <= n )
assume A3: n is_at_least_length_of - p ; :: thesis: len p <= n
n is_at_least_length_of p

proof

let i be Nat; :: according to ALGSEQ_1:def 3 :: thesis: ( not n <= i or p . i = 0. L )
A4: i in NAT by ORDINAL1:def 13;
assume i >= n ; :: thesis: p . i = 0. L
then (- p) . i = 0. L by A3, ALGSEQ_1:def 3;
then - (p . i) = 0. L by A4, BHSP_1:def 10;
hence p . i = 0. L by VECTSP_2:34; :: thesis: verum

end;

hence len p <= n by ALGSEQ_1:def 4; :: thesis: verum

end;

hence len (- p) = len p by A1, ALGSEQ_1:def 4; :: thesis: verum