let S, T be RealLinearSpace; :: thesis: for I being LinearOperator of S,T st I is bijective holds
ex J being LinearOperator of T,S st
( J = I " & J is bijective )
let I be LinearOperator of S,T; :: thesis: ( I is bijective implies ex J being LinearOperator of T,S st
( J = I " & J is bijective ) )
assume A1: I is bijective ; :: thesis: ex J being LinearOperator of T,S st
( J = I " & J is bijective )
then a1: ( I is one-to-one & I is onto ) ;
then A2: ( rng I = the carrier of T & dom I = the carrier of S ) by FUNCT_2:def 1;
A3: ( rng I = dom (I ") & dom I = rng (I ") ) by A1, FUNCT_1:33;
then reconsider J = I " as Function of T,S by A2, FUNCT_2:1;
A4: for v, w being Point of T holds J . (v + w) = (J . v) + (J . w)

proof

let v, w be Point of T; :: thesis: J . (v + w) = (J . v) + (J . w)
consider t being Point of S such that
A5: v = I . t by FUNCT_2:113, a1;
consider s being Point of S such that
A6: w = I . s by FUNCT_2:113, a1;
A7: J . (v + w) = J . (I . (t + s)) by A5, A6, VECTSP_1:def 20
.= t + s by A1, A2, FUNCT_1:34 ;
J . w = s by A1, A2, A6, FUNCT_1:34;
hence J . (v + w) = (J . v) + (J . w) by A1, A2, A5, A7, FUNCT_1:34; :: thesis: verum

end;

for v being Point of T
for r being Real holds J . (r * v) = r * (J . v)

proof

let v be Point of T; :: thesis: for r being Real holds J . (r * v) = r * (J . v)
let r be Real; :: thesis: J . (r * v) = r * (J . v)
consider t being Point of S such that
A9: v = I . t by FUNCT_2:113, a1;
J . (r * v) = J . (I . (r * t)) by A9, LOPBAN_1:def 5
.= r * t by A1, A2, FUNCT_1:34 ;
hence J . (r * v) = r * (J . v) by A1, A2, A9, FUNCT_1:34; :: thesis: verum

end;

then reconsider J = J as LinearOperator of T,S by A4, LOPBAN_1:def 5, VECTSP_1:def 20;
take J ; :: thesis: ( J = I " & J is bijective )
thus J = I " ; :: thesis: J is bijective
( J is one-to-one & J is onto ) by A1, A3, FUNCT_2:def 1;
hence J is bijective ; :: thesis: verum