let E, F, G be RealNormSpace; :: thesis:
let f be PartFunc of [:E,F:],G; :: thesis:
let Z be Subset of [:E,F:]; :: thesis:
let z be Point of [:E,F:]; :: thesis:
assume A1: ( Z is open & z in Z & Z c= dom f ) ; :: thesis:
A2: ex x1 being Point of E ex x2 being Point of F st z = [x1,x2] by PRVECT_3:18;
thus ( f is_partial_differentiable_in`1 z implies ( f | Z is_partial_differentiable_in`1 z & partdiff`1 (f,z) = partdiff`1 ((f | Z),z) ) ) :: thesis:

proof

assume A4: f is_partial_differentiable_in`1 z ; :: thesis:
set g = f * (reproj1 z);
consider N being Neighbourhood of z `1 such that
A6: ( N c= dom (f * (reproj1 z)) & ex R being RestFunc of E,G st
for x being Point of E st x in N holds
((f * (reproj1 z)) /. x) - ((f * (reproj1 z)) /. (z `1)) = ((partdiff`1 (f,z)) . (x - (z `1))) + (R /. (x - (z `1))) ) by A4, NDIFF_1:def 7;
consider R being RestFunc of E,G such that
A7: for x being Point of E st x in N holds
((f * (reproj1 z)) /. x) - ((f * (reproj1 z)) /. (z `1)) = ((partdiff`1 (f,z)) . (x - (z `1))) + (R /. (x - (z `1))) by A6;
set h = (f | Z) * (reproj1 z);
A9: (reproj1 z) . (z `1) = [(z `1),(z `2)] by NDIFF_7:def 1
.= z by A2 ;
consider r1 being Real such that
A10: ( r1 > 0 & Ball (z,r1) c= Z ) by A1, NDIFF_8:20;
A11: Ball (z,r1) = { y where y is Point of [:E,F:] : ||.(y - z).|| < r1 } by NDIFF_8:17;
consider r2 being Real such that
A13: ( r2 > 0 & { y where y is Point of E : ||.(y - (z `1)).|| < r2 } c= N ) by NFCONT_1:def 1;
set r = min (r1,r2);
A14: ( 0 < min (r1,r2) & min (r1,r2) <= r1 & min (r1,r2) <= r2 ) by A10, A13, XXREAL_0:15, XXREAL_0:17;
set M = Ball ((z `1),(min (r1,r2)));
A15: Ball ((z `1),(min (r1,r2))) = { y where y is Point of E : ||.(y - (z `1)).|| < min (r1,r2) } by NDIFF_8:17;
then reconsider M = Ball ((z `1),(min (r1,r2))) as Neighbourhood of z `1 by A14, NFCONT_1:def 1;
A17: { y where y is Point of E : ||.(y - (z `1)).|| < r2 } = Ball ((z `1),r2) by NDIFF_8:17;
A18: M c= Ball ((z `1),r2) by A14, NDIFF_8:15;
A19: ( M c= N & ( for x being Point of E st x in M holds
(reproj1 z) . x in Z ) )

proof

thus M c= N by A13, A17, A18, XBOOLE_1:1; :: thesis:
let x be Point of E; :: thesis:
assume x in M ; :: thesis:
then A20: ex y being Point of E st
( x = y & ||.(y - (z `1)).|| < min (r1,r2) ) by A15;
A21: (reproj1 z) . x = [x,(z `2)] by NDIFF_7:def 1;
- z = [(- (z `1)),(- (z `2))] by A2, PRVECT_3:18;
then ((reproj1 z) . x) - z = [(x - (z `1)),((z `2) - (z `2))] by A21, PRVECT_3:18
.= [(x - (z `1)),(0. F)] by RLVECT_1:15 ;
then ||.(((reproj1 z) . x) - z).|| = ||.(x - (z `1)).|| by NDIFF_8:2;
then ||.(((reproj1 z) . x) - z).|| < r1 by A14, A20, XXREAL_0:2;
then (reproj1 z) . x in { y where y is Point of [:E,F:] : ||.(y - z).|| < r1 } ;
hence (reproj1 z) . x in Z by A10, A11; :: thesis:

end;

A22: dom (reproj1 z) = the carrier of E by FUNCT_2:def 1;
A23: dom (f | Z) = Z by A1, RELAT_1:62;
A24: M c= dom ((f | Z) * (reproj1 z))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A25: x in M ; :: thesis:
then (reproj1 z) . x in Z by A19;
hence x in dom ((f | Z) * (reproj1 z)) by A22, A23, A25, FUNCT_1:11; :: thesis:

end;

A27: for x being Point of E st x in M holds
(((f | Z) * (reproj1 z)) /. x) - (((f | Z) * (reproj1 z)) /. (z `1)) = ((partdiff`1 (f,z)) . (x - (z `1))) + (R /. (x - (z `1)))

proof

let x be Point of E; :: thesis:
assume A28: x in M ; :: thesis:
then A29: x in N by A19;
A30: z `1 in N by NFCONT_1:4;
A31: z `1 in M by NFCONT_1:4;
A33: ((f | Z) * (reproj1 z)) /. x = ((f | Z) * (reproj1 z)) . x by A24, A28, PARTFUN1:def 6
.= (f | Z) . ((reproj1 z) . x) by A22, FUNCT_1:13
.= f . ((reproj1 z) . x) by A19, A28, FUNCT_1:49
.= (f * (reproj1 z)) . x by A22, FUNCT_1:13
.= (f * (reproj1 z)) /. x by A6, A29, PARTFUN1:def 6 ;
((f | Z) * (reproj1 z)) /. (z `1) = ((f | Z) * (reproj1 z)) . (z `1) by A24, A31, PARTFUN1:def 6
.= (f | Z) . ((reproj1 z) . (z `1)) by A22, FUNCT_1:13
.= f . ((reproj1 z) . (z `1)) by A1, A9, FUNCT_1:49
.= (f * (reproj1 z)) . (z `1) by A22, FUNCT_1:13
.= (f * (reproj1 z)) /. (z `1) by A6, A30, PARTFUN1:def 6 ;
hence (((f | Z) * (reproj1 z)) /. x) - (((f | Z) * (reproj1 z)) /. (z `1)) = ((partdiff`1 (f,z)) . (x - (z `1))) + (R /. (x - (z `1))) by A7, A19, A28, A33; :: thesis:

end;

then A35: (f | Z) * (reproj1 z) is_differentiable_in z `1 by A24, NDIFF_1:def 6;
thus f | Z is_partial_differentiable_in`1 z by A24, A27, NDIFF_1:def 6; :: thesis:
thus partdiff`1 ((f | Z),z) = partdiff`1 (f,z) by A35, A24, A27, NDIFF_1:def 7; :: thesis:

end;

assume A38: f is_partial_differentiable_in`2 z ; :: thesis:
set g = f * (reproj2 z);
consider N being Neighbourhood of z `2 such that
A40: ( N c= dom (f * (reproj2 z)) & ex R being RestFunc of F,G st
for x being Point of F st x in N holds
((f * (reproj2 z)) /. x) - ((f * (reproj2 z)) /. (z `2)) = ((partdiff`2 (f,z)) . (x - (z `2))) + (R /. (x - (z `2))) ) by A38, NDIFF_1:def 7;
consider R being RestFunc of F,G such that
A41: for x being Point of F st x in N holds
((f * (reproj2 z)) /. x) - ((f * (reproj2 z)) /. (z `2)) = ((partdiff`2 (f,z)) . (x - (z `2))) + (R /. (x - (z `2))) by A40;
set h = (f | Z) * (reproj2 z);
A43: (reproj2 z) . (z `2) = [(z `1),(z `2)] by NDIFF_7:def 2
.= z by A2 ;
consider r1 being Real such that
A44: ( r1 > 0 & Ball (z,r1) c= Z ) by A1, NDIFF_8:20;
A45: Ball (z,r1) = { y where y is Point of [:E,F:] : ||.(y - z).|| < r1 } by NDIFF_8:17;
consider r2 being Real such that
A47: ( r2 > 0 & { y where y is Point of F : ||.(y - (z `2)).|| < r2 } c= N ) by NFCONT_1:def 1;
set r = min (r1,r2);
A48: ( 0 < min (r1,r2) & min (r1,r2) <= r1 & min (r1,r2) <= r2 ) by A44, A47, XXREAL_0:15, XXREAL_0:17;
set M = Ball ((z `2),(min (r1,r2)));
A49: Ball ((z `2),(min (r1,r2))) = { y where y is Point of F : ||.(y - (z `2)).|| < min (r1,r2) } by NDIFF_8:17;
then reconsider M = Ball ((z `2),(min (r1,r2))) as Neighbourhood of z `2 by A48, NFCONT_1:def 1;
A51: { y where y is Point of F : ||.(y - (z `2)).|| < r2 } = Ball ((z `2),r2) by NDIFF_8:17;
A52: M c= Ball ((z `2),r2) by A48, NDIFF_8:15;
A53: ( M c= N & ( for x being Point of F st x in M holds
(reproj2 z) . x in Z ) )

proof

thus M c= N by A47, A51, A52, XBOOLE_1:1; :: thesis:
let x be Point of F; :: thesis:
assume x in M ; :: thesis:
then A54: ex y being Point of F st
( x = y & ||.(y - (z `2)).|| < min (r1,r2) ) by A49;
A55: (reproj2 z) . x = [(z `1),x] by NDIFF_7:def 2;
- z = [(- (z `1)),(- (z `2))] by A2, PRVECT_3:18;
then ((reproj2 z) . x) - z = [((z `1) - (z `1)),(x - (z `2))] by A55, PRVECT_3:18
.= [(0. E),(x - (z `2))] by RLVECT_1:15 ;
then ||.(((reproj2 z) . x) - z).|| = ||.(x - (z `2)).|| by NDIFF_8:3;
then ||.(((reproj2 z) . x) - z).|| < r1 by A48, A54, XXREAL_0:2;
then (reproj2 z) . x in { y where y is Point of [:E,F:] : ||.(y - z).|| < r1 } ;
hence (reproj2 z) . x in Z by A44, A45; :: thesis:

end;

A56: dom (reproj2 z) = the carrier of F by FUNCT_2:def 1;
A57: dom (f | Z) = Z by A1, RELAT_1:62;
A58: M c= dom ((f | Z) * (reproj2 z))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A59: x in M ; :: thesis:
then (reproj2 z) . x in Z by A53;
hence x in dom ((f | Z) * (reproj2 z)) by A56, A57, A59, FUNCT_1:11; :: thesis:

end;

A61: for x being Point of F st x in M holds
(((f | Z) * (reproj2 z)) /. x) - (((f | Z) * (reproj2 z)) /. (z `2)) = ((partdiff`2 (f,z)) . (x - (z `2))) + (R /. (x - (z `2)))

proof

let x be Point of F; :: thesis:
assume A62: x in M ; :: thesis:
then A63: x in N by A53;
A64: z `2 in N by NFCONT_1:4;
A65: z `2 in M by NFCONT_1:4;
A67: ((f | Z) * (reproj2 z)) /. x = ((f | Z) * (reproj2 z)) . x by A58, A62, PARTFUN1:def 6
.= (f | Z) . ((reproj2 z) . x) by A56, FUNCT_1:13
.= f . ((reproj2 z) . x) by A53, A62, FUNCT_1:49
.= (f * (reproj2 z)) . x by A56, FUNCT_1:13
.= (f * (reproj2 z)) /. x by A40, A63, PARTFUN1:def 6 ;
((f | Z) * (reproj2 z)) /. (z `2) = ((f | Z) * (reproj2 z)) . (z `2) by A58, A65, PARTFUN1:def 6
.= (f | Z) . ((reproj2 z) . (z `2)) by A56, FUNCT_1:13
.= f . ((reproj2 z) . (z `2)) by A1, A43, FUNCT_1:49
.= (f * (reproj2 z)) . (z `2) by A56, FUNCT_1:13
.= (f * (reproj2 z)) /. (z `2) by A40, A64, PARTFUN1:def 6 ;
hence (((f | Z) * (reproj2 z)) /. x) - (((f | Z) * (reproj2 z)) /. (z `2)) = ((partdiff`2 (f,z)) . (x - (z `2))) + (R /. (x - (z `2))) by A41, A53, A62, A67; :: thesis:

end;

hence f | Z is_partial_differentiable_in`2 z by A58, NDIFF_1:def 6; :: thesis:
(f | Z) * (reproj2 z) is_differentiable_in z `2 by A58, A61, NDIFF_1:def 6;
hence partdiff`2 ((f | Z),z) = partdiff`2 (f,z) by A58, A61, NDIFF_1:def 7; :: thesis: