theorem sd: :: VECTSP13:34

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