theorem Th25: :: BSPACE:25

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