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

now

let u be set ; :: 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 u' = u as bag of n by POLYNOM1:def 14;
(- (a * p)) . u' = - ((a * p) . u') by POLYNOM1:def 22
.= - (a * (p . u')) by POLYNOM7:def 10
.= (- a) * (p . u') by VECTSP_1:41
.= ((- a) * p) . u' by POLYNOM7:def 10 ;
hence (- (a * p)) . u = ((- a) * p) . u ; :: thesis: verum

end;

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

now

let u be set ; :: 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 u' = u as bag of n by POLYNOM1:def 14;
(- (a * p)) . u' = - ((a * p) . u') by POLYNOM1:def 22
.= - (a * (p . u')) by POLYNOM7:def 10
.= a * (- (p . u')) by VECTSP_1:40
.= a * ((- p) . u') by POLYNOM1:def 22
.= (a * (- p)) . u' by POLYNOM7:def 10 ;
hence (- (a * p)) . u = (a * (- p)) . u ; :: thesis: verum

end;

hence - (a * p) = a * (- p) by A2, FUNCT_1:9; :: thesis: verum