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);
len (1. (K,n)) = n by MATRIX_0:24;
then A1: dom (1. (K,n)) = Seg n by FINSEQ_1:def 3;
then A2: (1. (K,n)) .: (Seg n) = lines (1. (K,n)) by RELAT_1:113;
the_rank_of (1. (K,n)) = n by Lm8;
then 1. (K,n) is without_repeated_line by Th105;
then Seg n,(1. (K,n)) .: (Seg n) are_equipotent by A1, CARD_1:33;
then card (Seg n) = card (lines (1. (K,n))) by A2, CARD_1:5;
then A3: card (lines (1. (K,n))) = n by FINSEQ_1:57;
lines (1. (K,n)) is Basis of (n -VectSp_over K) by Lm8;
hence dim (n -VectSp_over K) = n by A3, VECTSP_9:def 1; :: thesis: verum