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

let u be set ; :: 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

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:25;
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:def 22; :: 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:9; :: thesis: verum