theorem Th13: :: NBVECTSP:13

for n being non zero Element of NAT ex B being finite Subset of (n -BinaryVectSp) st
( B is Basis of (n -BinaryVectSp) & card B = n & ex A being FinSequence of n -tuples_on BOOLEAN st
( len A = n & A is one-to-one & card (rng A) = n & rng A = B & ( for i, j being Nat st i in Seg n & j in Seg n holds
( ( i = j implies (A . i) . j = TRUE ) & ( i <> j implies (A . i) . j = FALSE ) ) ) ) )