let E be RealNormSpace; :: thesis:
let G, F be non trivial RealBanachSpace; :: thesis:
let Z be Subset of [:E,F:]; :: thesis:
let f be PartFunc of [:E,F:],G; :: thesis:
let c be Point of G; :: thesis:
let A be Subset of E; :: thesis:
let B be Subset of F; :: thesis:
let g be PartFunc of E,F; :: thesis:
assume A1: ( Z is open & dom f = Z & A is open & B is open & [:A,B:] c= Z & f is_differentiable_on Z & f `| Z is_continuous_on Z & dom g = A & rng g c= B & g is_continuous_on A & ( for x being Point of E st x in A holds
f . (x,(g . x)) = c ) & ( for x being Point of E
for z being Point of [:E,F:] st x in A & z = [x,(g . x)] holds
partdiff`2 (f,z) is invertible ) ) ; :: thesis:
then A2: ( f is_partial_differentiable_on`1 Z & f is_partial_differentiable_on`2 Z & f `partial`1| Z is_continuous_on Z & f `partial`2| Z is_continuous_on Z ) by NDIFF_7:52;
A3: for x being Point of E
for z being Point of [:E,F:] st x in A & z = [x,(g . x)] holds
( g is_differentiable_in x & diff (g,x) = - ((Inv (partdiff`2 (f,z))) * (partdiff`1 (f,z))) )

proof

let a be Point of E; :: thesis:
let z be Point of [:E,F:]; :: thesis:
assume A4: ( a in A & z = [a,(g . a)] ) ; :: thesis:
then A5: g . a in rng g by A1, FUNCT_1:def 3;
then reconsider b = g . a as Point of F ;
A6: f . (a,b) = c by A1, A4;
z in [:A,B:] by A1, A4, A5, ZFMISC_1:87;
then A9: f is_differentiable_in z by A1, NDIFF_1:31;
A10: g | A is_continuous_in a by A1, A4, NFCONT_1:def 7;
A11: g | A = g by A1, RELAT_1:68;
partdiff`2 (f,z) is invertible by A1, A4;
hence ( g is_differentiable_in a & diff (g,a) = - ((Inv (partdiff`2 (f,z))) * (partdiff`1 (f,z))) ) by A1, A4, A6, A9, A10, A11, Th45; :: thesis:

end;

for x being Point of E st x in A holds
g is_differentiable_in x

proof

let x be Point of E; :: thesis:
assume A13: x in A ; :: thesis:
then g . x in rng g by A1, FUNCT_1:def 3;
then reconsider y = g . x as Point of F ;
[x,y] = [x,(g . x)] ;
hence g is_differentiable_in x by A3, A13; :: thesis:

end;

proof

end;

A39: for x being Point of E st x in A holds
( x in dom ((f `partial`1| Z) * xg) & (f `partial`1| Z) * xg is_continuous_in x )

proof

let x be Point of E; :: thesis:
assume A40: x in A ; :: thesis:
then A41: g . x in rng g by A1, FUNCT_1:def 3;
[x,(g . x)] is set by TARSKI:1;
then reconsider z = [x,(g . x)] as Point of [:E,F:] by A41, PRVECT_3:18;
A44: z in [:A,B:] by A1, A40, A41, ZFMISC_1:87;
A46: ( xg . x = [x,(g . x)] & xg . x = xg /. x ) by A17, A40, PARTFUN1:def 6;
hence A47: x in dom ((f `partial`1| Z) * xg) by A1, A17, A40, A21, A44, FUNCT_1:11; :: thesis:
xg | A is_continuous_in x by A18, A40, NFCONT_1:def 7;
then A48: xg is_continuous_in x by A17, RELAT_1:69;
(f `partial`1| Z) | Z is_continuous_in xg /. x by A1, A2, A44, A46, NFCONT_1:def 7;
then f `partial`1| Z is_continuous_in xg /. x by A21, RELAT_1:69;
hence (f `partial`1| Z) * xg is_continuous_in x by A47, A48, NFCONT112; :: thesis:

end;

A49: for x being Point of E st x in A holds
( x in dom ((I * (f `partial`2| Z)) * xg) & (I * (f `partial`2| Z)) * xg is_continuous_in x )

proof

let x be Point of E; :: thesis:
assume A50: x in A ; :: thesis:
then A51: g . x in rng g by A1, FUNCT_1:def 3;
[x,(g . x)] is set by TARSKI:1;
then reconsider z = [x,(g . x)] as Point of [:E,F:] by A51, PRVECT_3:18;
A54: z in [:A,B:] by A1, A50, A51, ZFMISC_1:87;
A56: ( xg . x = [x,(g . x)] & xg . x = xg /. x ) by A17, A50, PARTFUN1:def 6;
xg | A is_continuous_in x by A18, A50, NFCONT_1:def 7;
then A58: xg is_continuous_in x by A17, RELAT_1:69;
(f `partial`2| Z) | Z is_continuous_in xg /. x by A1, A2, A54, A56, NFCONT_1:def 7;
then A61: f `partial`2| Z is_continuous_in xg /. x by A22, RELAT_1:69;
A62: partdiff`2 (f,(xg /. x)) is invertible by A1, A50, A56;
then A63: partdiff`2 (f,(xg /. x)) in InvertibleOperators (F,G) ;
A64: partdiff`2 (f,(xg /. x)) in dom I by A20, A62;
A65: (f `partial`2| Z) /. (xg /. x) = partdiff`2 (f,(xg /. x)) by A1, A2, A54, A56, NDIFF_7:def 11;
then (f `partial`2| Z) . (xg /. x) in dom I by A1, A22, A54, A56, A64, PARTFUN1:def 6;
then A68: xg /. x in dom (I * (f `partial`2| Z)) by A1, A22, A54, A56, FUNCT_1:11;
hence A70: x in dom ((I * (f `partial`2| Z)) * xg) by A17, A50, A56, FUNCT_1:11; :: thesis:
I | (InvertibleOperators (F,G)) is_continuous_in (f `partial`2| Z) /. (xg /. x) by A20, A63, A65, NFCONT_1:def 7;
then I is_continuous_in (f `partial`2| Z) /. (xg /. x) by A20, RELAT_1:69;
then I * (f `partial`2| Z) is_continuous_in xg /. x by A61, A68, NFCONT112;
hence (I * (f `partial`2| Z)) * xg is_continuous_in x by A58, A70, NFCONT112; :: thesis:

end;

for x being object st x in A holds
x in dom ((f `partial`1| Z) * xg) by A39;
then A72: A c= dom ((f `partial`1| Z) * xg) by TARSKI:def 3;
for x being object st x in A holds
x in dom ((I * (f `partial`2| Z)) * xg) by A49;
then A74: A c= dom ((I * (f `partial`2| Z)) * xg) by TARSKI:def 3;
A75: for x being Point of E st x in A holds
(f `partial`1| Z) * xg is_continuous_in x by A39;
for x being Point of E st x in A holds
(I * (f `partial`2| Z)) * xg is_continuous_in x by A49;
then consider H being PartFunc of E,(R_NormSpace_of_BoundedLinearOperators (E,F)) such that
A77: ( dom H = A & ( for x being Point of E st x in A holds
H . x = BL . ((((f `partial`1| Z) * xg) . x),(((I * (f `partial`2| Z)) * xg) . x)) ) & H is_continuous_on A ) by A19, A72, A74, A75, LmTh47;
A78: for x0 being Point of E st x0 in A holds
BL . [(((f `partial`1| Z) * xg) . x0),(((I * (f `partial`2| Z)) * xg) . x0)] = BL /. [(((f `partial`1| Z) * xg) . x0),(((I * (f `partial`2| Z)) * xg) . x0)]

proof

let x0 be Point of E; :: thesis:
assume x0 in A ; :: thesis:
then A82: ( ((f `partial`1| Z) * xg) . x0 in rng ((f `partial`1| Z) * xg) & ((I * (f `partial`2| Z)) * xg) . x0 in rng ((I * (f `partial`2| Z)) * xg) ) by A39, A49, FUNCT_1:3;
[(((f `partial`1| Z) * xg) . x0),(((I * (f `partial`2| Z)) * xg) . x0)] is set by TARSKI:1;
then [(((f `partial`1| Z) * xg) . x0),(((I * (f `partial`2| Z)) * xg) . x0)] is Point of [:(R_NormSpace_of_BoundedLinearOperators (E,G)),(R_NormSpace_of_BoundedLinearOperators (G,F)):] by A82, PRVECT_3:18;
then [(((f `partial`1| Z) * xg) . x0),(((I * (f `partial`2| Z)) * xg) . x0)] in the carrier of [:(R_NormSpace_of_BoundedLinearOperators (E,G)),(R_NormSpace_of_BoundedLinearOperators (G,F)):] ;
then [(((f `partial`1| Z) * xg) . x0),(((I * (f `partial`2| Z)) * xg) . x0)] in dom BL by FUNCT_2:def 1;
hence BL . [(((f `partial`1| Z) * xg) . x0),(((I * (f `partial`2| Z)) * xg) . x0)] = BL /. [(((f `partial`1| Z) * xg) . x0),(((I * (f `partial`2| Z)) * xg) . x0)] by PARTFUN1:def 6; :: thesis:

end;

for x0 being Point of E st x0 in A holds
(g `| A) | A is_continuous_in x0

proof

let x0 be Point of E; :: thesis:
assume A83: x0 in A ; :: thesis:
then A85: x0 in dom ((g `| A) | A) by A16, RELAT_1:69;
set F = (g `| A) | A;
for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Point of E st x1 in dom ((g `| A) | A) & ||.(x1 - x0).|| < s holds
||.((((g `| A) | A) /. x1) - (((g `| A) | A) /. x0)).|| < r ) )

proof

let r be Real; :: thesis:
assume 0 < r ; :: thesis:
then consider s being Real such that
A88: ( 0 < s & ( for x1 being Point of E st x1 in A & ||.(x1 - x0).|| < s holds
||.((H /. x1) - (H /. x0)).|| < r ) ) by A77, A83, NFCONT_1:19;
take s ; :: thesis:
thus 0 < s by A88; :: thesis:
let x1 be Point of E; :: thesis:
assume A89: ( x1 in dom ((g `| A) | A) & ||.(x1 - x0).|| < s ) ; :: thesis:
then A90: x1 in A by A16, RELAT_1:69;
then A91: ||.((H /. x1) - (H /. x0)).|| < r by A88, A89;
A92: H /. x1 = H . x1 by A77, A90, PARTFUN1:def 6
.= BL . ((((f `partial`1| Z) * xg) . x1),(((I * (f `partial`2| Z)) * xg) . x1)) by A77, A90
.= BL /. [(((f `partial`1| Z) * xg) . x1),(((I * (f `partial`2| Z)) * xg) . x1)] by A78, A90 ;
A93: ((g `| A) | A) /. x1 = (g `| A) /. x1 by A16, RELAT_1:69
.= - (H /. x1) by A23, A90, A92 ;
A94: H /. x0 = H . x0 by A77, A83, PARTFUN1:def 6
.= BL . ((((f `partial`1| Z) * xg) . x0),(((I * (f `partial`2| Z)) * xg) . x0)) by A77, A83
.= BL /. [(((f `partial`1| Z) * xg) . x0),(((I * (f `partial`2| Z)) * xg) . x0)] by A78, A83 ;
((g `| A) | A) /. x0 = (g `| A) /. x0 by A16, RELAT_1:69
.= - (H /. x0) by A23, A83, A94 ;
then (((g `| A) | A) /. x1) - (((g `| A) | A) /. x0) = (- (H /. x1)) + (H /. x0) by A93, RLVECT_1:17
.= - ((H /. x1) - (H /. x0)) by RLVECT_1:33 ;
hence ||.((((g `| A) | A) /. x1) - (((g `| A) | A) /. x0)).|| < r by A91, NORMSP_1:2; :: thesis:

end;

hence (g `| A) | A is_continuous_in x0 by A85, NFCONT_1:7; :: thesis:

end;

hence g `| A is_continuous_on A by A16, NFCONT_1:def 7; :: thesis:
thus for x being Point of E
for z being Point of [:E,F:] st x in A & z = [x,(g . x)] holds
diff (g,x) = - ((Inv (partdiff`2 (f,z))) * (partdiff`1 (f,z))) by A3; :: thesis: