let n be set ; :: thesis: for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr
for p being Series of n,L
for a being Element of L holds
( - (a * p) = (- a) * p & - (a * p) = a * (- p) )
let L be non empty right_complementable distributive add-associative right_zeroed doubleLoopStr ; :: thesis: for p being Series of n,L
for a being Element of L holds
( - (a * p) = (- a) * p & - (a * p) = a * (- p) )
let p be Series of n,L; :: thesis: for a being Element of L holds
( - (a * p) = (- a) * p & - (a * p) = a * (- p) )
let a be Element of L; :: thesis: ( - (a * p) = (- a) * p & - (a * p) = a * (- p) )
set ap = a * p;

A1: now :: thesis: for u being object st u in dom (- (a * p)) holds
(- (a * p)) . u = ((- a) * p) . u

let u be object ; :: thesis: ( u in dom (- (a * p)) implies (- (a * p)) . u = ((- a) * p) . u )
assume u in dom (- (a * p)) ; :: thesis: (- (a * p)) . u = ((- a) * p) . u
then reconsider u9 = u as bag of n ;
(- (a * p)) . u9 = - ((a * p) . u9) by POLYNOM1:17
.= - (a * (p . u9)) by POLYNOM7:def 9
.= (- a) * (p . u9) by VECTSP_1:9
.= ((- a) * p) . u9 by POLYNOM7:def 9 ;
hence (- (a * p)) . u = ((- a) * p) . u ; :: thesis: verum

end;

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

A2: now :: thesis: for u being object st u in dom (- (a * p)) holds
(- (a * p)) . u = (a * (- p)) . u

let u be object ; :: thesis: ( u in dom (- (a * p)) implies (- (a * p)) . u = (a * (- p)) . u )
assume u in dom (- (a * p)) ; :: thesis: (- (a * p)) . u = (a * (- p)) . u
then reconsider u9 = u as bag of n ;
(- (a * p)) . u9 = - ((a * p) . u9) by POLYNOM1:17
.= - (a * (p . u9)) by POLYNOM7:def 9
.= a * (- (p . u9)) by VECTSP_1:8
.= a * ((- p) . u9) by POLYNOM1:17
.= (a * (- p)) . u9 by POLYNOM7:def 9 ;
hence (- (a * p)) . u = (a * (- p)) . u ; :: thesis: verum

end;

dom (- (a * p)) = Bags n by FUNCT_2:def 1
.= dom (a * (- p)) by FUNCT_2:def 1 ;
hence - (a * p) = a * (- p) by A2, FUNCT_1:2; :: thesis: verum