let X, Y be RealLinearSpace; :: thesis: for T being LinearOperator of X,Y st T is bijective holds
( T " is LinearOperator of Y,X & rng (T ") = the carrier of X )
let T be LinearOperator of X,Y; :: thesis: ( T is bijective implies ( T " is LinearOperator of Y,X & rng (T ") = the carrier of X ) )
assume A1: T is bijective ; :: thesis: ( T " is LinearOperator of Y,X & rng (T ") = the carrier of X )
A2: rng T = the carrier of Y by A1, FUNCT_2:def 3;
A3: dom T = the carrier of X by FUNCT_2:def 1;
T " is LinearOperator of Y,X

proof

reconsider T1 = T " as Function of Y,X by A1, A2, FUNCT_2:25;
A4: T1 is additive

proof

let y1, y2 be Point of Y; :: according to VECTSP_1:def 19 :: thesis: T1 . (y1 + y2) = (T1 . y1) + (T1 . y2)
consider x1, x2 being Point of X such that
A5: ( T1 . y1 = x1 & T1 . y2 = x2 ) ;
A6: ( T . x1 = y1 & T . x2 = y2 ) by A5, A1, A2, FUNCT_1:32;
x1 + x2 = T1 . (T . (x1 + x2)) by A1, FUNCT_1:32, A3
.= T1 . (y1 + y2) by A6, VECTSP_1:def 20 ;
hence T1 . (y1 + y2) = (T1 . y1) + (T1 . y2) by A5; :: thesis: verum

end;

T1 is homogeneous

proof

let y1 be Point of Y; :: according to LOPBAN_1:def 5 :: thesis: for b₁ being object holds T1 . (b₁ * y1) = b₁ * (T1 . y1)
let r be Real; :: thesis: T1 . (r * y1) = r * (T1 . y1)
set x1 = T1 . y1;
r * (T1 . y1) = T1 . (T . (r * (T1 . y1))) by A1, FUNCT_1:32, A3
.= T1 . (r * (T . (T1 . y1))) by LOPBAN_1:def 5
.= T1 . (r * y1) by A1, A2, FUNCT_1:32 ;
hence T1 . (r * y1) = r * (T1 . y1) ; :: thesis: verum

end;

hence T " is LinearOperator of Y,X by A4; :: thesis: verum

end;

hence ( T " is LinearOperator of Y,X & rng (T ") = the carrier of X ) by A1, FUNCT_1:33, A3; :: thesis: verum