let m, n be non zero Element of NAT ; :: thesis: for A being FinSequence of n -tuples_on BOOLEAN
for B being finite Subset of () st rng A = B & m <= n & len A = m & 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
B is linearly-independent

let A be FinSequence of n -tuples_on BOOLEAN; :: thesis: for B being finite Subset of () st rng A = B & m <= n & len A = m & 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
B is linearly-independent

let B be finite Subset of (); :: thesis: ( rng A = B & m <= n & len A = m & 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 ) ) ) implies B is linearly-independent )

assume that
A1: rng A = B and
A2: m <= n and
A3: len A = m and
A4: A is one-to-one and
A5: 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 ) ) ; :: thesis:
set V = n -BinaryVectSp ;
for l being Linear_Combination of B st Sum l = 0. () holds
Carrier l = {}
proof
let l be Linear_Combination of B; :: thesis: ( Sum l = 0. () implies Carrier l = {} )
assume A6: Sum l = 0. () ; :: thesis:
assume Carrier l <> {} ; :: thesis: contradiction
then consider x being object such that
A7: x in Carrier l by XBOOLE_0:def 1;
consider v being Element of () such that
A8: ( x = v & l . v <> 0. Z_2 ) by A7;
A9: Carrier l c= B by VECTSP_6:def 4;
reconsider Suml = Sum l as Element of n -tuples_on BOOLEAN ;
consider j being object such that
A10: ( j in dom A & v = A . j ) by ;
A11: j in Seg m by ;
reconsider j = j as Nat by A10;
Suml . j = l . (A . j) by Th9, A1, A2, A3, A4, A5, A11;
hence contradiction by A6, A8, A10, BSPACE:5; :: thesis: verum
end;
hence B is linearly-independent by VECTSP_7:def 1; :: thesis: verum