theorem DimF: :: VECTSP13:28

for F being Field
for n being Nat holds dim (F ^* n) = n