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_1:25;
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:146;
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:60;
then card (Seg n) = card (lines (1. K,n)) by A2, CARD_1:21;
then A3: card (lines (1. K,n)) = n by FINSEQ_1:78;
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 2; :: thesis: verum