theorem Th26: :: BSPACE:26

for X being set
for a, b being Element of Z_2
for x being Element of (bspace X) holds (a + b) * x = (a * x) + (b * x)