let F be Field; :: thesis: 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 )
let X be finite-dimensional VectSp of F; :: thesis: 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 )
let Y be VectSp of F; :: thesis: for T being linear-transformation of X,Y st T is bijective holds
( Y is finite-dimensional & dim X = dim Y )
let T be linear-transformation of X,Y; :: thesis: ( T is bijective implies ( Y is finite-dimensional & dim X = dim Y ) )
assume AS1: T is bijective ; :: thesis: ( Y is finite-dimensional & dim X = dim Y )
hence X1: Y is finite-dimensional by HM151; :: thesis: dim X = dim Y
for I being Basis of X holds dim Y = card I

proof

let I be Basis of X; :: thesis: dim Y = card I
dom T = the carrier of X by FUNCT_2:def 1;
then X12: card I = card (T .: I) by CARD_1:5, AS1, CARD_1:33;
T .: I is Basis of Y by AS1, HM12;
hence dim Y = card I by X1, X12, VECTSP_9:def 1; :: thesis: verum

end;

hence dim X = dim Y by VECTSP_9:def 1; :: thesis: verum