let X be set ; :: thesis: for L being non empty right_complementable add-associative right_zeroed addLoopStr
for f being Series of X,L holds (0_ X,L) - f = - f
let L be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for f being Series of X,L holds (0_ X,L) - f = - f
let f be Series of X,L; :: thesis: (0_ X,L) - f = - f
set p = (0_ X,L) - f;

A1: now

let x be set ; :: thesis: ( x in dom ((0_ X,L) - f) implies ((0_ X,L) - f) . x = (- f) . x )
assume x in dom ((0_ X,L) - f) ; :: thesis: ((0_ X,L) - f) . x = (- f) . x
then reconsider b = x as Element of Bags X ;
((0_ X,L) - f) . b = ((0_ X,L) + (- f)) . b by POLYNOM1:def 23
.= ((0_ X,L) . b) + ((- f) . b) by POLYNOM1:def 21
.= (0. L) + ((- f) . b) by POLYNOM1:81
.= (- f) . b by ALGSTR_1:def 5 ;
hence ((0_ X,L) - f) . x = (- f) . x ; :: thesis: verum

end;

dom ((0_ X,L) - f) = Bags X by FUNCT_2:def 1
.= dom (- f) by FUNCT_2:def 1 ;
hence (0_ X,L) - f = - f by A1, FUNCT_1:9; :: thesis: verum