theorem :: REALSET2:15

for F being Field
for a, b being Element of F holds - (a * b) = a * (- b) by VECTSP_1:8;