theorem Th27: :: BSPACE:27

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