let E, F be non trivial RealBanachSpace; :: thesis:
let D be Subset of E; :: thesis:
let f be PartFunc of E,F; :: thesis:
let f1 be PartFunc of [:E,F:],F; :: thesis:
let Z be Subset of [:E,F:]; :: thesis:
assume that
A1: D is open and
A2: ( dom f = D & D <> {} ) and
A3: f is_differentiable_on D and
A4: f `| D is_continuous_on D and
A5: Z = [:D, the carrier of F:] and
A6: dom f1 = Z and
A7: for s being Point of E
for t being Point of F st s in D holds
f1 . (s,t) = (f /. s) - t ; :: thesis:
A9: Z is open by A1, A5, Th4;
A10: for z being Point of [:E,F:] st z in Z holds
( f1 is_partial_differentiable_in`1 z & partdiff`1 (f1,z) = diff (f,(z `1)) )

proof

let z be Point of [:E,F:]; :: thesis:
assume A11: z in Z ; :: thesis:
consider x being Point of E, y being Point of F such that
A12: z = [x,y] by PRVECT_3:18;
set CST = D --> y;
A13: ( rng (D --> y) = {y} & dom (D --> y) = D ) by A2, FUNCOP_1:8, FUNCOP_1:13;
then reconsider CST = D --> y as PartFunc of E,F by RELSET_1:4;
A14: ( CST is_differentiable_on D & ( for s being Point of E st s in D holds
(CST `| D) /. s = 0. (R_NormSpace_of_BoundedLinearOperators (E,F)) ) ) by A1, A13, NDIFF_1:33;
A16: dom (f - CST) = D /\ D by A2, A13, VFUNCT_1:def 2
.= D ;
A17: for s being object holds
( s in dom (f1 * (reproj1 z)) iff s in dom (f - CST) )

proof

let s be object ; :: thesis:

hereby :: thesis:

assume A19: s in dom (f1 * (reproj1 z)) ; :: thesis:
then reconsider t = s as Point of E ;
(reproj1 z) . t = [t,(z `2)] by NDIFF_7:def 1
.= [t,y] by A12 ;
then [t,y] in dom f1 by A19, FUNCT_1:11;
hence s in dom (f - CST) by A5, A6, A16, ZFMISC_1:87; :: thesis:

end;

assume A20: s in dom (f - CST) ; :: thesis:
then reconsider t = s as Point of E ;
(reproj1 z) . t = [t,(z `2)] by NDIFF_7:def 1
.= [t,y] by A12 ;
then A23: (reproj1 z) . t in dom f1 by A5, A6, A16, A20, ZFMISC_1:87;
dom (reproj1 z) = the carrier of E by FUNCT_2:def 1;
hence s in dom (f1 * (reproj1 z)) by A23, FUNCT_1:11; :: thesis:

end;

A24: for s being object st s in dom (f1 * (reproj1 z)) holds
(f1 * (reproj1 z)) . s = (f - CST) . s

proof

let s be object ; :: thesis:
assume A25: s in dom (f1 * (reproj1 z)) ; :: thesis:
then A26: ( s in dom (reproj1 z) & (reproj1 z) . s in dom f1 ) by FUNCT_1:11;
reconsider t = s as Point of E by A25;
A27: (reproj1 z) . t = [t,(z `2)] by NDIFF_7:def 1
.= [t,y] by A12 ;
then A28: t in D by A5, A6, A26, ZFMISC_1:87;
then A29: CST /. s = CST . s by A13, PARTFUN1:def 6
.= y by A28, FUNCOP_1:7 ;
thus (f1 * (reproj1 z)) . s = f1 . (t,y) by A25, A27, FUNCT_1:12
.= (f /. t) - (CST /. s) by A7, A28, A29
.= (f - CST) /. s by A17, A25, VFUNCT_1:def 2
.= (f - CST) . s by A17, A25, PARTFUN1:def 6 ; :: thesis:

end;

A32: x in D by A5, A11, A12, ZFMISC_1:87;
then A33: f is_differentiable_in x by A1, A3, NDIFF_1:31;
CST is_differentiable_in x by A1, A14, A32, NDIFF_1:31;
then A34: ( f - CST is_differentiable_in x & diff ((f - CST),x) = (diff (f,x)) - (diff (CST,x)) ) by A33, NDIFF_1:36;
hence f1 is_partial_differentiable_in`1 z by A12, A17, A24, FUNCT_1:2, TARSKI:2; :: thesis:
A36: diff (CST,x) = (CST `| D) /. x by A14, A32, NDIFF_1:def 9
.= 0. (R_NormSpace_of_BoundedLinearOperators (E,F)) by A1, A13, A32, NDIFF_1:33 ;
thus partdiff`1 (f1,z) = diff ((f - CST),x) by A12, A17, A24, FUNCT_1:2, TARSKI:2
.= diff (f,(z `1)) by A12, A34, A36, RLVECT_1:13 ; :: thesis:

end;

then A37: f1 is_partial_differentiable_on`1 Z by A6;
then A38: Z = dom (f1 `partial`1| Z) by NDIFF_7:def 10;
for x0 being Point of [:E,F:]
for r being Real st x0 in Z & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Point of [:E,F:] st x1 in Z & ||.(x1 - x0).|| < s holds
||.(((f1 `partial`1| Z) /. x1) - ((f1 `partial`1| Z) /. x0)).|| < r ) )

proof

let x0 be Point of [:E,F:]; :: thesis:
let r be Real; :: thesis:
assume A39: ( x0 in Z & 0 < r ) ; :: thesis:
consider s0 being Point of E, t0 being Point of F such that
A40: x0 = [s0,t0] by PRVECT_3:18;
A41: s0 in D by A5, A39, A40, ZFMISC_1:87;
then consider s being Real such that
A43: ( 0 < s & ( for s1 being Point of E st s1 in D & ||.(s1 - s0).|| < s holds
||.(((f `| D) /. s1) - ((f `| D) /. s0)).|| < r ) ) by A4, A39, NFCONT_1:19;
take s ; :: thesis:
thus 0 < s by A43; :: thesis:
let x1 be Point of [:E,F:]; :: thesis:
assume A44: ( x1 in Z & ||.(x1 - x0).|| < s ) ; :: thesis:
consider s1 being Point of E, t1 being Point of F such that
A45: x1 = [s1,t1] by PRVECT_3:18;
A46: s1 in D by A5, A44, A45, ZFMISC_1:87;
- x0 = [(- s0),(- t0)] by A40, PRVECT_3:18;
then x1 - x0 = [(s1 - s0),(t1 - t0)] by A45, PRVECT_3:18;
then ||.(s1 - s0).|| <= ||.(x1 - x0).|| by LOPBAN_7:15;
then A48: ||.(s1 - s0).|| < s by A44, XXREAL_0:2;
A49: (f `| D) /. s1 = diff (f,(x1 `1)) by A3, A45, A46, NDIFF_1:def 9
.= partdiff`1 (f1,x1) by A10, A44
.= (f1 `partial`1| Z) /. x1 by A37, A44, NDIFF_7:def 10 ;
(f `| D) /. s0 = diff (f,(x0 `1)) by A3, A40, A41, NDIFF_1:def 9
.= partdiff`1 (f1,x0) by A10, A39
.= (f1 `partial`1| Z) /. x0 by A37, A39, NDIFF_7:def 10 ;
hence ||.(((f1 `partial`1| Z) /. x1) - ((f1 `partial`1| Z) /. x0)).|| < r by A43, A46, A48, A49; :: thesis:

end;

then A50: f1 `partial`1| Z is_continuous_on Z by A38, NFCONT_1:19;
reconsider J = FuncUnit F as Point of (R_NormSpace_of_BoundedLinearOperators (F,F)) ;
A51: for z being Point of [:E,F:] st z in Z holds
( f1 is_partial_differentiable_in`2 z & partdiff`2 (f1,z) = - J )

proof

let z be Point of [:E,F:]; :: thesis:
assume A52: z in Z ; :: thesis:
the carrier of F c= the carrier of F ;
then reconsider CF = the carrier of F as Subset of F ;
for y being Point of F st y in CF holds
ex r being Real st
( 0 < r & Ball (y,r) c= CF )

proof

let y be Point of F; :: thesis:
assume y in CF ; :: thesis:
take r = 1; :: thesis:
thus 0 < r ; :: thesis:
thus Ball (y,r) c= CF ; :: thesis:

end;

then A53: CF is open by NDIFF_8:20;
consider x being Point of E, y being Point of F such that
A54: z = [x,y] by PRVECT_3:18;
A55: x in D by A5, A52, A54, ZFMISC_1:87;
set fx = CF --> (f /. x);
A57: ( rng (CF --> (f /. x)) = {(f /. x)} & dom (CF --> (f /. x)) = CF ) by FUNCOP_1:8, FUNCOP_1:13;
reconsider fx = CF --> (f /. x) as PartFunc of F,F ;
A58: ( fx is_differentiable_on CF & ( for s being Point of F st s in CF holds
(fx `| CF) /. s = 0. (R_NormSpace_of_BoundedLinearOperators (F,F)) ) ) by A53, A57, NDIFF_1:33;
set I = id CF;
A59: ( dom (id CF) = CF & rng (id CF) = CF ) ;
A60: (id CF) | CF = id CF ;
reconsider I = id CF as PartFunc of F,F ;
A61: ( I is_differentiable_on CF & ( for s being Point of F st s in CF holds
(I `| CF) /. s = id CF ) ) by A53, A59, A60, NDIFF_1:38;
( dom (fx - I) = (dom fx) /\ (dom I) & ( for s being Element of F st s in dom (fx - I) holds
(fx - I) /. s = (fx /. s) - (I /. s) ) ) by VFUNCT_1:def 2;
then A63: dom (fx - I) = CF /\ CF by FUNCOP_1:13
.= CF ;
A64: for s being object holds
( s in dom (f1 * (reproj2 z)) iff s in dom (fx - I) )

proof

let s be object ; :: thesis:
A66: ( s in dom (f1 * (reproj2 z)) iff ( s in dom (reproj2 z) & (reproj2 z) . s in dom f1 ) ) by FUNCT_1:11;
thus ( s in dom (f1 * (reproj2 z)) implies s in dom (fx - I) ) by A63; :: thesis:
assume s in dom (fx - I) ; :: thesis:
then reconsider t = s as Point of F ;
A69: (reproj2 z) . t = [(z `1),t] by NDIFF_7:def 2
.= [x,t] by A54 ;
dom (reproj2 z) = the carrier of F by FUNCT_2:def 1;
hence s in dom (f1 * (reproj2 z)) by A5, A6, A55, A66, A69, ZFMISC_1:87; :: thesis:

end;

A71: for s being object st s in dom (f1 * (reproj2 z)) holds
(f1 * (reproj2 z)) . s = (fx - I) . s

proof

let s be object ; :: thesis:
assume A72: s in dom (f1 * (reproj2 z)) ; :: thesis:
then reconsider t = s as Point of F ;
A73: (reproj2 z) . t = [(z `1),t] by NDIFF_7:def 2
.= [x,t] by A54 ;
A74: t in CF ;
then A75: I /. s = I . s by A59, PARTFUN1:def 6
.= s by A74 ;
A76: fx /. s = fx . s by A57, A74, PARTFUN1:def 6
.= f /. x by A74, FUNCOP_1:7 ;
thus (f1 * (reproj2 z)) . s = f1 . (x,t) by A72, A73, FUNCT_1:12
.= (f /. x) - (I /. s) by A7, A55, A75
.= (fx - I) /. s by A64, A72, A76, VFUNCT_1:def 2
.= (fx - I) . s by A64, A72, PARTFUN1:def 6 ; :: thesis:

end;

A79: fx is_differentiable_in y by A53, A58, NDIFF_1:31;
I is_differentiable_in y by A53, A61, NDIFF_1:31;
then A80: ( fx - I is_differentiable_in y & diff ((fx - I),y) = (diff (fx,y)) - (diff (I,y)) ) by A79, NDIFF_1:36;
hence f1 is_partial_differentiable_in`2 z by A54, A64, A71, FUNCT_1:2, TARSKI:2; :: thesis:
A82: diff (I,y) = (I `| CF) /. y by A61, NDIFF_1:def 9
.= J by A53, A59, A60, NDIFF_1:38 ;
diff (fx,y) = (fx `| CF) /. y by A58, NDIFF_1:def 9
.= 0. (R_NormSpace_of_BoundedLinearOperators (F,F)) by A53, A57, NDIFF_1:33 ;
then diff ((fx - I),y) = - J by A80, A82, RLVECT_1:14;
hence partdiff`2 (f1,z) = - J by A54, A64, A71, FUNCT_1:2, TARSKI:2; :: thesis:

end;

then A84: f1 is_partial_differentiable_on`2 Z by A6;
then A85: Z = dom (f1 `partial`2| Z) by NDIFF_7:def 11;
for x0 being Point of [:E,F:]
for r being Real st x0 in Z & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Point of [:E,F:] st x1 in Z & ||.(x1 - x0).|| < s holds
||.(((f1 `partial`2| Z) /. x1) - ((f1 `partial`2| Z) /. x0)).|| < r ) )

proof

let x0 be Point of [:E,F:]; :: thesis:
let r be Real; :: thesis:
assume A86: ( x0 in Z & 0 < r ) ; :: thesis:
take s = 1; :: thesis:
thus 0 < s ; :: thesis:
let x1 be Point of [:E,F:]; :: thesis:
assume A88: ( x1 in Z & ||.(x1 - x0).|| < s ) ; :: thesis:
A90: - J = partdiff`2 (f1,x1) by A51, A88
.= (f1 `partial`2| Z) /. x1 by A84, A88, NDIFF_7:def 11 ;
- J = partdiff`2 (f1,x0) by A51, A86
.= (f1 `partial`2| Z) /. x0 by A84, A86, NDIFF_7:def 11 ;
then ((f1 `partial`2| Z) /. x1) - ((f1 `partial`2| Z) /. x0) = 0. (R_NormSpace_of_BoundedLinearOperators (F,F)) by A90, RLVECT_1:15;
hence ||.(((f1 `partial`2| Z) /. x1) - ((f1 `partial`2| Z) /. x0)).|| < r by A86, NORMSP_0:def 6; :: thesis:

end;

then f1 `partial`2| Z is_continuous_on Z by A85, NFCONT_1:19;
hence ( f1 is_differentiable_on Z & f1 `| Z is_continuous_on Z ) by A9, A37, A50, A84, NDIFF_7:52; :: thesis:
thus for x being Point of E
for y being Point of F
for z being Point of [:E,F:] st x in D & z = [x,y] holds
ex I being Point of (R_NormSpace_of_BoundedLinearOperators (F,F)) st
( I = id the carrier of F & partdiff`1 (f1,z) = diff (f,x) & partdiff`2 (f1,z) = - I ) :: thesis:

proof

let x be Point of E; :: thesis:
let y be Point of F; :: thesis:
let z be Point of [:E,F:]; :: thesis:
assume A92: ( x in D & z = [x,y] ) ; :: thesis:
then A93: z in Z by A5, ZFMISC_1:87;
take J ; :: thesis:
thus J = id the carrier of F ; :: thesis:
thus partdiff`1 (f1,z) = diff (f,x) by A10, A92, A93; :: thesis:
thus partdiff`2 (f1,z) = - J by A51, A93; :: thesis:

end;