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

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