let n be set ; :: thesis: for L being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for p, q being Series of n,L holds - (p + q) = (- p) + (- q)
let L be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; :: thesis: for p, q being Series of n,L holds - (p + q) = (- p) + (- q)
let p, q be Series of n,L; :: thesis: - (p + q) = (- p) + (- q)

A1: now

let x be set ; :: thesis: ( x in dom (- (p + q)) implies (- (p + q)) . x = ((- p) + (- q)) . x )
assume x in dom (- (p + q)) ; :: thesis: (- (p + q)) . x = ((- p) + (- q)) . x
then reconsider b = x as bag of n by PRE_POLY:def 12;
((- p) + (- q)) . b = ((- p) . b) + ((- q) . b) by POLYNOM1:def 21
.= (- (p . b)) + ((- q) . b) by POLYNOM1:def 22
.= (- (p . b)) + (- (q . b)) by POLYNOM1:def 22
.= - ((q . b) + (p . b)) by RLVECT_1:45
.= - ((p + q) . b) by POLYNOM1:def 21
.= (- (p + q)) . b by POLYNOM1:def 22 ;
hence (- (p + q)) . x = ((- p) + (- q)) . x ; :: thesis: verum

end;

dom (- (p + q)) = Bags n by FUNCT_2:def 1
.= dom ((- p) + (- q)) by FUNCT_2:def 1 ;
hence - (p + q) = (- p) + (- q) by A1, FUNCT_1:9; :: thesis: verum