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

A1: now

let x be set ; :: thesis: ( x in dom (- (0_ X,L)) implies (- (0_ X,L)) . x = (0_ X,L) . x )
assume x in dom (- (0_ X,L)) ; :: thesis: (- (0_ X,L)) . x = (0_ X,L) . x
then reconsider b = x as bag of X by PRE_POLY:def 12;
(- (0_ X,L)) . b = - ((0_ X,L) . b) by POLYNOM1:def 22
.= - (0. L) by POLYNOM1:81
.= 0. L by RLVECT_1:25
.= (0_ X,L) . b by POLYNOM1:81 ;
hence (- (0_ X,L)) . x = (0_ X,L) . x ; :: thesis: verum

end;

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