let L be non empty right_complementable right-distributive add-associative right_zeroed doubleLoopStr ; :: thesis: for p being Polynomial of L
for x being Element of L holds - (x * p) = x * (- p)
let p be Polynomial of L; :: thesis: for x being Element of L holds - (x * p) = x * (- p)
let x be Element of L; :: thesis: - (x * p) = x * (- p)
set f = - (x * p);
set g = x * (- p);

A1: now

let i9 be set ; :: thesis: ( i9 in dom (- (x * p)) implies (- (x * p)) . i9 = (x * (- p)) . i9 )
assume i9 in dom (- (x * p)) ; :: thesis: (- (x * p)) . i9 = (x * (- p)) . i9
then reconsider i = i9 as Element of NAT ;
(- (x * p)) . i = - ((x * p) . i) by BHSP_1:def 10
.= - (x * (p . i)) by POLYNOM5:def 3
.= x * (- (p . i)) by VECTSP_1:40
.= x * ((- p) . i) by BHSP_1:def 10
.= (x * (- p)) . i by POLYNOM5:def 3 ;
hence (- (x * p)) . i9 = (x * (- p)) . i9 ; :: thesis: verum

end;

dom (- (x * p)) = NAT by FUNCT_2:def 1
.= dom (x * (- p)) by FUNCT_2:def 1 ;
hence - (x * p) = x * (- p) by A1, FUNCT_1:9; :: thesis: verum