let X, Y be RealLinearSpace; :: thesis: for L being LinearOperator of X,Y st L is bijective holds
ex K being LinearOperator of Y,X st
( K = L " & K is one-to-one & K is onto )
let L be LinearOperator of X,Y; :: thesis: ( L is bijective implies ex K being LinearOperator of Y,X st
( K = L " & K is one-to-one & K is onto ) )
assume A1: L is bijective ; :: thesis: ex K being LinearOperator of Y,X st
( K = L " & K is one-to-one & K is onto )
then A2: rng L = the carrier of Y by FUNCT_2:def 3;
then reconsider K = L " as Function of the carrier of Y, the carrier of X by A1, FUNCT_2:25;
A3: dom L = the carrier of X by FUNCT_2:def 1;
A4: 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
A5: x = L . a by A2, FUNCT_2:113;
consider b being Element of X such that
A6: y = L . b by A2, FUNCT_2:113;
A7: K . x = a by A1, A3, A5, FUNCT_1:34;
A8: K . y = b by A1, A3, A6, FUNCT_1:34;
x + y = L . (a + b) by A5, A6, VECTSP_1:def 20;
hence K . (x + y) = (K . x) + (K . y) by A1, A3, A7, A8, FUNCT_1:34; :: thesis: verum

end;

for x being VECTOR of Y
for r being Real holds K . (r * x) = r * (K . x)

proof

let x be VECTOR of Y; :: thesis: for r being Real holds K . (r * x) = r * (K . x)
let r be Real; :: thesis: K . (r * x) = r * (K . x)
consider a being VECTOR of X such that
A9: x = L . a by A2, FUNCT_2:113;
A10: K . x = a by A1, A3, A9, FUNCT_1:34;
r * x = L . (r * a) by A9, LOPBAN_1:def 5;
hence K . (r * x) = r * (K . x) by A1, A3, A10, FUNCT_1:34; :: thesis: verum

end;

then reconsider K = K as LinearOperator of Y,X by A4, LOPBAN_1:def 5;
take K ; :: thesis: ( K = L " & K is one-to-one & K is onto )
rng K = the carrier of X by A1, A3, FUNCT_1:33;
hence ( K = L " & K is one-to-one & K is onto ) by A1, FUNCT_2:def 3; :: thesis: verum