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

let x be Point of S; :: thesis:
assume A5: x in Z ; :: thesis:
then A6: u is_differentiable_in x by A1, A2, NDIFF_1:31;
A7: v is_differentiable_in x by A1, A2, A5, NDIFF_1:31;
thus ( w is_differentiable_in x & diff (w,x) = <:(diff (u,x)),(diff (v,x)):> ) by A1, A6, A7, Th54; :: thesis:

end;

then for x being Point of S st x in Z holds
w is_differentiable_in x ;
hence A8: w is_differentiable_on Z by A2, A3, 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 A9: x in Z ; :: thesis:
thus (w `| Z) /. x = diff (w,x) by A8, A9, NDIFF_1:def 9
.= <:(diff (u,x)),(diff (v,x)):> by A4, A9
.= <:((u `| Z) /. x),(diff (v,x)):> by A1, A9, NDIFF_1:def 9
.= <:((u `| Z) /. x),((v `| Z) /. x):> by A1, A9, NDIFF_1:def 9 ; :: thesis:

end;