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 :: 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:8
.= x * ((- p) . i) by BHSP_1:44
.= (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