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

let x be object ; :: 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 ;
(- (0_ (X,L))) . b = - ((0_ (X,L)) . b) by POLYNOM1:17
.= - (0. L) by POLYNOM1:22
.= 0. L by RLVECT_1:12
.= (0_ (X,L)) . b by POLYNOM1:22 ;
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:2; :: thesis: verum