theorem Th8: :: NBVECTSP:8

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