let S, T, U be RealNormSpace; :: thesis: for x being Point of S
for u being PartFunc of S,T
for v being PartFunc of S,U
for w being PartFunc of S,[:T,U:] st u is_differentiable_in x & v is_differentiable_in x & w = <:u,v:> holds
( w is_differentiable_in x & diff (w,x) = <:(diff (u,x)),(diff (v,x)):> & ( for dx being Point of S holds (diff (w,x)) . dx = [((diff (u,x)) . dx),((diff (v,x)) . dx)] ) )
let x0 be Point of S; :: thesis: for u being PartFunc of S,T
for v being PartFunc of S,U
for w being PartFunc of S,[:T,U:] st u is_differentiable_in x0 & v is_differentiable_in x0 & w = <:u,v:> holds
( w is_differentiable_in x0 & diff (w,x0) = <:(diff (u,x0)),(diff (v,x0)):> & ( for dx being Point of S holds (diff (w,x0)) . dx = [((diff (u,x0)) . dx),((diff (v,x0)) . dx)] ) )
let f1 be PartFunc of S,T; :: thesis: for v being PartFunc of S,U
for w being PartFunc of S,[:T,U:] st f1 is_differentiable_in x0 & v is_differentiable_in x0 & w = <:f1,v:> holds
( w is_differentiable_in x0 & diff (w,x0) = <:(diff (f1,x0)),(diff (v,x0)):> & ( for dx being Point of S holds (diff (w,x0)) . dx = [((diff (f1,x0)) . dx),((diff (v,x0)) . dx)] ) )
let f2 be PartFunc of S,U; :: thesis: for w being PartFunc of S,[:T,U:] st f1 is_differentiable_in x0 & f2 is_differentiable_in x0 & w = <:f1,f2:> holds
( w is_differentiable_in x0 & diff (w,x0) = <:(diff (f1,x0)),(diff (f2,x0)):> & ( for dx being Point of S holds (diff (w,x0)) . dx = [((diff (f1,x0)) . dx),((diff (f2,x0)) . dx)] ) )
let w be PartFunc of S,[:T,U:]; :: thesis: ( f1 is_differentiable_in x0 & f2 is_differentiable_in x0 & w = <:f1,f2:> implies ( w is_differentiable_in x0 & diff (w,x0) = <:(diff (f1,x0)),(diff (f2,x0)):> & ( for dx being Point of S holds (diff (w,x0)) . dx = [((diff (f1,x0)) . dx),((diff (f2,x0)) . dx)] ) ) )
assume that
A1: f1 is_differentiable_in x0 and
A2: f2 is_differentiable_in x0 and
A3: w = <:f1,f2:> ; :: thesis: ( w is_differentiable_in x0 & diff (w,x0) = <:(diff (f1,x0)),(diff (f2,x0)):> & ( for dx being Point of S holds (diff (w,x0)) . dx = [((diff (f1,x0)) . dx),((diff (f2,x0)) . dx)] ) )
A4: dom w = (dom f1) /\ (dom f2) by A3, FUNCT_3:def 7;
A5: for t being Point of S st t in dom w holds
w /. t = [(f1 /. t),(f2 /. t)]
proof
let t be Point of S; :: thesis: ( t in dom w implies w /. t = [(f1 /. t),(f2 /. t)] )
assume A6: t in dom w ; :: thesis: w /. t = [(f1 /. t),(f2 /. t)]
then A7: t in dom f1 by A4, XBOOLE_0:def 4;
A8: t in dom f2 by A4, A6, XBOOLE_0:def 4;
thus w /. t = w . t by A6, PARTFUN1:def 6
.= [(f1 . t),(f2 . t)] by A3, A6, FUNCT_3:def 7
.= [(f1 /. t),(f2 . t)] by A7, PARTFUN1:def 6
.= [(f1 /. t),(f2 /. t)] by A8, PARTFUN1:def 6 ; :: thesis: verum
end;
consider N1 being Neighbourhood of x0 such that
A9: N1 c= dom f1 and
A10: ex L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) ex R being RestFunc of S,T st
for x being Point of S st x in N1 holds
(f1 /. x) - (f1 /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A1;
consider L1 being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)), R1 being RestFunc of S,T such that
A11: for x being Point of S st x in N1 holds
(f1 /. x) - (f1 /. x0) = (L1 . (x - x0)) + (R1 /. (x - x0)) by A10;
A12: diff (f1,x0) = L1 by A1, A9, A11, NDIFF_1:def 7;
consider N2 being Neighbourhood of x0 such that
A13: N2 c= dom f2 and
A14: ex L being Point of (R_NormSpace_of_BoundedLinearOperators (S,U)) ex R being RestFunc of S,U st
for x being Point of S st x in N2 holds
(f2 /. x) - (f2 /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A2;
consider L2 being Point of (R_NormSpace_of_BoundedLinearOperators (S,U)), R2 being RestFunc of S,U such that
A15: for x being Point of S st x in N2 holds
(f2 /. x) - (f2 /. x0) = (L2 . (x - x0)) + (R2 /. (x - x0)) by A14;
A16: diff (f2,x0) = L2 by A2, A13, A15, NDIFF_1:def 7;
deffunc H1( object ) -> Element of the carrier of [:T,U:] = [(R1 /. $1),(R2 /. $1)];
A17: for x being object st x in the carrier of S holds
H1(x) in the carrier of [:T,U:] ;
consider R being Function of S,[:T,U:] such that
A18: for dx being object st dx in the carrier of S holds
R . dx = H1(dx) from FUNCT_2:sch 2(A17);
 A19: for dx being Point of S holds R /. dx = [(R1 /. dx),(R2 /. dx)] by A18;
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: ( r0 > 0 implies ex d being Real st
( d > 0 & ( for z being Point of S st z <> 0. S & ||.z.|| < d holds
(||.z.|| ") * ||.(R /. z).|| < r0 ) ) )
assume A20: r0 > 0 ; :: thesis: ex d being Real st
( d > 0 & ( for z being Point of S st z <> 0. S & ||.z.|| < d holds
(||.z.|| ") * ||.(R /. z).|| < r0 ) )
set r = r0 / 2;
A21: ( 0 < r0 / 2 & r0 / 2 < r0 ) by A20, XREAL_1:215, XREAL_1:216;
R1 is RestFunc-like ;
then consider d1 being Real such that
A22: ( d1 > 0 & ( for z being Point of S st z <> 0. S & ||.z.|| < d1 holds
(||.z.|| ") * ||.(R1 /. z).|| < r0 / 2 ) ) by A21, NDIFF_1:23;
R2 is RestFunc-like ;
then consider d2 being Real such that
A23: ( d2 > 0 & ( for z being Point of S st z <> 0. S & ||.z.|| < d2 holds
(||.z.|| ") * ||.(R2 /. z).|| < r0 / 2 ) ) by A21, NDIFF_1:23;
reconsider d = min (d1,d2) as Real ;
take d ; :: thesis: ( d > 0 & ( for z being Point of S st z <> 0. S & ||.z.|| < d holds
(||.z.|| ") * ||.(R /. z).|| < r0 ) )
thus 0 < d by A22, A23, XXREAL_0:15; :: thesis: for z being Point of S st z <> 0. S & ||.z.|| < d holds
(||.z.|| ") * ||.(R /. z).|| < r0
let z be Point of S; :: thesis: ( z <> 0. S & ||.z.|| < d implies (||.z.|| ") * ||.(R /. z).|| < r0 )
assume A24: ( z <> 0. S & ||.z.|| < d ) ; :: thesis: (||.z.|| ") * ||.(R /. z).|| < r0
d <= d1 by XXREAL_0:17;
then ||.z.|| < d1 by A24, XXREAL_0:2;
then A25: (||.z.|| ") * ||.(R1 /. z).|| < r0 / 2 by A22, A24;
d <= d2 by XXREAL_0:17;
then ||.z.|| < d2 by A24, XXREAL_0:2;
then A26: (||.z.|| ") * ||.(R2 /. z).|| < r0 / 2 by A23, A24;
A27: R /. z = [(R1 /. z),(R2 /. z)] by A18;
0 <= ||.z.|| by NORMSP_1:4;
then 0 < ||.z.|| by A24, XXREAL_0:1, NORMSP_0:def 5;
then 0 < ||.z.|| " by XREAL_1:122;
then A28: (||.z.|| ") * ||.(R /. z).|| <= (||.z.|| ") * (||.(R1 /. z).|| + ||.(R2 /. z).||) by A27, Th17, XREAL_1:64;
((||.z.|| ") * ||.(R1 /. z).||) + ((||.z.|| ") * ||.(R2 /. z).||) < (r0 / 2) + (r0 / 2) by A25, A26, XREAL_1:8;
hence (||.z.|| ") * ||.(R /. z).|| < r0 by A28, XXREAL_0:2; :: thesis: verum
end;
then reconsider R = R as RestFunc of S,[:T,U:] by NDIFF_1:23;
deffunc H2( object ) -> object = [(L1 . $1),(L2 . $1)];
A29: for x being object st x in the carrier of S holds
H2(x) in the carrier of [:T,U:]
proof
let x be object ; :: thesis: ( x in the carrier of S implies H2(x) in the carrier of [:T,U:] )
assume x in the carrier of S ; :: thesis: H2(x) in the carrier of [:T,U:]
then reconsider y = x as Point of S ;
[(L1 . y),(L2 . y)] is Point of [:T,U:] ;
hence H2(x) in the carrier of [:T,U:] ; :: thesis: verum
end;
consider L being Function of S,[:T,U:] such that
A30: for dx being object st dx in the carrier of S holds
L . dx = H2(dx) from FUNCT_2:sch 2(A29);
 reconsider LL1 = L1 as Lipschitzian LinearOperator of S,T by LOPBAN_1:def 9;
reconsider LL2 = L2 as Lipschitzian LinearOperator of S,U by LOPBAN_1:def 9;
for x, y being Element of S holds L . (x + y) = (L . x) + (L . y)
proof
let x, y be Element of S; :: thesis: L . (x + y) = (L . x) + (L . y)
A31: L . x = [(L1 . x),(L2 . x)] by A30;
A32: L . y = [(L1 . y),(L2 . y)] by A30;
A33: ( LL1 is additive & LL2 is additive ) ;
thus L . (x + y) = [(LL1 . (x + y)),(LL2 . (x + y))] by A30
.= [((LL1 . x) + (LL1 . y)),(LL2 . (x + y))] by A33
.= [((LL1 . x) + (LL1 . y)),((LL2 . x) + (LL2 . y))] by A33
.= (L . x) + (L . y) by A31, A32, PRVECT_3:18 ; :: thesis: verum
end;
then A34: 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: for a being Real holds L . (a * x) = a * (L . x)
let a be Real; :: thesis: L . (a * x) = a * (L . x)
A35: L . x = [(L1 . x),(L2 . x)] by A30;
thus L . (a * x) = [(LL1 . (a * x)),(LL2 . (a * x))] by A30
.= [(a * (LL1 . x)),(LL2 . (a * x))] by LOPBAN_1:def 5
.= [(a * (LL1 . x)),(a * (LL2 . x))] by LOPBAN_1:def 5
.= a * (L . x) by A35, PRVECT_3:18 ; :: thesis: verum
end;
then reconsider L = L as LinearOperator of S,[:T,U:] by A34, LOPBAN_1:def 5;
set K = ||.L1.|| + ||.L2.||;
( 0 <= ||.L1.|| & 0 <= ||.L2.|| ) by NORMSP_1:4;
then A36: 0 + 0 <= ||.L1.|| + ||.L2.|| by XREAL_1:7;
for w being VECTOR of S holds ||.(L . w).|| <= (||.L1.|| + ||.L2.||) * ||.w.||
proof
let w be Element of S; :: thesis: ||.(L . w).|| <= (||.L1.|| + ||.L2.||) * ||.w.||
A37: L . w = [(LL1 . w),(LL2 . w)] by A30;
A38: ||.(L . w).|| <= ||.(LL1 . w).|| + ||.(LL2 . w).|| by A37, Th17;
A39: ||.(LL1 . w).|| <= ||.L1.|| * ||.w.|| by LOPBAN_1:32;
A40: ||.(LL2 . w).|| <= ||.L2.|| * ||.w.|| by LOPBAN_1:32;
||.(LL1 . w).|| + ||.(LL2 . w).|| <= (||.L1.|| * ||.w.||) + (||.L2.|| * ||.w.||) by A39, A40, XREAL_1:7;
hence ||.(L . w).|| <= (||.L1.|| + ||.L2.||) * ||.w.|| by A38, XXREAL_0:2; :: thesis: verum
end;
then reconsider L = L as Lipschitzian LinearOperator of S,[:T,U:] by A36, LOPBAN_1:def 8;
reconsider L = L as Point of (R_NormSpace_of_BoundedLinearOperators (S,[:T,U:])) by LOPBAN_1:def 9;
consider N being Neighbourhood of x0 such that
A41: N c= N1 and
A42: N c= N2 by NDIFF_1:1;
A43: N c= dom f2 by A13, A42, XBOOLE_1:1;
N c= dom f1 by A9, A41, XBOOLE_1:1;
then N /\ N c= (dom f1) /\ (dom f2) by A43, XBOOLE_1:27;
then A44: N c= dom w by A3, FUNCT_3:def 7;
A45: now :: thesis: for x being Point of S st x in N holds
(w /. x) - (w /. x0) = (L . (x - x0)) + (R /. (x - x0))
let x be Point of S; :: thesis: ( x in N implies (w /. x) - (w /. x0) = (L . (x - x0)) + (R /. (x - x0)) )
A46: x0 in N by NFCONT_1:4;
assume A47: x in N ; :: thesis: (w /. x) - (w /. x0) = (L . (x - x0)) + (R /. (x - x0))
A48: L . (x - x0) = [(L1 . (x - x0)),(L2 . (x - x0))] by A30;
A49: R /. (x - x0) = [(R1 /. (x - x0)),(R2 /. (x - x0))] by A19;
A50: w /. x = [(f1 /. x),(f2 /. x)] by A5, A44, A47;
w /. x0 = [(f1 /. x0),(f2 /. x0)] by A5, A44, A46;
then - (w /. x0) = [(- (f1 /. x0)),(- (f2 /. x0))] by PRVECT_3:18;
hence (w /. x) - (w /. x0) = [((f1 /. x) - (f1 /. x0)),((f2 /. x) - (f2 /. x0))] by A50, PRVECT_3:18
.= [((L1 . (x - x0)) + (R1 /. (x - x0))),((f2 /. x) - (f2 /. x0))] by A11, A41, A47
.= [((L1 . (x - x0)) + (R1 /. (x - x0))),((L2 . (x - x0)) + (R2 /. (x - x0)))] by A15, A42, A47
.= (L . (x - x0)) + (R /. (x - x0)) by A48, A49, PRVECT_3:18 ;
:: thesis: verum
end;
hence w is_differentiable_in x0 by A44; :: thesis: ( diff (w,x0) = <:(diff (f1,x0)),(diff (f2,x0)):> & ( for dx being Point of S holds (diff (w,x0)) . dx = [((diff (f1,x0)) . dx),((diff (f2,x0)) . dx)] ) )
then A52: diff (w,x0) = L by A44, A45, NDIFF_1:def 7;
diff (f1,x0) is Lipschitzian LinearOperator of S,T by LOPBAN_1:def 9;
then A53: dom (diff (f1,x0)) = the carrier of S by FUNCT_2:def 1;
diff (f2,x0) is Lipschitzian LinearOperator of S,U by LOPBAN_1:def 9;
then A54: dom (diff (f2,x0)) = the carrier of S by FUNCT_2:def 1;
A55: diff (w,x0) is Lipschitzian LinearOperator of S,[:T,U:] by LOPBAN_1:def 9;
then A56: dom (diff (w,x0)) = the carrier of S by FUNCT_2:def 1;
dom (diff (w,x0)) = (dom (diff (f1,x0))) /\ (dom (diff (f2,x0))) by A53, A54, A55, FUNCT_2:def 1;
hence ( diff (w,x0) = <:(diff (f1,x0)),(diff (f2,x0)):> & ( for dx being Point of S holds (diff (w,x0)) . dx = [((diff (f1,x0)) . dx),((diff (f2,x0)) . dx)] ) ) by A12, A16, A30, A52, A56, FUNCT_3:def 7; :: thesis: verum