theorem :: MATRIX13:112

for n being Nat
for K being Field holds dim (n -VectSp_over K) = n