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 x0 be Point of S; :: thesis:
assume A1: ( w = <:u,v:> & u is_differentiable_in x0 & v is_differentiable_in x0 ) ; :: thesis:
consider Nu being Neighbourhood of x0 such that
A2: ( Nu c= dom u & ex Ru being RestFunc of S,E st
for x being Point of S st x in Nu holds
(u /. x) - (u /. x0) = ((diff (u,x0)) . (x - x0)) + (Ru /. (x - x0)) ) by A1, NDIFF_1:def 7;
consider Ru being RestFunc of S,E such that
A3: for x being Point of S st x in Nu holds
(u /. x) - (u /. x0) = ((diff (u,x0)) . (x - x0)) + (Ru /. (x - x0)) by A2;
consider Nv being Neighbourhood of x0 such that
A4: ( Nv c= dom v & ex Rv being RestFunc of S,F st
for x being Point of S st x in Nv holds
(v /. x) - (v /. x0) = ((diff (v,x0)) . (x - x0)) + (Rv /. (x - x0)) ) by A1, NDIFF_1:def 7;
consider Rv being RestFunc of S,F such that
A5: for x being Point of S st x in Nv holds
(v /. x) - (v /. x0) = ((diff (v,x0)) . (x - x0)) + (Rv /. (x - x0)) by A4;
consider N being Neighbourhood of x0 such that
A6: N c= Nu and
A7: N c= Nv by NDIFF_1:1;
reconsider L1 = diff (u,x0) as Lipschitzian LinearOperator of S,E by LOPBAN_1:def 9;
reconsider L2 = diff (v,x0) as Lipschitzian LinearOperator of S,F by LOPBAN_1:def 9;
set L = <:(diff (u,x0)),(diff (v,x0)):>;
A8: dom <:(diff (u,x0)),(diff (v,x0)):> = (dom L1) /\ (dom L2) by FUNCT_3:def 7
.= the carrier of S /\ (dom L2) by FUNCT_2:def 1
.= the carrier of S /\ the carrier of S by FUNCT_2:def 1
.= the carrier of S ;
A9: rng <:(diff (u,x0)),(diff (v,x0)):> c= [:(rng L1),(rng L2):] by FUNCT_3:51;
[:(rng L1),(rng L2):] c= the carrier of [:E,F:] by ZFMISC_1:96;
then reconsider L = <:(diff (u,x0)),(diff (v,x0)):> as Function of S,[:E,F:] by A8, A9, FUNCT_2:2, XBOOLE_1:1;
A10: ( L1 is additive & L2 is additive ) ;
for x, y being Element of S holds L . (x + y) = (L . x) + (L . y)

proof

let x, y be Element of S; :: thesis:
A11: L . x = [(L1 . x),(L2 . x)] by A8, FUNCT_3:def 7;
A12: L . y = [(L1 . y),(L2 . y)] by A8, FUNCT_3:def 7;
thus L . (x + y) = [(L1 . (x + y)),(L2 . (x + y))] by A8, FUNCT_3:def 7
.= [((L1 . x) + (L1 . y)),(L2 . (x + y))] by A10
.= [((L1 . x) + (L1 . y)),((L2 . x) + (L2 . y))] by A10
.= (L . x) + (L . y) by A11, A12, PRVECT_3:18 ; :: thesis:

end;

then A13: L is additive ;
for x being VECTOR of S
for a being Real holds L . (a * x) = a * (L . x)

proof

let x be VECTOR of S; :: thesis:
let a be Real; :: thesis:
A14: L . x = [(L1 . x),(L2 . x)] by A8, FUNCT_3:def 7;
thus L . (a * x) = [(L1 . (a * x)),(L2 . (a * x))] by A8, FUNCT_3:def 7
.= [(a * (L1 . x)),(L2 . (a * x))] by LOPBAN_1:def 5
.= [(a * (L1 . x)),(a * (L2 . x))] by LOPBAN_1:def 5
.= a * (L . x) by A14, PRVECT_3:18 ; :: thesis:

end;

then reconsider L = L as LinearOperator of S,[:E,F:] by A13, LOPBAN_1:def 5;
set K = ||.(diff (u,x0)).|| + ||.(diff (v,x0)).||;
( 0 <= ||.(diff (u,x0)).|| & 0 <= ||.(diff (v,x0)).|| ) by NORMSP_1:4;
then A15: 0 + 0 <= ||.(diff (u,x0)).|| + ||.(diff (v,x0)).|| by XREAL_1:7;
for x being VECTOR of S holds ||.(L . x).|| <= (||.(diff (u,x0)).|| + ||.(diff (v,x0)).||) * ||.x.||

proof

let x be VECTOR of S; :: thesis:
L . x = [(L1 . x),(L2 . x)] by A8, FUNCT_3:def 7;
then A16: ||.(L . x).|| <= ||.(L1 . x).|| + ||.(L2 . x).|| by Th17;
A17: ||.(L1 . x).|| <= ||.(diff (u,x0)).|| * ||.x.|| by LOPBAN_1:32;
||.(L2 . x).|| <= ||.(diff (v,x0)).|| * ||.x.|| by LOPBAN_1:32;
then ||.(L1 . x).|| + ||.(L2 . x).|| <= (||.(diff (u,x0)).|| * ||.x.||) + (||.(diff (v,x0)).|| * ||.x.||) by A17, XREAL_1:7;
hence ||.(L . x).|| <= (||.(diff (u,x0)).|| + ||.(diff (v,x0)).||) * ||.x.|| by A16, XXREAL_0:2; :: thesis:

end;

then L is Lipschitzian by A15, LOPBAN_1:def 8;
then reconsider L = L as Point of (R_NormSpace_of_BoundedLinearOperators (S,[:E,F:])) by LOPBAN_1:def 9;
set R = <:Ru,Rv:>;
Ru is total by NDIFF_1:def 5;
then A18: dom Ru = the carrier of S by PARTFUN1:def 2;
Rv is total by NDIFF_1:def 5;
then A19: dom Rv = the carrier of S by PARTFUN1:def 2;
A20: dom <:Ru,Rv:> = (dom Ru) /\ (dom Rv) by FUNCT_3:def 7
.= the carrier of S by A18, A19 ;
A21: rng <:Ru,Rv:> c= [:(rng Ru),(rng Rv):] by FUNCT_3:51;
[:(rng Ru),(rng Rv):] c= [:([#] E),([#] F):] by ZFMISC_1:96;
then rng <:Ru,Rv:> c= the carrier of [:E,F:] by A21, XBOOLE_1:1;
then reconsider R = <:Ru,Rv:> as PartFunc of S,[:E,F:] by A20, RELSET_1:4;
A22: R is total by A20, PARTFUN1:def 2;
A23: for dx being Point of S holds R /. dx = [(Ru /. dx),(Rv /. dx)]

proof

let dx be Point of S; :: thesis:
thus R /. dx = R . dx by A20, PARTFUN1:def 6
.= [(Ru . dx),(Rv . dx)] by A20, FUNCT_3:def 7
.= [(Ru /. dx),(Rv . dx)] by A18, PARTFUN1:def 6
.= [(Ru /. dx),(Rv /. dx)] by A19, PARTFUN1:def 6 ; :: thesis:

end;

for r being Real st r > 0 holds
ex d being Real st
( d > 0 & ( for z being Point of S st z <> 0. S & ||.z.|| < d holds
(||.z.|| ") * ||.(R /. z).|| < r ) )

proof

let r0 be Real; :: thesis:
assume A24: r0 > 0 ; :: thesis:
set r = r0 / 2;
A25: ( 0 < r0 / 2 & r0 / 2 < r0 ) by A24, XREAL_1:215, XREAL_1:216;
Ru is RestFunc-like ;
then consider d1 being Real such that
A26: ( d1 > 0 & ( for z being Point of S st z <> 0. S & ||.z.|| < d1 holds
(||.z.|| ") * ||.(Ru /. z).|| < r0 / 2 ) ) by A25, NDIFF_1:23;
Rv is RestFunc-like ;
then consider d2 being Real such that
A27: ( d2 > 0 & ( for z being Point of S st z <> 0. S & ||.z.|| < d2 holds
(||.z.|| ") * ||.(Rv /. z).|| < r0 / 2 ) ) by A25, NDIFF_1:23;
reconsider d = min (d1,d2) as Real ;
take d ; :: thesis:
thus 0 < d by A26, A27, XXREAL_0:15; :: thesis:
let z be Point of S; :: thesis:
assume A28: ( z <> 0. S & ||.z.|| < d ) ; :: thesis:
d <= d1 by XXREAL_0:17;
then ||.z.|| < d1 by A28, XXREAL_0:2;
then A29: (||.z.|| ") * ||.(Ru /. z).|| < r0 / 2 by A26, A28;
d <= d2 by XXREAL_0:17;
then ||.z.|| < d2 by A28, XXREAL_0:2;
then A30: (||.z.|| ") * ||.(Rv /. z).|| < r0 / 2 by A27, A28;
A31: R /. z = [(Ru /. z),(Rv /. z)] by A23;
0 <= ||.z.|| by NORMSP_1:4;
then 0 < ||.z.|| by A28, XXREAL_0:1, NORMSP_0:def 5;
then 0 < ||.z.|| " by XREAL_1:122;
then A32: (||.z.|| ") * ||.(R /. z).|| <= (||.z.|| ") * (||.(Ru /. z).|| + ||.(Rv /. z).||) by A31, Th17, XREAL_1:64;
((||.z.|| ") * ||.(Ru /. z).||) + ((||.z.|| ") * ||.(Rv /. z).||) < (r0 / 2) + (r0 / 2) by A29, A30, XREAL_1:8;
hence (||.z.|| ") * ||.(R /. z).|| < r0 by A32, XXREAL_0:2; :: thesis:

end;

then reconsider R = R as RestFunc of S,[:E,F:] by A22, NDIFF_1:23;
A33: dom w = (dom u) /\ (dom v) by A1, FUNCT_3:def 7;
A34: N c= dom u by A2, A6, XBOOLE_1:1;
A35: N c= dom v by A4, A7, XBOOLE_1:1;
A36: N c= dom w by A33, A34, A35, XBOOLE_1:19;
A37: for x being Point of S st x in N holds
(w /. x) - (w /. x0) = (L . (x - x0)) + (R /. (x - x0))

proof

let x be Point of S; :: thesis:
assume A38: x in N ; :: thesis:
A39: x0 in N by NFCONT_1:4;
R is total by NDIFF_1:def 5;
then A40: dom R = the carrier of S by PARTFUN1:def 2;
Ru is total by NDIFF_1:def 5;
then A41: dom Ru = the carrier of S by PARTFUN1:def 2;
Rv is total by NDIFF_1:def 5;
then A42: dom Rv = the carrier of S by PARTFUN1:def 2;
A43: w /. x = w . x by A36, A38, PARTFUN1:def 6
.= [(u . x),(v . x)] by A1, A38, A36, FUNCT_3:def 7
.= [(u /. x),(v . x)] by A34, A38, PARTFUN1:def 6
.= [(u /. x),(v /. x)] by A35, A38, PARTFUN1:def 6 ;
w /. x0 = w . x0 by A36, A39, PARTFUN1:def 6
.= [(u . x0),(v . x0)] by A1, A36, A39, FUNCT_3:def 7
.= [(u /. x0),(v . x0)] by A34, A39, PARTFUN1:def 6
.= [(u /. x0),(v /. x0)] by A35, A39, PARTFUN1:def 6 ;
then A44: - (w /. x0) = [(- (u /. x0)),(- (v /. x0))] by PRVECT_3:18;
A45: (w /. x) - (w /. x0) = [((u /. x) - (u /. x0)),((v /. x) - (v /. x0))] by A43, A44, PRVECT_3:18;
A46: (u /. x) - (u /. x0) = ((diff (u,x0)) . (x - x0)) + (Ru /. (x - x0)) by A3, A6, A38;
A47: (v /. x) - (v /. x0) = ((diff (v,x0)) . (x - x0)) + (Rv /. (x - x0)) by A5, A7, A38;
A48: R /. (x - x0) = R . (x - x0) by A40, PARTFUN1:def 6
.= [(Ru . (x - x0)),(Rv . (x - x0))] by A40, FUNCT_3:def 7
.= [(Ru /. (x - x0)),(Rv . (x - x0))] by A41, PARTFUN1:def 6
.= [(Ru /. (x - x0)),(Rv /. (x - x0))] by A42, PARTFUN1:def 6 ;
A49: L . (x - x0) = [((diff (u,x0)) . (x - x0)),((diff (v,x0)) . (x - x0))] by FUNCT_3:def 7, A8;
thus (w /. x) - (w /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A45, A46, A47, A48, A49, PRVECT_3:18; :: thesis:

end;

hence w is_differentiable_in x0 by A33, A34, A35, XBOOLE_1:19; :: thesis:
hence diff (w,x0) = <:(diff (u,x0)),(diff (v,x0)):> by A36, A37, NDIFF_1:def 7; :: thesis: