let S, T, U be RealNormSpace; :: thesis:
let Z be Subset of S; :: thesis:
let u be PartFunc of S,T; :: thesis:
let v be PartFunc of S,U; :: thesis:
let w be PartFunc of S,[:T,U:]; :: thesis:
assume A1: ( u is_differentiable_on Z & v is_differentiable_on Z & w = <:u,v:> ) ; :: thesis:
A2: dom w = (dom u) /\ (dom v) by A1, FUNCT_3:def 7;
A3: Z is open by A1, NDIFF_1:32;
A4: Z c= dom w by A1, A2, XBOOLE_1:19;
for x being Point of S st x in Z holds
w is_differentiable_in x

let x be Point of S; :: thesis:
assume A5: x in Z ; :: thesis:
then A6: u is_differentiable_in x by A1, A3, NDIFF_1:31;
v is_differentiable_in x by A1, A3, A5, NDIFF_1:31;
hence w is_differentiable_in x by A1, A6, Th27; :: thesis:

end;

hence A7: w is_differentiable_on Z by A3, A4, NDIFF_1:31; :: thesis:
thus for x being Point of S st x in Z holds
(w `| Z) /. x = <:((u `| Z) /. x),((v `| Z) /. x):> :: thesis:

let x be Point of S; :: thesis:
assume A8: x in Z ; :: thesis:
then A9: u is_differentiable_in x by A1, A3, NDIFF_1:31;
A10: v is_differentiable_in x by A1, A3, A8, NDIFF_1:31;
thus (w `| Z) /. x = diff (w,x) by A7, A8, NDIFF_1:def 9
.= <:(diff (u,x)),(diff (v,x)):> by A1, A9, A10, Th27
.= <:((u `| Z) /. x),(diff (v,x)):> by A1, A8, NDIFF_1:def 9
.= <:((u `| Z) /. x),((v `| Z) /. x):> by A1, A8, NDIFF_1:def 9 ; :: thesis:

end;

thus for x being Point of S st x in Z holds
for dx being Point of S holds ((w `| Z) /. x) . dx = [(((u `| Z) /. x) . dx),(((v `| Z) /. x) . dx)] :: thesis:

let x be Point of S; :: thesis:
assume A11: x in Z ; :: thesis:
let dx be Point of S; :: thesis:
A12: u is_differentiable_in x by A1, A3, A11, NDIFF_1:31;
A13: v is_differentiable_in x by A1, A3, A11, NDIFF_1:31;
thus ((w `| Z) /. x) . dx = (diff (w,x)) . dx by A7, A11, NDIFF_1:def 9
.= [((diff (u,x)) . dx),((diff (v,x)) . dx)] by A1, A12, A13, Th27
.= [(((u `| Z) /. x) . dx),((diff (v,x)) . dx)] by A1, A11, NDIFF_1:def 9
.= [(((u `| Z) /. x) . dx),(((v `| Z) /. x) . dx)] by A1, A11, NDIFF_1:def 9 ; :: thesis:

end;