let R be Ring; :: thesis: for X, Y being LeftMod of R
for T being linear-transformation of X,Y st T is bijective holds
( X is free iff Y is free )
let X, Y be LeftMod of R; :: thesis: for T being linear-transformation of X,Y st T is bijective holds
( X is free iff Y is free )
let T be linear-transformation of X,Y; :: thesis: ( T is bijective implies ( X is free iff Y is free ) )
assume AS1: T is bijective ; :: thesis: ( X is free iff Y is free )
consider K being linear-transformation of Y,X such that
AS3: ( K = T " & K is bijective ) by HM1, AS1;
thus ( X is free iff Y is free ) by HM9, AS1, AS3; :: thesis: verum