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

let x be Nat; :: thesis: ( x < len p implies (- (- p)) . x = p . x )
assume x < len p ; :: thesis: (- (- p)) . x = p . x
A2: x in NAT by ORDINAL1:def 13;
hence (- (- p)) . x = - ((- p) . x) by BHSP_1:def 10
.= - (- (p . x)) by A2, BHSP_1:def 10
.= p . x by RLVECT_1:30 ;
:: thesis: verum

end;

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