let V be Subspace of n -BinaryVectSp ; :: thesis: V is finite

the carrier of V c= the carrier of (n -BinaryVectSp) by VECTSP_4:def 2;

hence V is finite ; :: thesis: verum

the carrier of V c= the carrier of (n -BinaryVectSp) by VECTSP_4:def 2;

hence V is finite ; :: thesis: verum