let X, Y be free Z_Module; :: 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 HM1, 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