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 :: thesis: for i9 being object st i9 in dom (- (x * p)) holds
(- (x * p)) . i9 = ((- x) * p) . i9

let i9 be object ; :: 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:44
.= - (x * (p . i)) by POLYNOM5:def 4
.= (- x) * (p . i) by VECTSP_1:9
.= ((- x) * p) . i by POLYNOM5:def 4 ;
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:2; :: thesis: verum