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 (Polynom-Ring n,L) by POLYNOM1:def 27;
reconsider p' = p', q' = q' as Element of (Polynom-Ring n,L) ;
A1: - p = - p' by Lm7;
- q = - q' by Lm7;
then A2: ( (- p') * q' = (- p) *' q & p' * (- q') = p *' (- q) ) by A1, POLYNOM1:def 27;
A3: ( - (p' * q') = (- p') * q' & - (p' * q') = p' * (- q') ) by VECTSP_1:41;
p' * q' = p *' q by POLYNOM1:def 27;
hence ( - (p *' q) = (- p) *' q & - (p *' q) = p *' (- q) ) by A2, A3, Lm7; :: thesis: verum