let n be non zero Element of NAT ; :: thesis: ( n -BinaryVectSp is finite-dimensional & dim (n -BinaryVectSp) = n )

set V = n -BinaryVectSp ;

consider B being finite Subset of (n -BinaryVectSp) such that

A1: ( 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 Th13;

thus n -BinaryVectSp is finite-dimensional by A1, MATRLIN:def 1; :: thesis: dim (n -BinaryVectSp) = n

hence dim (n -BinaryVectSp) = n by A1, VECTSP_9:def 1; :: thesis: verum

set V = n -BinaryVectSp ;

consider B being finite Subset of (n -BinaryVectSp) such that

A1: ( 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 Th13;

thus n -BinaryVectSp is finite-dimensional by A1, MATRLIN:def 1; :: thesis: dim (n -BinaryVectSp) = n

hence dim (n -BinaryVectSp) = n by A1, VECTSP_9:def 1; :: thesis: verum