let E, F, G be RealNormSpace; :: thesis:
let Z be Subset of [:E,F:]; :: thesis:
let f be PartFunc of [:E,F:],G; :: thesis:
assume A1: f is_differentiable_on Z ; :: thesis:
then A2: Z is open by NDIFF_1:32;
for z being Point of [:E,F:] st z in Z holds
f is_partial_differentiable_in`1 z

proof

let z be Point of [:E,F:]; :: thesis:
assume z in Z ; :: thesis:
then f is_differentiable_in z by A1, A2, NDIFF_1:31;
hence f is_partial_differentiable_in`1 z by NDIFF_9:14; :: thesis:

end;

hence A3: f is_partial_differentiable_on`1 Z by A1, A2, NDIFF_7:43; :: thesis:
for z being Point of [:E,F:] st z in Z holds
f is_partial_differentiable_in`2 z

proof

let z be Point of [:E,F:]; :: thesis:
assume z in Z ; :: thesis:
then f is_differentiable_in z by A1, A2, NDIFF_1:31;
hence f is_partial_differentiable_in`2 z by NDIFF_9:14; :: thesis:

end;

hence A4: f is_partial_differentiable_on`2 Z by A1, A2, NDIFF_7:44; :: thesis:
let z be Point of [:E,F:]; :: thesis:
assume A5: z in Z ; :: thesis:
then A6: f is_differentiable_in z by A1, A2, NDIFF_1:31;
reconsider L1 = partdiff`1 (f,z) as Lipschitzian LinearOperator of E,G by LOPBAN_1:def 9;
reconsider L2 = partdiff`2 (f,z) as Lipschitzian LinearOperator of F,G by LOPBAN_1:def 9;
A7: (partdiff`1 (f,z)) . (0. E) = L1 . (0 * (0. E)) by RLVECT_1:10
.= 0 * (L1 . (0. E)) by LOPBAN_1:def 5
.= 0. G by RLVECT_1:10 ;
A8: (partdiff`2 (f,z)) . (0. F) = L2 . (0 * (0. F)) by RLVECT_1:10
.= 0 * (L2 . (0. F)) by LOPBAN_1:def 5
.= 0. G by RLVECT_1:10 ;
thus for dx being Point of E holds ((f `partial`1| Z) /. z) . dx = ((f `| Z) /. z) . (dx,(0. F)) :: thesis:

proof

let dx be Point of E; :: thesis:
((f `| Z) /. z) . (dx,(0. F)) = (diff (f,z)) . (dx,(0. F)) by A1, A5, NDIFF_1:def 9
.= (diff (f,z)) . [dx,(0. F)] by BINOP_1:def 1
.= ((partdiff`1 (f,z)) . dx) + ((partdiff`2 (f,z)) . (0. F)) by A6, NDIFF_9:14
.= (partdiff`1 (f,z)) . dx by A8, RLVECT_1:4
.= ((f `partial`1| Z) /. z) . dx by A3, A5, NDIFF_7:def 10 ;
hence ((f `partial`1| Z) /. z) . dx = ((f `| Z) /. z) . (dx,(0. F)) ; :: thesis:

end;

thus for dy being Point of F holds ((f `partial`2| Z) /. z) . dy = ((f `| Z) /. z) . ((0. E),dy) :: thesis:

proof

let dy be Point of F; :: thesis:
((f `| Z) /. z) . ((0. E),dy) = (diff (f,z)) . ((0. E),dy) by A1, A5, NDIFF_1:def 9
.= (diff (f,z)) . [(0. E),dy] by BINOP_1:def 1
.= ((partdiff`1 (f,z)) . (0. E)) + ((partdiff`2 (f,z)) . dy) by A6, NDIFF_9:14
.= (partdiff`2 (f,z)) . dy by A7, RLVECT_1:4
.= ((f `partial`2| Z) /. z) . dy by A4, A5, NDIFF_7:def 11 ;
hence ((f `partial`2| Z) /. z) . dy = ((f `| Z) /. z) . ((0. E),dy) ; :: thesis:

end;