let L be non empty right_complementable distributive Abelian add-associative right_zeroed doubleLoopStr ; :: thesis: for p1, p2 being Polynomial of L holds
( - (p1 *' p2) = (- p1) *' p2 & - (p1 *' p2) = p1 *' (- p2) )
let p1, p2 be Polynomial of L; :: thesis: ( - (p1 *' p2) = (- p1) *' p2 & - (p1 *' p2) = p1 *' (- p2) )
reconsider p19 = p1, p29 = p2 as Element of (Polynom-Ring L) by POLYNOM3:def 10;
p1 *' p2 = p19 * p29 by POLYNOM3:def 10;
then A1: - (p1 *' p2) = - (p19 * p29) by Lm4;
- p1 = - p19 by Lm4;
then (- p1) *' p2 = (- p19) * p29 by POLYNOM3:def 10;
hence - (p1 *' p2) = (- p1) *' p2 by A1, VECTSP_1:9; :: thesis: - (p1 *' p2) = p1 *' (- p2)
- p2 = - p29 by Lm4;
then p1 *' (- p2) = p19 * (- p29) by POLYNOM3:def 10;
hence - (p1 *' p2) = p1 *' (- p2) by A1, VECTSP_1:8; :: thesis: verum