:: deftheorem Def4 defines MLTB NBVECTSP:def 4 :
for n being non zero Element of NAT
for b₂ being Function of [: the carrier of Z_2,(n -tuples_on BOOLEAN):],(n -tuples_on BOOLEAN) holds
( b₂ = MLTB n iff for a being Element of BOOLEAN
for x being Element of n -tuples_on BOOLEAN
for i being set st i in Seg n holds
(b₂ . (a,x)) . i = a '&' (x . i) );