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 :: thesis: for x being object st x in dom (- (p + q)) holds
(- (p + q)) . x = ((- p) + (- q)) . x

let x be object ; :: 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 ;
((- p) + (- q)) . b = ((- p) . b) + ((- q) . b) by POLYNOM1:15
.= (- (p . b)) + ((- q) . b) by POLYNOM1:17
.= (- (p . b)) + (- (q . b)) by POLYNOM1:17
.= - ((q . b) + (p . b)) by RLVECT_1:31
.= - ((p + q) . b) by POLYNOM1:15
.= (- (p + q)) . b by POLYNOM1:17 ;
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:2; :: thesis: verum