:: deftheorem Def6 defines bspace-scalar-mult BSPACE:def 6 :
for X being set
for b₂ being Function of [: the carrier of Z_2,(bool X):],(bool X) holds
( b₂ = bspace-scalar-mult X iff for a being Element of Z_2
for c being Subset of X holds b₂ . (a,c) = a \*\ c );