let X, Y be free Z_Module; 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; 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; ( L is bijective implies ( A is Basis of X iff L .: A is Basis of Y ) )
assume AS1:
L is bijective
; ( 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; ( L .: A is Basis of Y implies A is Basis of X )
assume
L .: A is Basis of Y
; 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; verum