let F be Field; :: thesis: for X, Y being VectSp of F

for T being linear-transformation of X,Y st T is bijective holds

( X is finite-dimensional iff Y is finite-dimensional )

let X, Y be VectSp of F; :: thesis: for T being linear-transformation of X,Y st T is bijective holds

( X is finite-dimensional iff Y is finite-dimensional )

let T be linear-transformation of X,Y; :: thesis: ( T is bijective implies ( X is finite-dimensional iff Y is finite-dimensional ) )

assume AS1: T is bijective ; :: thesis: ( X is finite-dimensional iff Y is finite-dimensional )

consider K being linear-transformation of Y,X such that

AS3: ( K = T " & K is bijective ) by ZMODUL06:42, AS1;

thus ( X is finite-dimensional iff Y is finite-dimensional ) by HM13, AS1, AS3; :: thesis: verum

for T being linear-transformation of X,Y st T is bijective holds

( X is finite-dimensional iff Y is finite-dimensional )

let X, Y be VectSp of F; :: thesis: for T being linear-transformation of X,Y st T is bijective holds

( X is finite-dimensional iff Y is finite-dimensional )

let T be linear-transformation of X,Y; :: thesis: ( T is bijective implies ( X is finite-dimensional iff Y is finite-dimensional ) )

assume AS1: T is bijective ; :: thesis: ( X is finite-dimensional iff Y is finite-dimensional )

consider K being linear-transformation of Y,X such that

AS3: ( K = T " & K is bijective ) by ZMODUL06:42, AS1;

thus ( X is finite-dimensional iff Y is finite-dimensional ) by HM13, AS1, AS3; :: thesis: verum