:: deftheorem defines -BinaryVectSp NBVECTSP:def 5 :
for n being non zero Element of NAT holds n -BinaryVectSp = ModuleStr(# (n -tuples_on BOOLEAN),(XORB n),(ZeroB n),(MLTB n) #);