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 :: thesis: for x being object st x in dom ((0_ (X,L)) - f) holds
((0_ (X,L)) - f) . x = (- f) . x

let x be object ; :: 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 7
.= ((0_ (X,L)) . b) + ((- f) . b) by POLYNOM1:15
.= (0. L) + ((- f) . b) by POLYNOM1:22
.= (- f) . b by ALGSTR_1:def 2 ;
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:2; :: thesis: verum