let F be Field; :: thesis: for U being finite-dimensional VectSp of F holds U,F ^* (dim U) are_isomorphic
let U be finite-dimensional VectSp of F; :: thesis: U,F ^* (dim U) are_isomorphic
dim (F ^* (dim U)) = dim U by DimF;
hence U,F ^* (dim U) are_isomorphic by UisoV; :: thesis: verum