let V be finite-dimensional RealLinearSpace; :: thesis: for W being RealLinearSpace st ex T being LinearOperator of V,W st T is bijective holds
( W is finite-dimensional & dim W = dim V )
let W be RealLinearSpace; :: thesis: ( ex T being LinearOperator of V,W st T is bijective implies ( W is finite-dimensional & dim W = dim V ) )
given T being LinearOperator of V,W such that A1: T is bijective ; :: thesis: ( W is finite-dimensional & dim W = dim V )
consider A being finite Subset of V such that
A2: A is Basis of V by RLVECT_5:def 1;
A3: dom T = the carrier of V by FUNCT_2:def 1;
A4: T .: A is Basis of W by A1, A2, Th87;
hence W is finite-dimensional by RLVECT_5:def 1; :: thesis: dim W = dim V
hence dim W = card (T .: A) by A4, RLVECT_5:def 2
.= card A by A1, A3, CARD_1:5, CARD_1:33
.= dim V by A2, RLVECT_5:def 2 ;
:: thesis: verum