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: now :: thesis: for n being Nat st n is_at_least_length_of - p holds
len p <= n

let n be Nat; :: thesis: ( n is_at_least_length_of - p implies len p <= n )
assume A2: 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 2 :: thesis: ( not n <= i or p . i = 0. L )
assume i >= n ; :: thesis: p . i = 0. L
then ( i in NAT & (- p) . i = 0. L ) by A2, ORDINAL1:def 12;
then - (p . i) = 0. L by BHSP_1:44;
hence p . i = 0. L by VECTSP_2:3; :: thesis: verum

end;

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

end;

len p is_at_least_length_of - p

proof

let i be Nat; :: according to ALGSEQ_1:def 2 :: thesis: ( not len p <= i or (- p) . i = 0. L )
assume A3: i >= len p ; :: thesis: (- p) . i = 0. L
thus (- p) . i = - (p . i) by BHSP_1:44
.= - (0. L) by A3, ALGSEQ_1:8
.= 0. L by RLVECT_1:12 ; :: thesis: verum

end;

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