for m, n being non zero Element of NAT
for L being the carrier of (b₂ -BinaryVectSp) -valued FinSequence
for Suml being Element of n -tuples_on BOOLEAN
for j being Nat st len L = m & m <= n & Suml = Sum L & j in Seg n holds
ex x being FinSequence of Z_2 st
( len x = m & Suml . j = Sum x & ( 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 ) ) )