let n be Ordinal; for L being non trivial right_complementable well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for p, q being Polynomial of n,L holds
( - (p *' q) = (- p) *' q & - (p *' q) = p *' (- q) )
let L be non trivial right_complementable well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr ; for p, q being Polynomial of n,L holds
( - (p *' q) = (- p) *' q & - (p *' q) = p *' (- q) )
let p, q be Polynomial of n,L; ( - (p *' q) = (- p) *' q & - (p *' q) = p *' (- q) )
reconsider p9 = p, q9 = q as Element of (Polynom-Ring (n,L)) by POLYNOM1:def 11;
reconsider p9 = p9, q9 = q9 as Element of (Polynom-Ring (n,L)) ;
A1:
p9 * q9 = p *' q
by POLYNOM1:def 11;
- p = - p9
by Lm7;
then A2:
(- p9) * q9 = (- p) *' q
by POLYNOM1:def 11;
- q = - q9
by Lm7;
then A3:
p9 * (- q9) = p *' (- q)
by POLYNOM1:def 11;
( - (p9 * q9) = (- p9) * q9 & - (p9 * q9) = p9 * (- q9) )
by VECTSP_1:9;
hence
( - (p *' q) = (- p) *' q & - (p *' q) = p *' (- q) )
by A2, A3, A1, Lm7; verum