theorem vd: :: VECTSP13:36

for X being non empty set
for L being non empty right-distributive doubleLoopStr
for a being Element of L
for f, g being Function of X,L holds a '*' (f '+' g) = (a '*' f) '+' (a '*' g)