let B be Basis of (VecSp (E,F)); :: thesis: not B is empty
A: Lin B = ModuleStr(# the carrier of (VecSp (E,F)), the addF of (VecSp (E,F)), the ZeroF of (VecSp (E,F)), the lmult of (VecSp (E,F)) #) by VECTSP_7:def 3;

now :: thesis: not B = {}

assume B = {} ; :: thesis: contradiction
then B = {} the carrier of (VecSp (E,F)) ;
then Lin B = (0). (VecSp (E,F)) by VECTSP_7:9;
then the carrier of (VecSp (E,F)) = {(0. (VecSp (E,F)))} by A, VECTSP_4:def 3;
then the carrier of E = {(0. E)} by FIELD_4:def 6;
hence contradiction ; :: thesis: verum

end;

hence not B is empty ; :: thesis: verum