let F be Field; :: thesis: for n being Nat holds dim (F ^* n) = n
let n be Nat; :: thesis: dim (F ^* n) = n
dim (Lin (Base (F,n))) = card (Base (F,n)) by VECTSP_9:26
.= n by cardB ;
hence dim (F ^* n) = n by lemspan; :: thesis: verum