let n be non zero Element of NAT ; :: thesis: for A being FinSequence of n -tuples_on BOOLEAN

for C being Subset of (n -BinaryVectSp) st 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 ) ) ) & C c= rng A holds

( Lin C is Subspace of n -BinaryVectSp & C is Basis of (Lin C) & dim (Lin C) = card C )

let A be FinSequence of n -tuples_on BOOLEAN; :: thesis: for C being Subset of (n -BinaryVectSp) st 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 ) ) ) & C c= rng A holds

( Lin C is Subspace of n -BinaryVectSp & C is Basis of (Lin C) & dim (Lin C) = card C )

let C be Subset of (n -BinaryVectSp); :: thesis: ( 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 ) ) ) & C c= rng A implies ( Lin C is Subspace of n -BinaryVectSp & C is Basis of (Lin C) & dim (Lin C) = card C ) )

assume 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 ) ) ) ) ; :: thesis: ( not C c= rng A or ( Lin C is Subspace of n -BinaryVectSp & C is Basis of (Lin C) & dim (Lin C) = card C ) )

assume A2: C c= rng A ; :: thesis: ( Lin C is Subspace of n -BinaryVectSp & C is Basis of (Lin C) & dim (Lin C) = card C )

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

B is linearly-independent by A1, Th10;

then A3: C is linearly-independent by A2, VECTSP_7:1;

for x being object st x in C holds

x in the carrier of (Lin C) by VECTSP_7:8, STRUCT_0:def 5;

then reconsider C0 = C as Subset of (Lin C) by TARSKI:def 3;

Lin C0 = ModuleStr(# the carrier of (Lin C), the addF of (Lin C), the ZeroF of (Lin C), the lmult of (Lin C) #) by VECTSP_9:17;

then C0 is Basis of (Lin C) by VECTSP_7:def 3, A3, VECTSP_9:12;

hence ( Lin C is Subspace of n -BinaryVectSp & C is Basis of (Lin C) & dim (Lin C) = card C ) by VECTSP_9:def 1; :: thesis: verum

for C being Subset of (n -BinaryVectSp) st 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 ) ) ) & C c= rng A holds

( Lin C is Subspace of n -BinaryVectSp & C is Basis of (Lin C) & dim (Lin C) = card C )

let A be FinSequence of n -tuples_on BOOLEAN; :: thesis: for C being Subset of (n -BinaryVectSp) st 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 ) ) ) & C c= rng A holds

( Lin C is Subspace of n -BinaryVectSp & C is Basis of (Lin C) & dim (Lin C) = card C )

let C be Subset of (n -BinaryVectSp); :: thesis: ( 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 ) ) ) & C c= rng A implies ( Lin C is Subspace of n -BinaryVectSp & C is Basis of (Lin C) & dim (Lin C) = card C ) )

assume 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 ) ) ) ) ; :: thesis: ( not C c= rng A or ( Lin C is Subspace of n -BinaryVectSp & C is Basis of (Lin C) & dim (Lin C) = card C ) )

assume A2: C c= rng A ; :: thesis: ( Lin C is Subspace of n -BinaryVectSp & C is Basis of (Lin C) & dim (Lin C) = card C )

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

B is linearly-independent by A1, Th10;

then A3: C is linearly-independent by A2, VECTSP_7:1;

for x being object st x in C holds

x in the carrier of (Lin C) by VECTSP_7:8, STRUCT_0:def 5;

then reconsider C0 = C as Subset of (Lin C) by TARSKI:def 3;

Lin C0 = ModuleStr(# the carrier of (Lin C), the addF of (Lin C), the ZeroF of (Lin C), the lmult of (Lin C) #) by VECTSP_9:17;

then C0 is Basis of (Lin C) by VECTSP_7:def 3, A3, VECTSP_9:12;

hence ( Lin C is Subspace of n -BinaryVectSp & C is Basis of (Lin C) & dim (Lin C) = card C ) by VECTSP_9:def 1; :: thesis: verum