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;
p1 + p2 = p1' + p2' by POLYNOM3:def 12;
then A1: - (p1 + p2) = - (p1' + p2') by Lm5;
A2: ( - p1 = - p1' & - p2 = - p2' ) by Lm5;
- (p1' + p2') = (- p1') + (- p2') by RLVECT_1:45;
hence - (p1 + p2) = (- p1) + (- p2) by A1, A2, POLYNOM3:def 12; :: thesis: verum