theorem :: VECTSP_1:11

for F being non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr
for x, y, z being Element of F holds x * (y - z) = (x * y) - (x * z)