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: dom (- (a | n,L)) = Bags n by FUNCT_2:def 1
.= dom ((- a) | n,L) by FUNCT_2:def 1 ;

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 u' = u as Element of Bags n ;

now

per cases ( u' = EmptyBag n or u' <> EmptyBag n ) ;

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

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

end;

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

- (0. L) = 0. L by RLVECT_1:25;
hence - ((a | n,L) . u') = 0. L by A3, POLYNOM7:18
.= ((- a) | n,L) . u' 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;

hence - (a | n,L) = (- a) | n,L by A1, FUNCT_1:9; :: thesis: verum