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

for T being linear-transformation of X,Y

for A being Subset of X st T is bijective holds

( A is Basis of X iff T .: A is Basis of Y )

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

for A being Subset of X st T is bijective holds

( A is Basis of X iff T .: A is Basis of Y )

let L be linear-transformation of X,Y; :: thesis: for A being Subset of X st L is bijective holds

( A is Basis of X iff L .: A is Basis of Y )

let A be Subset of X; :: thesis: ( L is bijective implies ( A is Basis of X iff L .: A is Basis of Y ) )

assume AS1: L is bijective ; :: thesis: ( A is Basis of X iff L .: A is Basis of Y )

D1: dom L = the carrier of X by FUNCT_2:def 1;

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

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

thus ( A is Basis of X implies L .: A is Basis of Y ) by AS1, HM11; :: thesis: ( L .: A is Basis of Y implies A is Basis of X )

assume L .: A is Basis of Y ; :: thesis: A is Basis of X

then K .: (L .: A) is Basis of X by AS3, HM11;

hence A is Basis of X by D1, AS1, AS3, FUNCT_1:107; :: thesis: verum

for T being linear-transformation of X,Y

for A being Subset of X st T is bijective holds

( A is Basis of X iff T .: A is Basis of Y )

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

for A being Subset of X st T is bijective holds

( A is Basis of X iff T .: A is Basis of Y )

let L be linear-transformation of X,Y; :: thesis: for A being Subset of X st L is bijective holds

( A is Basis of X iff L .: A is Basis of Y )

let A be Subset of X; :: thesis: ( L is bijective implies ( A is Basis of X iff L .: A is Basis of Y ) )

assume AS1: L is bijective ; :: thesis: ( A is Basis of X iff L .: A is Basis of Y )

D1: dom L = the carrier of X by FUNCT_2:def 1;

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

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

thus ( A is Basis of X implies L .: A is Basis of Y ) by AS1, HM11; :: thesis: ( L .: A is Basis of Y implies A is Basis of X )

assume L .: A is Basis of Y ; :: thesis: A is Basis of X

then K .: (L .: A) is Basis of X by AS3, HM11;

hence A is Basis of X by D1, AS1, AS3, FUNCT_1:107; :: thesis: verum