let R be Ring; :: thesis: for X, Y being LeftMod of R
for L being linear-transformation of X,Y st L is bijective holds
ex K being linear-transformation of Y,X st
( K = L " & K is bijective )
let X, Y be LeftMod of R; :: thesis: for L being linear-transformation of X,Y st L is bijective holds
ex K being linear-transformation of Y,X st
( K = L " & K is bijective )
let L be linear-transformation of X,Y; :: thesis: ( L is bijective implies ex K being linear-transformation of Y,X st
( K = L " & K is bijective ) )
assume A1: L is bijective ; :: thesis: ex K being linear-transformation of Y,X st
( K = L " & K is bijective )
then P2: rng L = the carrier of Y by FUNCT_2:def 3;
then reconsider K = L " as Function of Y,X by A1, FUNCT_2:25;
D0: dom L = the carrier of X by FUNCT_2:def 1;
B0: K is additive

proof

let x, y be Element of Y; :: according to VECTSP_1:def 19 :: thesis: K . (x + y) = (K . x) + (K . y)
consider a being Element of X such that
B01: x = L . a by P2, FUNCT_2:113;
consider b being Element of X such that
B02: y = L . b by P2, FUNCT_2:113;
B03: K . x = a by A1, FUNCT_1:34, D0, B01;
B04: K . y = b by A1, FUNCT_1:34, D0, B02;
x + y = L . (a + b) by VECTSP_1:def 20, B01, B02;
hence K . (x + y) = (K . x) + (K . y) by B03, B04, A1, FUNCT_1:34, D0; :: thesis: verum

end;

for r being Element of R
for x being Element of Y holds K . (r * x) = r * (K . x)

proof

let r be Element of R; :: thesis: for x being Element of Y holds K . (r * x) = r * (K . x)
let x be Element of Y; :: thesis: K . (r * x) = r * (K . x)
consider a being Element of X such that
B01: x = L . a by P2, FUNCT_2:113;
B03: K . x = a by A1, FUNCT_1:34, D0, B01;
r * x = L . (r * a) by MOD_2:def 2, B01;
hence K . (r * x) = r * (K . x) by B03, A1, FUNCT_1:34, D0; :: thesis: verum

end;

then reconsider K = K as linear-transformation of Y,X by B0, MOD_2:def 2;
take K ; :: thesis: ( K = L " & K is bijective )
rng K = the carrier of X by D0, FUNCT_1:33, A1;
then K is onto by FUNCT_2:def 3;
hence ( K = L " & K is bijective ) by A1; :: thesis: verum