theorem vd: :: VECTSP13:39

for X being non empty set
for R being Ring
for L being non empty vector-distributive ModuleStr over R
for a, b being Element of R
for f, g being Function of X,L holds a '*' (f '+' g) = (a '*' f) '+' (a '*' g)