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)
let p1, p2 be Polynomial of L; :: thesis: - (p1 + p2) = (- p1) + (- p2)
reconsider p19 = p1, p29 = p2 as Element of (Polynom-Ring L) by POLYNOM3:def 10;
A1: - (p19 + p29) = (- p19) + (- p29) by RLVECT_1:31;
A2: - p2 = - p29 by Lm4;
p1 + p2 = p19 + p29 by POLYNOM3:def 10;
then A3: - (p1 + p2) = - (p19 + p29) by Lm4;
- p1 = - p19 by Lm4;
hence - (p1 + p2) = (- p1) + (- p2) by A3, A2, A1, POLYNOM3:def 10; :: thesis: verum