for n being non zero Element of NAT holds
( n -BinaryVectSp is finite-dimensional & dim (n -BinaryVectSp) = n )