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

A1: now :: thesis: for x being Nat st x < len p holds
(- (- p)) . x = p . x

let x be Nat; :: thesis: ( x < len p implies (- (- p)) . x = p . x )
assume x < len p ; :: thesis: (- (- p)) . x = p . x
thus (- (- p)) . x = - ((- p) . x) by BHSP_1:44
.= - (- (p . x)) by BHSP_1:44
.= p . x by RLVECT_1:17 ; :: thesis: verum

end;

len p = len (- p) by POLYNOM4:8
.= len (- (- p)) by POLYNOM4:8 ;
hence - (- p) = p by A1, ALGSEQ_1:12; :: thesis: verum