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 ;
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 ;
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 ;
x1 + x2 = T1 . (T . (x1 + x2)) by
.= T1 . (y1 + y2) by ;
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 b1 being object holds T1 . (b1 * y1) = b1 * (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
.= T1 . (r * (T . (T1 . y1))) by LOPBAN_1:def 5
.= T1 . (r * y1) by ;
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 ; :: thesis: verum