let F, G be non trivial RealBanachSpace; :: thesis:
set E1 = R_NormSpace_of_BoundedLinearOperators (F,G);
set F1 = R_NormSpace_of_BoundedLinearOperators (G,F);
set G1 = R_NormSpace_of_BoundedLinearOperators (F,F);
A1: R_NormSpace_of_BoundedLinearOperators (F,F) is non trivial RealBanachSpace by Th64;
set A1 = InvertibleOperators (F,G);
set B1 = InvertibleOperators (G,F);
consider g1 being PartFunc of (R_NormSpace_of_BoundedLinearOperators (F,G)),(R_NormSpace_of_BoundedLinearOperators (G,F)) such that
A2: ( dom g1 = InvertibleOperators (F,G) & rng g1 = InvertibleOperators (G,F) & g1 is one-to-one & g1 is_continuous_on InvertibleOperators (F,G) & ex J being PartFunc of (R_NormSpace_of_BoundedLinearOperators (G,F)),(R_NormSpace_of_BoundedLinearOperators (F,G)) st
( J = g1 " & J is one-to-one & dom J = InvertibleOperators (G,F) & rng J = InvertibleOperators (F,G) & J is_continuous_on InvertibleOperators (G,F) ) & ( for u being Point of (R_NormSpace_of_BoundedLinearOperators (F,G)) st u in InvertibleOperators (F,G) holds
g1 . u = Inv u ) ) by LOPBAN13:25;
take g1 ; :: thesis:
thus ( dom g1 = InvertibleOperators (F,G) & rng g1 = InvertibleOperators (G,F) & g1 is one-to-one & g1 is_continuous_on InvertibleOperators (F,G) & ex J being PartFunc of (R_NormSpace_of_BoundedLinearOperators (G,F)),(R_NormSpace_of_BoundedLinearOperators (F,G)) st
( J = g1 " & J is one-to-one & dom J = InvertibleOperators (G,F) & rng J = InvertibleOperators (F,G) & J is_continuous_on InvertibleOperators (G,F) ) & ( for u being Point of (R_NormSpace_of_BoundedLinearOperators (F,G)) st u in InvertibleOperators (F,G) holds
g1 . u = Inv u ) ) by A2; :: thesis:
let i be Nat; :: thesis:
reconsider Z0 = [:(InvertibleOperators (F,G)),(InvertibleOperators (G,F)):] as Subset of [:(R_NormSpace_of_BoundedLinearOperators (F,G)),(R_NormSpace_of_BoundedLinearOperators (G,F)):] by ZFMISC_1:96;
set Z1 = [#] [:(R_NormSpace_of_BoundedLinearOperators (F,G)),(R_NormSpace_of_BoundedLinearOperators (G,F)):];
reconsider Z1 = [#] [:(R_NormSpace_of_BoundedLinearOperators (F,G)),(R_NormSpace_of_BoundedLinearOperators (G,F)):] as non empty Subset of [:(R_NormSpace_of_BoundedLinearOperators (F,G)),(R_NormSpace_of_BoundedLinearOperators (G,F)):] ;
A3: ( [:(InvertibleOperators (F,G)),(InvertibleOperators (G,F)):] c= Z1 & Z1 is open ) by ZFMISC_1:96;
reconsider a = id ([#] F) as Lipschitzian LinearOperator of F,F by LOPBAN_2:3;
reconsider a = a as Point of (R_NormSpace_of_BoundedLinearOperators (F,F)) by LOPBAN_1:def 9;
consider f0 being Lipschitzian BilinearOperator of (R_NormSpace_of_BoundedLinearOperators (F,G)),(R_NormSpace_of_BoundedLinearOperators (G,F)),(R_NormSpace_of_BoundedLinearOperators (F,F)) such that
A4: for u being Point of (R_NormSpace_of_BoundedLinearOperators (F,G))
for v being Point of (R_NormSpace_of_BoundedLinearOperators (G,F)) holds f0 . (u,v) = v * u by Th38;
reconsider f1 = f0 | Z1 as PartFunc of [:(R_NormSpace_of_BoundedLinearOperators (F,G)),(R_NormSpace_of_BoundedLinearOperators (G,F)):],(R_NormSpace_of_BoundedLinearOperators (F,F)) ;
A5: dom f1 = Z1 by FUNCT_2:def 1;
A6: dom f0 = [#] [:(R_NormSpace_of_BoundedLinearOperators (F,G)),(R_NormSpace_of_BoundedLinearOperators (G,F)):] by FUNCT_2:def 1;
for k being Nat st k <= (i + 1) - 1 holds
diff (f0,k,([#] [:(R_NormSpace_of_BoundedLinearOperators (F,G)),(R_NormSpace_of_BoundedLinearOperators (G,F)):])) is_differentiable_on [#] [:(R_NormSpace_of_BoundedLinearOperators (F,G)),(R_NormSpace_of_BoundedLinearOperators (G,F)):] by NDIFF12:21;
then A7: f1 is_differentiable_on i + 1,Z1 by A6, NDIFF_6:14;
A8: diff (f1,(i + 1),Z1) is_continuous_on Z1 by NDIFF_1:45, NDIFF12:21;
A9: for x being Point of (R_NormSpace_of_BoundedLinearOperators (F,G)) st x in InvertibleOperators (F,G) holds
f1 . (x,(g1 . x)) = a

proof

let x be Point of (R_NormSpace_of_BoundedLinearOperators (F,G)); :: thesis:
assume A10: x in InvertibleOperators (F,G) ; :: thesis:
then g1 . x in rng g1 by A2, FUNCT_1:3;
then reconsider g1x = g1 . x as Point of (R_NormSpace_of_BoundedLinearOperators (G,F)) ;
x in { v where v is Point of (R_NormSpace_of_BoundedLinearOperators (F,G)) : v is invertible } by A10, LOPBAN13:def 3;
then A11: ex v being Point of (R_NormSpace_of_BoundedLinearOperators (F,G)) st
( x = v & v is invertible ) ;
thus f1 . (x,(g1 . x)) = g1x * x by A4
.= (Inv x) * x by A2, A10
.= id F by A11, LOPBAN13:22
.= a ; :: thesis:

end;

A12: for x being Point of (R_NormSpace_of_BoundedLinearOperators (F,G))
for z being Point of [:(R_NormSpace_of_BoundedLinearOperators (F,G)),(R_NormSpace_of_BoundedLinearOperators (G,F)):] st x in InvertibleOperators (F,G) & z = [x,(g1 . x)] holds
for y being Point of (R_NormSpace_of_BoundedLinearOperators (G,F)) holds (partdiff`2 (f1,z)) . y = y * x

proof

let x be Point of (R_NormSpace_of_BoundedLinearOperators (F,G)); :: thesis:
let z be Point of [:(R_NormSpace_of_BoundedLinearOperators (F,G)),(R_NormSpace_of_BoundedLinearOperators (G,F)):]; :: thesis:
assume A13: ( x in InvertibleOperators (F,G) & z = [x,(g1 . x)] ) ; :: thesis:
A14: partdiff`2 (f1,z) = f0 * (reproj2 z) by NDIFF12:4;
thus for y being Point of (R_NormSpace_of_BoundedLinearOperators (G,F)) holds (partdiff`2 (f1,z)) . y = y * x :: thesis:

proof

let y be Point of (R_NormSpace_of_BoundedLinearOperators (G,F)); :: thesis:
A15: (reproj2 z) . y = [(z `1),y] by NDIFF_7:def 2
.= [x,y] by A13 ;
A16: dom (reproj2 z) = the carrier of (R_NormSpace_of_BoundedLinearOperators (G,F)) by FUNCT_2:def 1;
thus (partdiff`2 (f1,z)) . y = f0 . [x,y] by A14, A15, A16, FUNCT_1:13
.= f0 . (x,y) by BINOP_1:def 1
.= y * x by A4 ; :: thesis:

end;

end;

A17: for x being Point of (R_NormSpace_of_BoundedLinearOperators (F,G))
for z being Point of [:(R_NormSpace_of_BoundedLinearOperators (F,G)),(R_NormSpace_of_BoundedLinearOperators (G,F)):] st x in InvertibleOperators (F,G) & z = [x,(g1 . x)] holds
partdiff`2 (f1,z) is invertible

proof

let x be Point of (R_NormSpace_of_BoundedLinearOperators (F,G)); :: thesis:
let z be Point of [:(R_NormSpace_of_BoundedLinearOperators (F,G)),(R_NormSpace_of_BoundedLinearOperators (G,F)):]; :: thesis:
assume A18: ( x in InvertibleOperators (F,G) & z = [x,(g1 . x)] ) ; :: thesis:
then A19: for y being Point of (R_NormSpace_of_BoundedLinearOperators (G,F)) holds (partdiff`2 (f1,z)) . y = y * x by A12;
x in { v where v is Point of (R_NormSpace_of_BoundedLinearOperators (F,G)) : v is invertible } by A18, LOPBAN13:def 3;
then ex v being Point of (R_NormSpace_of_BoundedLinearOperators (F,G)) st
( x = v & v is invertible ) ;
hence partdiff`2 (f1,z) is invertible by A19, Th63; :: thesis:

end;

thus ( g1 is_differentiable_on i + 1, InvertibleOperators (F,G) & diff (g1,(i + 1),(InvertibleOperators (F,G))) is_continuous_on InvertibleOperators (F,G) ) :: thesis:

proof

per cases ;

suppose A20: InvertibleOperators (F,G) = {} ; :: thesis:

then A21: InvertibleOperators (F,G) c= dom g1 by XBOOLE_1:2;
for k being Nat st k <= (i + 1) - 1 holds
diff (g1,k,(InvertibleOperators (F,G))) is_differentiable_on InvertibleOperators (F,G) by A20, XBOOLE_1:2;
hence g1 is_differentiable_on i + 1, InvertibleOperators (F,G) by A21, NDIFF_6:14; :: thesis:
A22: for x0 being Point of (R_NormSpace_of_BoundedLinearOperators (F,G)) st x0 in InvertibleOperators (F,G) holds
(diff (g1,(i + 1),(InvertibleOperators (F,G)))) | (InvertibleOperators (F,G)) is_continuous_in x0 by A20;
InvertibleOperators (F,G) c= dom (diff (g1,(i + 1),(InvertibleOperators (F,G)))) by A20, XBOOLE_1:2;
hence diff (g1,(i + 1),(InvertibleOperators (F,G))) is_continuous_on InvertibleOperators (F,G) by A22, NFCONT_1:def 7; :: thesis:

end;

suppose A23: InvertibleOperators (F,G) <> {} ; :: thesis:

per cases ;

suppose A24: R_NormSpace_of_BoundedLinearOperators (G,F) is trivial ; :: thesis:

for x being object st x in [#] (R_NormSpace_of_BoundedLinearOperators (G,F)) holds
x in {(0. (R_NormSpace_of_BoundedLinearOperators (G,F)))}

proof

let x be object ; :: thesis:
assume x in [#] (R_NormSpace_of_BoundedLinearOperators (G,F)) ; :: thesis:
then x = 0. (R_NormSpace_of_BoundedLinearOperators (G,F)) by A24, ZFMISC_1:def 10;
hence x in {(0. (R_NormSpace_of_BoundedLinearOperators (G,F)))} by TARSKI:def 1; :: thesis:

end;

then A25: [#] (R_NormSpace_of_BoundedLinearOperators (G,F)) = {(0. (R_NormSpace_of_BoundedLinearOperators (G,F)))} by ZFMISC_1:31, TARSKI:def 3;
consider x being object such that
A26: x in InvertibleOperators (F,G) by A23, XBOOLE_0:def 1;
reconsider x = x as Point of (R_NormSpace_of_BoundedLinearOperators (F,G)) by A26;
g1 . x in rng g1 by A2, A26, FUNCT_1:3;
then reconsider z = [x,(g1 . x)] as Point of [:(R_NormSpace_of_BoundedLinearOperators (F,G)),(R_NormSpace_of_BoundedLinearOperators (G,F)):] by ZFMISC_1:87;
A27: for y being Point of (R_NormSpace_of_BoundedLinearOperators (G,F)) holds (partdiff`2 (f1,z)) . y = 0. (R_NormSpace_of_BoundedLinearOperators (F,F))

proof

let y be Point of (R_NormSpace_of_BoundedLinearOperators (G,F)); :: thesis:
A28: y = 0. (R_NormSpace_of_BoundedLinearOperators (G,F)) by A25, TARSKI:def 1;
reconsider ff = (partdiff`2 (f1,z)) . y as Lipschitzian LinearOperator of F,F by LOPBAN_1:def 9;
for s being object st s in dom ff holds
ff . s = 0. F

proof

let s be object ; :: thesis:
assume s in dom ff ; :: thesis:
then reconsider s1 = s as Point of F ;
reconsider xx = x as Lipschitzian LinearOperator of F,G by LOPBAN_1:def 9;
A29: dom xx = [#] F by FUNCT_2:def 1;
reconsider Z0 = 0. (R_NormSpace_of_BoundedLinearOperators (G,F)) as Lipschitzian LinearOperator of G,F by LOPBAN_1:def 9;
A30: modetrans ((0. (R_NormSpace_of_BoundedLinearOperators (G,F))),G,F) = Z0 by LOPBAN_1:def 11;
((partdiff`2 (f1,z)) . y) . s1 = ((0. (R_NormSpace_of_BoundedLinearOperators (G,F))) * x) . s1 by A12, A26, A28
.= (Z0 * xx) . s1 by A30, LOPBAN_1:def 11
.= Z0 . (xx . s1) by A29, FUNCT_1:13
.= (([#] G) --> (0. F)) . (xx . s1) by LOPBAN_1:31
.= 0. F by FUNCOP_1:7 ;
hence ff . s = 0. F ; :: thesis:

end;

then ff = (dom ff) --> (0. F) by FUNCOP_1:11;
hence (partdiff`2 (f1,z)) . y = 0. (R_NormSpace_of_BoundedLinearOperators (F,F)) by LOPBAN_1:31; :: thesis:

end;

A31: partdiff`2 (f1,z) is Lipschitzian LinearOperator of (R_NormSpace_of_BoundedLinearOperators (G,F)),(R_NormSpace_of_BoundedLinearOperators (F,F)) by LOPBAN_1:def 9;
ex x being object st
( x in [#] (R_NormSpace_of_BoundedLinearOperators (F,F)) & not x = 0. (R_NormSpace_of_BoundedLinearOperators (F,F)) )

proof

assume A32: for x being object st x in [#] (R_NormSpace_of_BoundedLinearOperators (F,F)) holds
x = 0. (R_NormSpace_of_BoundedLinearOperators (F,F)) ; :: thesis:
for x, y being object st x in [#] (R_NormSpace_of_BoundedLinearOperators (F,F)) & y in [#] (R_NormSpace_of_BoundedLinearOperators (F,F)) holds
x = y

proof

let x, y be object ; :: thesis:
assume ( x in [#] (R_NormSpace_of_BoundedLinearOperators (F,F)) & y in [#] (R_NormSpace_of_BoundedLinearOperators (F,F)) ) ; :: thesis:
then ( x = 0. (R_NormSpace_of_BoundedLinearOperators (F,F)) & y = 0. (R_NormSpace_of_BoundedLinearOperators (F,F)) ) by A32;
hence x = y ; :: thesis:

end;

hence contradiction by A1, ZFMISC_1:def 10; :: thesis:

end;

then consider y being object such that
A33: ( y in [#] (R_NormSpace_of_BoundedLinearOperators (F,F)) & y <> 0. (R_NormSpace_of_BoundedLinearOperators (F,F)) ) ;
not y in rng (partdiff`2 (f1,z))

proof

assume y in rng (partdiff`2 (f1,z)) ; :: thesis:
then consider x being object such that
A34: ( x in dom (partdiff`2 (f1,z)) & y = (partdiff`2 (f1,z)) . x ) by FUNCT_1:def 3;
reconsider x0 = x as Point of (R_NormSpace_of_BoundedLinearOperators (G,F)) by A31, A34, FUNCT_2:def 1;
(partdiff`2 (f1,z)) . x0 = 0. (R_NormSpace_of_BoundedLinearOperators (F,F)) by A27;
hence contradiction by A33, A34; :: thesis:

end;

then not partdiff`2 (f1,z) is invertible by A33, LOPBAN13:def 1;
hence ( g1 is_differentiable_on i + 1, InvertibleOperators (F,G) & diff (g1,(i + 1),(InvertibleOperators (F,G))) is_continuous_on InvertibleOperators (F,G) ) by A17, A26; :: thesis:

end;

suppose not R_NormSpace_of_BoundedLinearOperators (G,F) is trivial ; :: thesis:

hence ( g1 is_differentiable_on i + 1, InvertibleOperators (F,G) & diff (g1,(i + 1),(InvertibleOperators (F,G))) is_continuous_on InvertibleOperators (F,G) ) by A1, A2, A3, A5, A7, A8, A9, A17, Th65; :: thesis:

end;

end;

end;

end;

end;