set V = the VectSp of F;
the carrier of ((0). the VectSp of F) = {(0. the VectSp of F)} by VECTSP_4:def 3
.= {(0. ((0). the VectSp of F))} by VECTSP_4:def 2 ;
hence ex b₁ being VectSp of F st b₁ is trivial ; :: thesis: verum