theorem :: REALSET2:11

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