let X, Y be non trivial RealBanachSpace; :: thesis: ex I being Function of (InvertibleOperators (X,Y)),(InvertibleOperators (Y,X)) st
( I is one-to-one & I is onto & ( for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st u in InvertibleOperators (X,Y) holds
I . u = Inv u ) )
set S = R_NormSpace_of_BoundedLinearOperators (X,Y);
defpred S₁[ object , object ] means ex u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st
( $1 = u & $2 = Inv u );
A1: for x being object st x in InvertibleOperators (X,Y) holds
ex y being object st
( y in InvertibleOperators (Y,X) & S₁[x,y] )

proof

let x be object ; :: thesis: ( x in InvertibleOperators (X,Y) implies ex y being object st
( y in InvertibleOperators (Y,X) & S₁[x,y] ) )
assume x in InvertibleOperators (X,Y) ; :: thesis: ex y being object st
( y in InvertibleOperators (Y,X) & S₁[x,y] )
then consider u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) such that
A2: ( x = u & u is invertible ) ;
take y = Inv u; :: thesis: ( y in InvertibleOperators (Y,X) & S₁[x,y] )
y is invertible by A2, LM60;
hence y in InvertibleOperators (Y,X) ; :: thesis: S₁[x,y]
thus S₁[x,y] by A2; :: thesis: verum

end;

consider I being Function of (InvertibleOperators (X,Y)),(InvertibleOperators (Y,X)) such that
A3: for x being object st x in InvertibleOperators (X,Y) holds
S₁[x,I . x] from FUNCT_2:sch 1(A1);
take I ; :: thesis: ( I is one-to-one & I is onto & ( for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st u in InvertibleOperators (X,Y) holds
I . u = Inv u ) )
A4: for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st u in InvertibleOperators (X,Y) holds
I . u = Inv u

proof

let u be Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)); :: thesis: ( u in InvertibleOperators (X,Y) implies I . u = Inv u )
assume u in InvertibleOperators (X,Y) ; :: thesis: I . u = Inv u
then S₁[u,I . u] by A3;
hence I . u = Inv u ; :: thesis: verum

end;

A5: ( InvertibleOperators (X,Y) <> {} implies InvertibleOperators (Y,X) <> {} )

proof

assume InvertibleOperators (X,Y) <> {} ; :: thesis: InvertibleOperators (Y,X) <> {}
then consider x being object such that
A6: x in InvertibleOperators (X,Y) by XBOOLE_0:def 1;
consider u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) such that
A7: ( x = u & u is invertible ) by A6;
Inv u is invertible by A7, LM60;
then Inv u in InvertibleOperators (Y,X) ;
hence InvertibleOperators (Y,X) <> {} ; :: thesis: verum

end;

B7: for x1, x2 being object st x1 in InvertibleOperators (X,Y) & x2 in InvertibleOperators (X,Y) & I . x1 = I . x2 holds
x1 = x2

proof

let x1, x2 be object ; :: thesis: ( x1 in InvertibleOperators (X,Y) & x2 in InvertibleOperators (X,Y) & I . x1 = I . x2 implies x1 = x2 )
assume that
A8: ( x1 in InvertibleOperators (X,Y) & x2 in InvertibleOperators (X,Y) ) and
A9: I . x1 = I . x2 ; :: thesis: x1 = x2
reconsider u1 = x1, u2 = x2 as Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) by A8;
A10: ( ex v1 being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st
( u1 = v1 & v1 is invertible ) & ex v2 being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st
( u2 = v2 & v2 is invertible ) ) by A8;
A11: I . u1 = Inv u1 by A4, A8;
u1 = Inv (Inv u1) by A10, LM60
.= Inv (Inv u2) by A4, A8, A9, A11
.= u2 by A10, LM60 ;
hence x1 = x2 ; :: thesis: verum

end;

now :: thesis: for y being object st y in InvertibleOperators (Y,X) holds
y in rng I

let y be object ; :: thesis: ( y in InvertibleOperators (Y,X) implies y in rng I )
assume y in InvertibleOperators (Y,X) ; :: thesis: y in rng I
then consider v being Point of (R_NormSpace_of_BoundedLinearOperators (Y,X)) such that
A15: ( y = v & v is invertible ) ;
Inv v is invertible by A15, LM60;
then A16: Inv v in InvertibleOperators (X,Y) ;
Inv (Inv v) = v by A15, LM60;
then y = I . (Inv v) by A4, A15, A16;
hence y in rng I by A5, A16, FUNCT_2:4; :: thesis: verum

end;

then InvertibleOperators (Y,X) c= rng I by TARSKI:def 3;
hence ( I is one-to-one & I is onto & ( for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st u in InvertibleOperators (X,Y) holds
I . u = Inv u ) ) by A4, A5, B7, FUNCT_2:19, XBOOLE_0:def 10; :: thesis: verum