theorem :: REALSET2:12

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