let n be Nat; :: thesis: for K being Field holds dim (n -VectSp_over K) = n
let K be Field; :: thesis: dim (n -VectSp_over K) = n
set ONE = 1. K,n;
A1: ( lines (1. K,n) is Basis of n -VectSp_over K & the_rank_of (1. K,n) = n & len (1. K,n) = n ) by Lm8, MATRIX_1:25;
then ( 1. K,n is without_repeated_line & dom (1. K,n) = Seg n ) by Th105, FINSEQ_1:def 3;
then ( Seg n,(1. K,n) .: (Seg n) are_equipotent & (1. K,n) .: (Seg n) = lines (1. K,n) ) by CARD_1:60, RELAT_1:146;
then card (Seg n) = card (lines (1. K,n)) by CARD_1:21;
then card (lines (1. K,n)) = n by FINSEQ_1:78;
hence dim (n -VectSp_over K) = n by A1, VECTSP_9:def 2; :: thesis: verum