let E, G, F be RealNormSpace; :: thesis:
let Z be Subset of [:E,F:]; :: thesis:
let f be PartFunc of [:E,F:],G; :: thesis:
let z be Point of [:E,F:]; :: thesis:
assume A1: f is_differentiable_in z ; :: thesis:
reconsider y = (IsoCPNrSP (E,F)) . z as Point of (product <*E,F*>) ;
((IsoCPNrSP (E,F)) ") . ((IsoCPNrSP (E,F)) . z) = z by FUNCT_2:26;
then A3: f * ((IsoCPNrSP (E,F)) ") is_differentiable_in y by A1, NDIFF_7:28;
then A4: ( f is_partial_differentiable_in`1 z & f is_partial_differentiable_in`2 z ) by NDIFF_5:41, NDIFF_7:34;
consider N being Neighbourhood of z such that
A5: ( N c= dom f & ex R being RestFunc of [:E,F:],G st
for w being Point of [:E,F:] st w in N holds
(f /. w) - (f /. z) = ((diff (f,z)) . (w - z)) + (R /. (w - z)) ) by A1, NDIFF_1:def 7;
consider R being RestFunc of [:E,F:],G such that
A6: for w being Point of [:E,F:] st w in N holds
(f /. w) - (f /. z) = ((diff (f,z)) . (w - z)) + (R /. (w - z)) by A5;
reconsider L = diff (f,z) as Lipschitzian LinearOperator of [:E,F:],G by LOPBAN_1:def 9;
consider L1 being Lipschitzian LinearOperator of E,G, L2 being Lipschitzian LinearOperator of F,G such that
A7: for dx being Point of E
for dy being Point of F holds L . [dx,dy] = (L1 . dx) + (L2 . dy) and
for dx being Point of E holds L1 . dx = L /. [dx,(0. F)] and
for dy being Point of F holds L2 . dy = L /. [(0. E),dy] by Th2;
reconsider LL1 = L1 as Point of (R_NormSpace_of_BoundedLinearOperators (E,G)) by LOPBAN_1:def 9;
reconsider LL2 = L2 as Point of (R_NormSpace_of_BoundedLinearOperators (F,G)) by LOPBAN_1:def 9;
set g1 = f * (reproj1 z);
set g2 = f * (reproj2 z);
reconsider x = z `1 as Point of E ;
reconsider y = z `2 as Point of F ;
A9: ex x1 being Point of E ex x2 being Point of F st z = [x1,x2] by PRVECT_3:18;
then A10: z = [x,y] ;
consider r0 being Real such that
A14: ( 0 < r0 & { y where y is Point of [:E,F:] : ||.(y - z).|| < r0 } c= N ) by NFCONT_1:def 1;
A15: { y where y is Point of [:E,F:] : ||.(y - z).|| < r0 } = Ball (z,r0) by NDIFF_8:17;
consider r being Real such that
A16: ( 0 < r & r < r0 & [:(Ball (x,r)),(Ball (y,r)):] c= Ball (z,r0) ) by A9, A14, NDIFF_8:22;
A17: [:(Ball (x,r)),(Ball (y,r)):] c= N by A14, A15, A16, XBOOLE_1:1;
deffunc H₁( Point of E) -> Element of the carrier of G = R /. [$1,(0. F)];
consider R1 being Function of the carrier of E, the carrier of G such that
A18: for p being Point of E holds R1 . p = H₁(p) from FUNCT_2:sch 4();
A20: for dx being Point of E holds R1 /. dx = R /. [dx,(0. F)] by A18;
deffunc H₂( Point of F) -> Element of the carrier of G = R /. [(0. E),$1];
consider R2 being Function of the carrier of F, the carrier of G such that
A21: for p being Point of F holds R2 . p = H₂(p) from FUNCT_2:sch 4();
A23: for dy being Point of F holds R2 /. dy = R /. [(0. E),dy] by A21;
for r being Real st r > 0 holds
ex d being Real st
( d > 0 & ( for z being Point of E st z <> 0. E & ||.z.|| < d holds
(||.z.|| ") * ||.(R1 /. z).|| < r ) )

let r be Real; :: thesis:
assume A25: r > 0 ; :: thesis:
R is total by NDIFF_1:def 5;
then consider d being Real such that
A26: ( d > 0 & ( for z being Point of [:E,F:] st z <> 0. [:E,F:] & ||.z.|| < d holds
(||.z.|| ") * ||.(R /. z).|| < r ) ) by A25, NDIFF_1:23;
take d ; :: thesis:
thus d > 0 by A26; :: thesis:
let x1 be Point of E; :: thesis:
assume A27: ( x1 <> 0. E & ||.x1.|| < d ) ; :: thesis:
reconsider z = [x1,(0. F)] as Point of [:E,F:] ;
A28: z <> 0. [:E,F:] by A27, XTUPLE_0:1;
A29: R /. z = R1 /. x1 by A18;
||.z.|| = ||.x1.|| by NDIFF_8:2;
hence (||.x1.|| ") * ||.(R1 /. x1).|| < r by A26, A27, A28, A29; :: thesis:

end;

then reconsider R1 = R1 as RestFunc of E,G by NDIFF_1:23;
for r being Real st r > 0 holds
ex d being Real st
( d > 0 & ( for z being Point of F st z <> 0. F & ||.z.|| < d holds
(||.z.|| ") * ||.(R2 /. z).|| < r ) )

proof

let r be Real; :: thesis:
assume A32: r > 0 ; :: thesis:
R is total by NDIFF_1:def 5;
then consider d being Real such that
A33: ( d > 0 & ( for z being Point of [:E,F:] st z <> 0. [:E,F:] & ||.z.|| < d holds
(||.z.|| ") * ||.(R /. z).|| < r ) ) by A32, NDIFF_1:23;
take d ; :: thesis:
thus d > 0 by A33; :: thesis:
let y1 be Point of F; :: thesis:
assume A34: ( y1 <> 0. F & ||.y1.|| < d ) ; :: thesis:
reconsider z = [(0. E),y1] as Point of [:E,F:] ;
A35: z <> 0. [:E,F:] by A34, XTUPLE_0:1;
A36: R /. z = R2 /. y1 by A21;
||.z.|| = ||.y1.|| by NDIFF_8:3;
hence (||.y1.|| ") * ||.(R2 /. y1).|| < r by A33, A34, A35, A36; :: thesis:

end;

then reconsider R2 = R2 as RestFunc of F,G by NDIFF_1:23;
reconsider N1 = Ball (x,r) as Neighbourhood of x by A16, NDIFF_8:19;
reconsider N2 = Ball (y,r) as Neighbourhood of y by A16, NDIFF_8:19;
A37: N1 c= dom (f * (reproj1 z))

proof

let s be object ; :: according to TARSKI:def 3 :: thesis:
assume A39: s in N1 ; :: thesis:
then reconsider t = s as Point of E ;
A40: dom (reproj1 z) = the carrier of E by FUNCT_2:def 1;
A41: (reproj1 z) . t = [t,y] by NDIFF_7:def 1;
( t in Ball (x,r) & y in Ball (y,r) ) by A16, A39, NDIFF_8:13;
then [t,y] in [:(Ball (x,r)),(Ball (y,r)):] by ZFMISC_1:87;
then (reproj1 z) . t in N by A17, A41;
hence s in dom (f * (reproj1 z)) by A5, A40, FUNCT_1:11; :: thesis:

end;

B42: N2 c= dom (f * (reproj2 z))

proof

let s be object ; :: according to TARSKI:def 3 :: thesis:
assume A43: s in N2 ; :: thesis:
then reconsider t = s as Point of F ;
A44: dom (reproj2 z) = the carrier of F by FUNCT_2:def 1;
A45: (reproj2 z) . t = [x,t] by NDIFF_7:def 2;
( t in Ball (y,r) & x in Ball (x,r) ) by A16, A43, NDIFF_8:13;
then [x,t] in [:(Ball (x,r)),(Ball (y,r)):] by ZFMISC_1:87;
then (reproj2 z) . t in N by A17, A45;
hence s in dom (f * (reproj2 z)) by A5, A44, FUNCT_1:11; :: thesis:

end;

for x1 being Point of E st x1 in N1 holds
((f * (reproj1 z)) /. x1) - ((f * (reproj1 z)) /. x) = (LL1 . (x1 - x)) + (R1 /. (x1 - x))

proof

let x1 be Point of E; :: thesis:
assume A48: x1 in N1 ; :: thesis:
then A50: (reproj1 z) . x1 in dom f by A37, FUNCT_1:11;
A51: (reproj1 z) . x1 = [x1,y] by NDIFF_7:def 1;
( x1 in Ball (x,r) & y in Ball (y,r) ) by A16, A48, NDIFF_8:13;
then A52: [x1,y] in [:(Ball (x,r)),(Ball (y,r)):] by ZFMISC_1:87;
A53: x in N1 by A16, NDIFF_8:13;
then A54: (reproj1 z) . x in dom f by A37, FUNCT_1:11;
- z = [(- x),(- y)] by A9, PRVECT_3:18;
then A56: ((reproj1 z) . x1) - z = [(x1 - x),(y - y)] by A51, PRVECT_3:18
.= [(x1 - x),(0. F)] by RLVECT_1:15 ;
A57: (f * (reproj1 z)) /. x1 = (f * (reproj1 z)) . x1 by A37, A48, PARTFUN1:def 6
.= f . ((reproj1 z) . x1) by A37, A48, FUNCT_1:12
.= f /. ((reproj1 z) . x1) by A50, PARTFUN1:def 6 ;
(f * (reproj1 z)) /. x = (f * (reproj1 z)) . x by A37, A53, PARTFUN1:def 6
.= f . ((reproj1 z) . x) by A37, A53, FUNCT_1:12
.= f /. ((reproj1 z) . x) by A54, PARTFUN1:def 6
.= f /. z by A10, NDIFF_7:def 1 ;
hence ((f * (reproj1 z)) /. x1) - ((f * (reproj1 z)) /. x) = ((diff (f,z)) . (((reproj1 z) . x1) - z)) + (R /. (((reproj1 z) . x1) - z)) by A6, A17, A51, A52, A57
.= ((L1 . (x1 - x)) + (L2 . (0. F))) + (R /. [(x1 - x),(0. F)]) by A7, A56
.= ((L1 . (x1 - x)) + (0. G)) + (R /. [(x1 - x),(0. F)]) by LOPBAN_7:3
.= (L1 . (x1 - x)) + (R /. [(x1 - x),(0. F)]) by RLVECT_1:4
.= (LL1 . (x1 - x)) + (R1 /. (x1 - x)) by A20 ;
:: thesis:

end;

then A59: LL1 = partdiff`1 (f,z) by A4, A37, NDIFF_1:def 7;
for y1 being Point of F st y1 in N2 holds
((f * (reproj2 z)) /. y1) - ((f * (reproj2 z)) /. y) = (LL2 . (y1 - y)) + (R2 /. (y1 - y))

proof

let y1 be Point of F; :: thesis:
assume A61: y1 in N2 ; :: thesis:
then A63: (reproj2 z) . y1 in dom f by B42, FUNCT_1:11;
A64: (reproj2 z) . y1 = [x,y1] by NDIFF_7:def 2;
( x in Ball (x,r) & y1 in Ball (y,r) ) by A16, A61, NDIFF_8:13;
then A65: [x,y1] in [:(Ball (x,r)),(Ball (y,r)):] by ZFMISC_1:87;
A66: y in N2 by A16, NDIFF_8:13;
then A67: (reproj2 z) . y in dom f by B42, FUNCT_1:11;
- z = [(- x),(- y)] by A9, PRVECT_3:18;
then A69: ((reproj2 z) . y1) - z = [(x - x),(y1 - y)] by A64, PRVECT_3:18
.= [(0. E),(y1 - y)] by RLVECT_1:15 ;
A70: (f * (reproj2 z)) /. y1 = (f * (reproj2 z)) . y1 by B42, A61, PARTFUN1:def 6
.= f . ((reproj2 z) . y1) by B42, A61, FUNCT_1:12
.= f /. ((reproj2 z) . y1) by A63, PARTFUN1:def 6 ;
(f * (reproj2 z)) /. y = (f * (reproj2 z)) . y by B42, A66, PARTFUN1:def 6
.= f . ((reproj2 z) . y) by B42, A66, FUNCT_1:12
.= f /. ((reproj2 z) . y) by A67, PARTFUN1:def 6
.= f /. z by A10, NDIFF_7:def 2 ;
hence ((f * (reproj2 z)) /. y1) - ((f * (reproj2 z)) /. y) = ((diff (f,z)) . (((reproj2 z) . y1) - z)) + (R /. (((reproj2 z) . y1) - z)) by A6, A17, A64, A65, A70
.= ((L1 . (0. E)) + (L2 . (y1 - y))) + (R /. [(0. E),(y1 - y)]) by A7, A69
.= ((0. G) + (L2 . (y1 - y))) + (R /. [(0. E),(y1 - y)]) by LOPBAN_7:3
.= (L2 . (y1 - y)) + (R /. [(0. E),(y1 - y)]) by RLVECT_1:4
.= (LL2 . (y1 - y)) + (R2 /. (y1 - y)) by A23 ;
:: thesis:

end;

then LL2 = partdiff`2 (f,z) by A4, B42, NDIFF_1:def 7;
hence ( f is_partial_differentiable_in`1 z & f is_partial_differentiable_in`2 z & ( for dx being Point of E
for dy being Point of F holds (diff (f,z)) . [dx,dy] = ((partdiff`1 (f,z)) . dx) + ((partdiff`2 (f,z)) . dy) ) ) by A3, A7, A59, NDIFF_5:41, NDIFF_7:34; :: thesis: