theorem :: NBVECTSP:15

for n being non zero Element of NAT
for A being FinSequence of n -tuples_on BOOLEAN
for C being Subset of (n -BinaryVectSp) st len A = n & A is one-to-one & card (rng A) = n & ( 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 ) ) ) & C c= rng A holds
( Lin C is Subspace of n -BinaryVectSp & C is Basis of (Lin C) & dim (Lin C) = card C )