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