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