theorem Th32: :: BSPACE:32

for X being set
for u, v being Element of (bspace X)
for x being Element of X holds (u + v) @ x = (u @ x) + (v @ x)