theorem Th27: :: LOPBAN15:25

for X being finite-dimensional RealLinearSpace holds
( product <*X*> is finite-dimensional & dim (product <*X*>) = dim X )