let n be set ; :: thesis: for L being non empty right_complementable add-associative right_zeroed doubleLoopStr
for a being Element of L holds - (a | (n,L)) = (- a) | (n,L)
let L be non empty right_complementable add-associative right_zeroed doubleLoopStr ; :: thesis: for a being Element of L holds - (a | (n,L)) = (- a) | (n,L)
let a be Element of L; :: thesis: - (a | (n,L)) = (- a) | (n,L)

A1: now :: thesis: for u being object st u in dom ((- a) | (n,L)) holds
((- a) | (n,L)) . u = (- (a | (n,L))) . u

let u be object ; :: thesis: ( u in dom ((- a) | (n,L)) implies ((- a) | (n,L)) . u = (- (a | (n,L))) . u )
assume u in dom ((- a) | (n,L)) ; :: thesis: ((- a) | (n,L)) . u = (- (a | (n,L))) . u
then reconsider u9 = u as Element of Bags n ;

now :: thesis: ( ( u9 = EmptyBag n & - ((a | (n,L)) . u9) = ((- a) | (n,L)) . u9 ) or ( u9 <> EmptyBag n & - ((a | (n,L)) . u9) = ((- a) | (n,L)) . u9 ) )

per cases ( u9 = EmptyBag n or u9 <> EmptyBag n ) ;

case A2: u9 = EmptyBag n ; :: thesis: - ((a | (n,L)) . u9) = ((- a) | (n,L)) . u9

hence - ((a | (n,L)) . u9) = - a by POLYNOM7:18
.= ((- a) | (n,L)) . u9 by A2, POLYNOM7:18 ;
:: thesis: verum

end;

case A3: u9 <> EmptyBag n ; :: thesis: - ((a | (n,L)) . u9) = ((- a) | (n,L)) . u9

- (0. L) = 0. L by RLVECT_1:12;
hence - ((a | (n,L)) . u9) = 0. L by A3, POLYNOM7:18
.= ((- a) | (n,L)) . u9 by A3, POLYNOM7:18 ;
:: thesis: verum

end;

end;

end;

hence ((- a) | (n,L)) . u = (- (a | (n,L))) . u by POLYNOM1:17; :: thesis: verum

end;

dom (- (a | (n,L))) = Bags n by FUNCT_2:def 1
.= dom ((- a) | (n,L)) by FUNCT_2:def 1 ;
hence - (a | (n,L)) = (- a) | (n,L) by A1, FUNCT_1:2; :: thesis: verum