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

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