let X, Y be RealLinearSpace; :: thesis: for L being LinearOperator of X,Y st L is isomorphism holds
ex K being LinearOperator of Y,X st
( K = L " & K is isomorphism )
let L be LinearOperator of X,Y; :: thesis: ( L is isomorphism implies ex K being LinearOperator of Y,X st
( K = L " & K is isomorphism ) )
assume A1: L is isomorphism ; :: thesis: ex K being LinearOperator of Y,X st
( K = L " & K is isomorphism )
then A2: ( L is one-to-one & L is onto ) ;
reconsider K = L " as Function of Y,X by A2, FUNCT_2:25;
A3: dom L = the carrier of X by FUNCT_2:def 1;
A4: K is additive

proof

let x, y be Point of Y; :: according to VECTSP_1:def 19 :: thesis: K . (x + y) = (K . x) + (K . y)
consider a being Point of X such that
A5: x = L . a by A2, FUNCT_2:113;
consider b being Point 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;

K is homogeneous

proof

let x be Point of Y; :: according to LOPBAN_1:def 5 :: thesis: for b₁ being object holds K . (b₁ * x) = b₁ * (K . x)
let r be Real; :: thesis: K . (r * x) = r * (K . x)
consider a being Point of X such that
A10: x = L . a by A2, FUNCT_2:113;
A11: K . x = a by A1, A3, A10, FUNCT_1:34;
A12: r * x = L . (r * a) by A10, LOPBAN_1:def 5;
thus K . (r * x) = r * (K . x) by A1, A3, A11, A12, FUNCT_1:34; :: thesis: verum

end;

then reconsider K = K as LinearOperator of Y,X by A4;
take K ; :: thesis: ( K = L " & K is isomorphism )
K is onto by A1, A3, FUNCT_1:33;
hence ( K = L " & K is isomorphism ) by A1, FUNCT_1:40; :: thesis: verum