let n be Ordinal; :: thesis: for L being non trivial right_complementable associative commutative well-unital distributive Abelian add-associative right_zeroed 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 associative commutative well-unital distributive Abelian add-associative right_zeroed 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 p' = p, q' = q as Element of by POLYNOM1:def 27;
reconsider p' = p', q' = q' as Element of ;
A1: p' * q' = p *' q by POLYNOM1:def 27;
- p = - p' by Lm7;
then A2: (- p') * q' = (- p) *' q by POLYNOM1:def 27;
- q = - q' by Lm7;
then A3: p' * (- q') = p *' (- q) by POLYNOM1:def 27;
( - (p' * q') = (- p') * q' & - (p' * q') = p' * (- q') ) by VECTSP_1:41;
hence ( - (p *' q) = (- p) *' q & - (p *' q) = p *' (- q) ) by A2, A3, A1, Lm7; :: thesis: verum