theorem HM15: :: VECTSP12:4

for F being Field
for X being finite-dimensional VectSp of F
for Y being VectSp of F
for T being linear-transformation of X,Y st T is bijective holds
( Y is finite-dimensional & dim X = dim Y )