let F be Field; :: thesis: for m being Ordinal
for p being Polynomial of F holds Poly (m,(- p)) = - (Poly (m,p))
let m be Ordinal; :: thesis: for p being Polynomial of F holds Poly (m,(- p)) = - (Poly (m,p))
let p be Polynomial of F; :: thesis: Poly (m,(- p)) = - (Poly (m,p))
set r1 = Poly (m,p);
set r2 = Poly (m,(- p));
set n = card (nonConstantPolys F);
I: dom (Poly (m,(- p))) = Bags (card (nonConstantPolys F)) by FUNCT_2:def 1
.= dom (- (Poly (m,p))) by FUNCT_2:def 1 ;

now :: thesis: for o being object st o in dom (Poly (m,(- p))) holds
(Poly (m,(- p))) . o = (- (Poly (m,p))) . o

let o be object ; :: thesis: ( o in dom (Poly (m,(- p))) implies (Poly (m,(- p))) . b₁ = (- (Poly (m,p))) . b₁ )
assume o in dom (Poly (m,(- p))) ; :: thesis: (Poly (m,(- p))) . b₁ = (- (Poly (m,p))) . b₁
then reconsider b = o as bag of card (nonConstantPolys F) ;

per cases ( support b = {} or support b = {m} or ( support b <> {} & support b <> {m} ) ) ;

suppose support b = {} ; :: thesis: (Poly (m,(- p))) . b₁ = (- (Poly (m,p))) . b₁

then for i being object st i in card (nonConstantPolys F) holds
b . i = {} by PRE_POLY:def 7;
then H: b = EmptyBag (card (nonConstantPolys F)) by PBOOLE:6;
(Poly (m,(- p))) . b = (- p) . 0 by H, defPg
.= - (p . 0) by BHSP_1:44
.= - ((Poly (m,p)) . b) by H, defPg
.= (- (Poly (m,p))) . b by POLYNOM1:17 ;
hence (Poly (m,(- p))) . o = (- (Poly (m,p))) . o ; :: thesis: verum

end;

suppose H: support b = {m} ; :: thesis: (Poly (m,(- p))) . b₁ = (- (Poly (m,p))) . b₁

then (Poly (m,(- p))) . b = (- p) . (b . m) by defPg
.= - (p . (b . m)) by BHSP_1:44
.= - ((Poly (m,p)) . b) by H, defPg
.= (- (Poly (m,p))) . b by POLYNOM1:17 ;
hence (Poly (m,(- p))) . o = (- (Poly (m,p))) . o ; :: thesis: verum

end;

suppose H: ( support b <> {} & support b <> {m} ) ; :: thesis: (Poly (m,(- p))) . b₁ = (- (Poly (m,p))) . b₁

then (Poly (m,(- p))) . b = - (0. F) by defPg
.= - ((Poly (m,p)) . b) by H, defPg
.= (- (Poly (m,p))) . b by POLYNOM1:17 ;
hence (Poly (m,(- p))) . o = (- (Poly (m,p))) . o ; :: thesis: verum

end;

end;

end;

hence Poly (m,(- p)) = - (Poly (m,p)) by I; :: thesis: verum