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