theorem Th6: :: NBVECTSP:6

for m, n being non zero Element of NAT
for L being the carrier of (b₂ -BinaryVectSp) -valued FinSequence
for j being Nat st len L = m & m <= n & j in Seg n holds
ex x being FinSequence of Z_2 st
( len x = m & ( for i being Nat st i in Seg m holds
ex K being Element of n -tuples_on BOOLEAN st
( K = L . i & x . i = K . j ) ) )