let I be Basis of V; :: thesis: not I is empty
assume I is empty ; :: thesis: contradiction
then I = {} the carrier of V ;
then Lin I = (0). V by ZMODUL02:67;
then (Omega). V = (0). V by VECTSP_7:def 3;
hence contradiction ; :: thesis: verum