let F be Field; :: thesis: for X, Y being VectSp of F
for T being linear-transformation of X,Y st T is bijective & X is finite-dimensional holds
Y is finite-dimensional
let X, Y be VectSp of F; :: thesis: for T being linear-transformation of X,Y st T is bijective & X is finite-dimensional holds
Y is finite-dimensional
let L be linear-transformation of X,Y; :: thesis: ( L is bijective & X is finite-dimensional implies Y is finite-dimensional )
assume AS1: L is bijective ; :: thesis: ( not X is finite-dimensional or Y is finite-dimensional )
assume X is finite-dimensional ; :: thesis: Y is finite-dimensional
then consider A being finite Subset of X such that
P1: A is Basis of X ;
L .: A is Basis of Y by P1, HM12, AS1;
hence Y is finite-dimensional ; :: thesis: verum