let E, F, G be RealNormSpace; :: thesis:
let x be Point of (R_NormSpace_of_BoundedLinearOperators (E,F)); :: thesis:
let L be Point of (R_NormSpace_of_BoundedLinearOperators ((R_NormSpace_of_BoundedLinearOperators (F,E)),(R_NormSpace_of_BoundedLinearOperators (E,E)))); :: thesis:
assume that
A1: x is invertible and
A2: for y being Point of (R_NormSpace_of_BoundedLinearOperators (F,E)) holds L . y = y * x ; :: thesis:
set EF = R_NormSpace_of_BoundedLinearOperators (E,F);
set FE = R_NormSpace_of_BoundedLinearOperators (F,E);
set EE = R_NormSpace_of_BoundedLinearOperators (E,E);
set FEEE = R_NormSpace_of_BoundedLinearOperators ((R_NormSpace_of_BoundedLinearOperators (F,E)),(R_NormSpace_of_BoundedLinearOperators (E,E)));
reconsider L1 = L as Lipschitzian LinearOperator of (R_NormSpace_of_BoundedLinearOperators (F,E)),(R_NormSpace_of_BoundedLinearOperators (E,E)) by LOPBAN_1:def 9;
reconsider x0 = x as Lipschitzian LinearOperator of E,F by LOPBAN_1:def 9;
A3: modetrans (x,E,F) = x0 by LOPBAN_1:def 11;
A4: ( x is one-to-one & rng x = [#] F & x " is Point of (R_NormSpace_of_BoundedLinearOperators (F,E)) ) by A1, LOPBAN13:def 1;
reconsider dx = x " as Point of (R_NormSpace_of_BoundedLinearOperators (F,E)) by A1, LOPBAN13:def 1;
reconsider dx0 = dx as Lipschitzian LinearOperator of F,E by LOPBAN_1:def 9;
A5: modetrans (dx,F,E) = dx0 by LOPBAN_1:def 11;
A6: for x1, x2 being object st x1 in [#] (R_NormSpace_of_BoundedLinearOperators (F,E)) & x2 in [#] (R_NormSpace_of_BoundedLinearOperators (F,E)) & L1 . x1 = L1 . x2 holds
x1 = x2

proof

let z1, z2 be object ; :: thesis:
assume A7: ( z1 in [#] (R_NormSpace_of_BoundedLinearOperators (F,E)) & z2 in [#] (R_NormSpace_of_BoundedLinearOperators (F,E)) & L1 . z1 = L1 . z2 ) ; :: thesis:
reconsider z10 = z1, z20 = z2 as Point of (R_NormSpace_of_BoundedLinearOperators (F,E)) by A7;
A8: L1 . z20 = z20 * x by A2;
reconsider z100 = z10 as Lipschitzian LinearOperator of F,E by LOPBAN_1:def 9;
reconsider z200 = z20 as Lipschitzian LinearOperator of F,E by LOPBAN_1:def 9;
A9: modetrans (z10,F,E) = z100 by LOPBAN_1:def 11;
A10: modetrans (z20,F,E) = z200 by LOPBAN_1:def 11;
A11: z100 * x0 = z10 * x by A9, LOPBAN_1:def 11
.= z20 * x by A2, A7, A8
.= z200 * x0 by A10, LOPBAN_1:def 11 ;
z100 = z100 * (id ([#] F)) by FUNCT_2:17
.= z100 * (x0 * (x0 ")) by A4, FUNCT_2:29
.= (z100 * x0) * (x0 ") by RELAT_1:36
.= z200 * (x0 * (x0 ")) by A11, RELAT_1:36
.= z200 * (id ([#] F)) by A4, FUNCT_2:29
.= z200 by FUNCT_2:17 ;
hence z1 = z2 ; :: thesis:

end;

then A12: L is one-to-one by FUNCT_2:19;
for y being object st y in [#] (R_NormSpace_of_BoundedLinearOperators (E,E)) holds
ex z being object st
( z in [#] (R_NormSpace_of_BoundedLinearOperators (F,E)) & y = L1 . z )

proof

let y be object ; :: thesis:
assume y in [#] (R_NormSpace_of_BoundedLinearOperators (E,E)) ; :: thesis:
then reconsider y0 = y as Point of (R_NormSpace_of_BoundedLinearOperators (E,E)) ;
reconsider y00 = y0 as Lipschitzian LinearOperator of E,E by LOPBAN_1:def 9;
reconsider ddx = dx * x as Lipschitzian LinearOperator of E,E by LOPBAN_1:def 9;
A13: modetrans ((dx * x),E,E) = ddx by LOPBAN_1:def 11;
A14: ddx = dx0 * x0 by A3, LOPBAN_1:def 11
.= id E by A4, LOPBAN13:11 ;
take z = y0 * dx; :: thesis:
thus z in [#] (R_NormSpace_of_BoundedLinearOperators (F,E)) ; :: thesis:
L1 . z = (y0 * dx) * x by A2
.= y0 * (dx * x) by LOPBAN13:10
.= y00 * (id E) by A13, A14, LOPBAN_1:def 11
.= y by FUNCT_2:17 ;
hence y = L1 . z ; :: thesis:

end;

then A15: rng L1 = [#] (R_NormSpace_of_BoundedLinearOperators (E,E)) by FUNCT_2:10;
then A16: L1 is bijective by A6, FUNCT_2:19, FUNCT_2:def 3;
defpred S₁[ object , object ] means ex y being Point of (R_NormSpace_of_BoundedLinearOperators (E,E)) st
( y = $1 & $2 = y * dx );
A17: for y being object st y in the carrier of (R_NormSpace_of_BoundedLinearOperators (E,E)) holds
ex z being object st
( z in the carrier of (R_NormSpace_of_BoundedLinearOperators (F,E)) & S₁[y,z] )

proof

let y be object ; :: thesis:
assume y in the carrier of (R_NormSpace_of_BoundedLinearOperators (E,E)) ; :: thesis:
then reconsider V1 = y as Point of (R_NormSpace_of_BoundedLinearOperators (E,E)) ;
take z = V1 * dx; :: thesis:
thus ( z in the carrier of (R_NormSpace_of_BoundedLinearOperators (F,E)) & S₁[y,z] ) ; :: thesis:

end;

consider R being Function of the carrier of (R_NormSpace_of_BoundedLinearOperators (E,E)), the carrier of (R_NormSpace_of_BoundedLinearOperators (F,E)) such that
A18: for y being object st y in the carrier of (R_NormSpace_of_BoundedLinearOperators (E,E)) holds
S₁[y,R . y] from FUNCT_2:sch 1(A17);
A19: for y being Point of (R_NormSpace_of_BoundedLinearOperators (E,E)) holds R . y = y * dx

proof

let y be Point of (R_NormSpace_of_BoundedLinearOperators (E,E)); :: thesis:
ex V being Point of (R_NormSpace_of_BoundedLinearOperators (E,E)) st
( V = y & R . y = V * dx ) by A18;
hence R . y = y * dx ; :: thesis:

end;

for y being Element of (R_NormSpace_of_BoundedLinearOperators (F,E)) holds (R * L1) . y = y

proof

let y0 be Element of (R_NormSpace_of_BoundedLinearOperators (F,E)); :: thesis:
reconsider y00 = y0 as Lipschitzian LinearOperator of F,E by LOPBAN_1:def 9;
A20: modetrans (y0,F,E) = y00 by LOPBAN_1:def 11;
reconsider xdx = x * dx as Lipschitzian LinearOperator of F,F by LOPBAN_1:def 9;
A21: xdx = x0 * dx0 by A5, LOPBAN_1:def 11
.= id F by A4, LOPBAN13:11 ;
thus (R * L1) . y0 = R . (L1 . y0) by FUNCT_2:15
.= R . (y0 * x) by A2
.= (y0 * x) * dx by A19
.= y0 * (x * dx) by LOPBAN13:10
.= y00 * (id F) by A20, A21, LOPBAN_1:def 11
.= y0 by FUNCT_2:17 ; :: thesis:

end;

then A22: R * L1 = id ([#] (R_NormSpace_of_BoundedLinearOperators (F,E))) ;
then R = L " by A12, A15, FUNCT_2:30;
then reconsider R = R as LinearOperator of (R_NormSpace_of_BoundedLinearOperators (E,E)),(R_NormSpace_of_BoundedLinearOperators (F,E)) by A16, LOPBAN_7:1;
set K = ||.dx.||;
for y being VECTOR of (R_NormSpace_of_BoundedLinearOperators (E,E)) holds ||.(R . y).|| <= ||.dx.|| * ||.y.||

proof

let y be VECTOR of (R_NormSpace_of_BoundedLinearOperators (E,E)); :: thesis:
reconsider y0 = y as Lipschitzian LinearOperator of E,E by LOPBAN_1:def 9;
A23: modetrans (y,E,E) = y0 by LOPBAN_1:def 11;
||.(y * dx).|| <= ||.y.|| * ||.dx.|| by A5, A23, LOPBAN_2:2;
hence ||.(R . y).|| <= ||.dx.|| * ||.y.|| by A19; :: thesis:

end;

then reconsider R = R as Lipschitzian LinearOperator of (R_NormSpace_of_BoundedLinearOperators (E,E)),(R_NormSpace_of_BoundedLinearOperators (F,E)) by LOPBAN_1:def 8, NORMSP_1:4;
R = L " by A12, A15, A22, FUNCT_2:30;
then L " is Point of (R_NormSpace_of_BoundedLinearOperators ((R_NormSpace_of_BoundedLinearOperators (E,E)),(R_NormSpace_of_BoundedLinearOperators (F,E)))) by LOPBAN_1:def 9;
hence L is invertible by A12, A15, LOPBAN13:def 1; :: thesis: