theorem :: VECTSP_1:13

for K being non empty right_complementable add-associative right_zeroed left-distributive doubleLoopStr
for a, b, c being Element of K holds (a - b) * c = (a * c) - (b * c)