let n be Ordinal; :: thesis: 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 ; :: thesis: 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; :: thesis: ( - (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; :: thesis: verum