theorem Th17: :: BSPACE:17

for X being set
for a being Element of Z_2
for c, d being Subset of X holds a \*\ (c \+\ d) = (a \*\ c) \+\ (a \*\ d)