let R be Ring; :: thesis: for p1, p2 being Polynomial of R holds p1 *' (- p2) = - (p1 *' p2)
let p1, p2 be Polynomial of R; :: thesis: p1 *' (- p2) = - (p1 *' p2)
reconsider a = p1, b = p2 as Element of the carrier of (Polynom-Ring R) by POLYNOM3:def 10;
A: a * b = p1 *' p2 by POLYNOM3:def 10;
- p2 = - b by FIELD_8:1;
hence p1 *' (- p2) = a * (- b) by POLYNOM3:def 10
.= - (a * b) by VECTSP_1:8
.= - (p1 *' p2) by A, FIELD_8:1 ;
:: thesis: verum