let n be non zero Element of NAT ; :: thesis: ex B being finite Subset of (n -BinaryVectSp) st

( B is Basis of (n -BinaryVectSp) & card B = n & ex A being FinSequence of n -tuples_on BOOLEAN st

( len A = n & A is one-to-one & card (rng A) = n & rng A = B & ( 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 ) ) ) ) )

set V = n -BinaryVectSp ;

consider A being FinSequence of n -tuples_on BOOLEAN such that

A1: ( len A = n & A is one-to-one & card (rng A) = n & ( 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 ) ) ) ) by Th8;

reconsider B = rng A as finite Subset of (n -BinaryVectSp) ;

A2: B is linearly-independent by A1, Th10;

Lin B = ModuleStr(# the carrier of (n -BinaryVectSp), the addF of (n -BinaryVectSp), the ZeroF of (n -BinaryVectSp), the lmult of (n -BinaryVectSp) #) by A1, Th12;

then B is Basis of (n -BinaryVectSp) by VECTSP_7:def 3, A2;

hence ex B being finite Subset of (n -BinaryVectSp) st

( B is Basis of (n -BinaryVectSp) & card B = n & ex A being FinSequence of n -tuples_on BOOLEAN st

( len A = n & A is one-to-one & card (rng A) = n & rng A = B & ( 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 ) ) ) ) ) by A1; :: thesis: verum

( B is Basis of (n -BinaryVectSp) & card B = n & ex A being FinSequence of n -tuples_on BOOLEAN st

( len A = n & A is one-to-one & card (rng A) = n & rng A = B & ( 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 ) ) ) ) )

set V = n -BinaryVectSp ;

consider A being FinSequence of n -tuples_on BOOLEAN such that

A1: ( len A = n & A is one-to-one & card (rng A) = n & ( 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 ) ) ) ) by Th8;

reconsider B = rng A as finite Subset of (n -BinaryVectSp) ;

A2: B is linearly-independent by A1, Th10;

Lin B = ModuleStr(# the carrier of (n -BinaryVectSp), the addF of (n -BinaryVectSp), the ZeroF of (n -BinaryVectSp), the lmult of (n -BinaryVectSp) #) by A1, Th12;

then B is Basis of (n -BinaryVectSp) by VECTSP_7:def 3, A2;

hence ex B being finite Subset of (n -BinaryVectSp) st

( B is Basis of (n -BinaryVectSp) & card B = n & ex A being FinSequence of n -tuples_on BOOLEAN st

( len A = n & A is one-to-one & card (rng A) = n & rng A = B & ( 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 ) ) ) ) ) by A1; :: thesis: verum