for n being non zero Element of NAT
for A being FinSequence of n -tuples_on BOOLEAN
for B being finite Subset of (n -BinaryVectSp) st rng A = B & len A = n & A is one-to-one & ( 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 ) ) ) holds
Lin B = ModuleStr(# the carrier of (n -BinaryVectSp), the addF of (n -BinaryVectSp), the ZeroF of (n -BinaryVectSp), the lmult of (n -BinaryVectSp) #)