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 p1' = p1, p2' = p2 as Element of (Polynom-Ring L) by POLYNOM3:def 12;
p1 *' p2 = p1' * p2' by POLYNOM3:def 12;
then A1: - (p1 *' p2) = - (p1' * p2') by Lm5;
- p1 = - p1' by Lm5;
then (- p1) *' p2 = (- p1') * p2' by POLYNOM3:def 12;
hence - (p1 *' p2) = (- p1) *' p2 by A1, VECTSP_1:41; :: thesis: - (p1 *' p2) = p1 *' (- p2)
- p2 = - p2' by Lm5;
then p1 *' (- p2) = p1' * (- p2') by POLYNOM3:def 12;
hence - (p1 *' p2) = p1 *' (- p2) by A1, VECTSP_1:40; :: thesis: verum