let L be non empty right_complementable left-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:41
.= ((- 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