:: deftheorem defines ZeroB NBVECTSP:def 2 :
for n being non zero Element of NAT holds ZeroB n = n |-> 0;