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 p1' = p1, p2' = p2 as Element of (Polynom-Ring L) by POLYNOM3:def 12;
A1: - (p1' + p2') = (- p1') + (- p2') by RLVECT_1:45;
A2: - p2 = - p2' by Lm5;
p1 + p2 = p1' + p2' by POLYNOM3:def 12;
then A3: - (p1 + p2) = - (p1' + p2') by Lm5;
- p1 = - p1' by Lm5;
hence - (p1 + p2) = (- p1) + (- p2) by A3, A2, A1, POLYNOM3:def 12; :: thesis: verum