let S, T, U be RealNormSpace; :: thesis: for Z being Subset 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_on Z & u `| Z is_continuous_on Z & v is_differentiable_on Z & v `| Z is_continuous_on Z & w = <:u,v:> holds
( w is_differentiable_on Z & w `| Z is_continuous_on Z )
let Z be Subset 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_on Z & u `| Z is_continuous_on Z & v is_differentiable_on Z & v `| Z is_continuous_on Z & w = <:u,v:> holds
( w is_differentiable_on Z & w `| Z is_continuous_on Z )
let u be PartFunc of S,T; :: thesis: for v being PartFunc of S,U
for w being PartFunc of S,[:T,U:] st u is_differentiable_on Z & u `| Z is_continuous_on Z & v is_differentiable_on Z & v `| Z is_continuous_on Z & w = <:u,v:> holds
( w is_differentiable_on Z & w `| Z is_continuous_on Z )
let v be PartFunc of S,U; :: thesis: for w being PartFunc of S,[:T,U:] st u is_differentiable_on Z & u `| Z is_continuous_on Z & v is_differentiable_on Z & v `| Z is_continuous_on Z & w = <:u,v:> holds
( w is_differentiable_on Z & w `| Z is_continuous_on Z )
let w be PartFunc of S,[:T,U:]; :: thesis: ( u is_differentiable_on Z & u `| Z is_continuous_on Z & v is_differentiable_on Z & v `| Z is_continuous_on Z & w = <:u,v:> implies ( w is_differentiable_on Z & w `| Z is_continuous_on Z ) )
assume A1: ( u is_differentiable_on Z & u `| Z is_continuous_on Z & v is_differentiable_on Z & v `| Z is_continuous_on Z & w = <:u,v:> ) ; :: thesis: ( w is_differentiable_on Z & w `| Z is_continuous_on Z )
then A2: ( w is_differentiable_on Z & ( for x being Point of S st x in Z holds
(w `| Z) /. x = <:((u `| Z) /. x),((v `| Z) /. x):> ) & ( 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)] ) ) by Th28;
thus w is_differentiable_on Z by A1, Th28; :: thesis: w `| Z is_continuous_on Z
A3: Z = dom (w `| Z) by A2, NDIFF_1:def 9;
set f = w `| Z;
set g = u `| Z;
set h = v `| Z;
for x0 being Point of S
for r being Real st x0 in Z & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Point of S st x1 in Z & ||.(x1 - x0).|| < s holds
||.(((w `| Z) /. x1) - ((w `| Z) /. x0)).|| < r ) )

proof

let x0 be Point of S; :: thesis: for r being Real st x0 in Z & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Point of S st x1 in Z & ||.(x1 - x0).|| < s holds
||.(((w `| Z) /. x1) - ((w `| Z) /. x0)).|| < r ) )
let r0 be Real; :: thesis: ( x0 in Z & 0 < r0 implies ex s being Real st
( 0 < s & ( for x1 being Point of S st x1 in Z & ||.(x1 - x0).|| < s holds
||.(((w `| Z) /. x1) - ((w `| Z) /. x0)).|| < r0 ) ) )
assume A4: ( x0 in Z & 0 < r0 ) ; :: thesis: ex s being Real st
( 0 < s & ( for x1 being Point of S st x1 in Z & ||.(x1 - x0).|| < s holds
||.(((w `| Z) /. x1) - ((w `| Z) /. x0)).|| < r0 ) )
set rr0 = r0 / 2;
A5: ( 0 < r0 / 2 & r0 / 2 < r0 ) by A4, XREAL_1:215, XREAL_1:216;
set r = (r0 / 2) / 2;
consider s1 being Real such that
A6: ( 0 < s1 & ( for x1 being Point of S st x1 in Z & ||.(x1 - x0).|| < s1 holds
||.(((u `| Z) /. x1) - ((u `| Z) /. x0)).|| < (r0 / 2) / 2 ) ) by A1, A4, A5, NFCONT_1:19, XREAL_1:215;
consider s2 being Real such that
A7: ( 0 < s2 & ( for x1 being Point of S st x1 in Z & ||.(x1 - x0).|| < s2 holds
||.(((v `| Z) /. x1) - ((v `| Z) /. x0)).|| < (r0 / 2) / 2 ) ) by A1, A4, A5, NFCONT_1:19, XREAL_1:215;
reconsider s = min (s1,s2) as Real ;
take s ; :: thesis: ( 0 < s & ( for x1 being Point of S st x1 in Z & ||.(x1 - x0).|| < s holds
||.(((w `| Z) /. x1) - ((w `| Z) /. x0)).|| < r0 ) )
thus 0 < s by A6, A7, XXREAL_0:15; :: thesis: for x1 being Point of S st x1 in Z & ||.(x1 - x0).|| < s holds
||.(((w `| Z) /. x1) - ((w `| Z) /. x0)).|| < r0
let x1 be Point of S; :: thesis: ( x1 in Z & ||.(x1 - x0).|| < s implies ||.(((w `| Z) /. x1) - ((w `| Z) /. x0)).|| < r0 )
assume A8: ( x1 in Z & ||.(x1 - x0).|| < s ) ; :: thesis: ||.(((w `| Z) /. x1) - ((w `| Z) /. x0)).|| < r0
s <= s1 by XXREAL_0:17;
then ||.(x1 - x0).|| < s1 by A8, XXREAL_0:2;
then A9: ||.(((u `| Z) /. x1) - ((u `| Z) /. x0)).|| < (r0 / 2) / 2 by A6, A8;
s <= s2 by XXREAL_0:17;
then ||.(x1 - x0).|| < s2 by A8, XXREAL_0:2;
then A10: ||.(((v `| Z) /. x1) - ((v `| Z) /. x0)).|| < (r0 / 2) / 2 by A7, A8;

A11: now :: thesis: for dx being Point of S holds ||.((((w `| Z) /. x1) - ((w `| Z) /. x0)) . dx).|| <= (2 * ((r0 / 2) / 2)) * ||.dx.||

let dx be Point of S; :: thesis: ||.((((w `| Z) /. x1) - ((w `| Z) /. x0)) . dx).|| <= (2 * ((r0 / 2) / 2)) * ||.dx.||
A12: (((w `| Z) /. x1) - ((w `| Z) /. x0)) . dx = (((w `| Z) /. x1) . dx) - (((w `| Z) /. x0) . dx) by LOPBAN_1:40;
A13: ((w `| Z) /. x0) . dx = [(((u `| Z) /. x0) . dx),(((v `| Z) /. x0) . dx)] by A1, A4, Th28;
A14: ((w `| Z) /. x1) . dx = [(((u `| Z) /. x1) . dx),(((v `| Z) /. x1) . dx)] by A1, A8, Th28;
- (((w `| Z) /. x0) . dx) = [(- (((u `| Z) /. x0) . dx)),(- (((v `| Z) /. x0) . dx))] by A13, PRVECT_3:18;
then (((w `| Z) /. x1) - ((w `| Z) /. x0)) . dx = [((((u `| Z) /. x1) . dx) - (((u `| Z) /. x0) . dx)),((((v `| Z) /. x1) . dx) - (((v `| Z) /. x0) . dx))] by A12, A14, PRVECT_3:18
.= [((((u `| Z) /. x1) - ((u `| Z) /. x0)) . dx),((((v `| Z) /. x1) . dx) - (((v `| Z) /. x0) . dx))] by LOPBAN_1:40
.= [((((u `| Z) /. x1) - ((u `| Z) /. x0)) . dx),((((v `| Z) /. x1) - ((v `| Z) /. x0)) . dx)] by LOPBAN_1:40 ;
then A15: ||.((((w `| Z) /. x1) - ((w `| Z) /. x0)) . dx).|| <= ||.((((u `| Z) /. x1) - ((u `| Z) /. x0)) . dx).|| + ||.((((v `| Z) /. x1) - ((v `| Z) /. x0)) . dx).|| by Th17;
reconsider g10 = ((u `| Z) /. x1) - ((u `| Z) /. x0) as Lipschitzian LinearOperator of S,T by LOPBAN_1:def 9;
||.((((u `| Z) /. x1) - ((u `| Z) /. x0)) . dx).|| = ||.(g10 . dx).|| ;
then A16: ||.((((u `| Z) /. x1) - ((u `| Z) /. x0)) . dx).|| <= ||.(((u `| Z) /. x1) - ((u `| Z) /. x0)).|| * ||.dx.|| by LOPBAN_1:32;
0 <= ||.dx.|| by NORMSP_1:4;
then ||.(((u `| Z) /. x1) - ((u `| Z) /. x0)).|| * ||.dx.|| <= ((r0 / 2) / 2) * ||.dx.|| by A9, XREAL_1:64;
then A17: ||.((((u `| Z) /. x1) - ((u `| Z) /. x0)) . dx).|| <= ((r0 / 2) / 2) * ||.dx.|| by A16, XXREAL_0:2;
reconsider h10 = ((v `| Z) /. x1) - ((v `| Z) /. x0) as Lipschitzian LinearOperator of S,U by LOPBAN_1:def 9;
||.((((v `| Z) /. x1) - ((v `| Z) /. x0)) . dx).|| = ||.(h10 . dx).|| ;
then A18: ||.((((v `| Z) /. x1) - ((v `| Z) /. x0)) . dx).|| <= ||.(((v `| Z) /. x1) - ((v `| Z) /. x0)).|| * ||.dx.|| by LOPBAN_1:32;
0 <= ||.dx.|| by NORMSP_1:4;
then ||.(((v `| Z) /. x1) - ((v `| Z) /. x0)).|| * ||.dx.|| <= ((r0 / 2) / 2) * ||.dx.|| by A10, XREAL_1:64;
then ||.((((v `| Z) /. x1) - ((v `| Z) /. x0)) . dx).|| <= ((r0 / 2) / 2) * ||.dx.|| by A18, XXREAL_0:2;
then ||.((((u `| Z) /. x1) - ((u `| Z) /. x0)) . dx).|| + ||.((((v `| Z) /. x1) - ((v `| Z) /. x0)) . dx).|| <= (((r0 / 2) / 2) * ||.dx.||) + (((r0 / 2) / 2) * ||.dx.||) by A17, XREAL_1:7;
hence ||.((((w `| Z) /. x1) - ((w `| Z) /. x0)) . dx).|| <= (2 * ((r0 / 2) / 2)) * ||.dx.|| by A15, XXREAL_0:2; :: thesis: verum

end;

reconsider f10 = ((w `| Z) /. x1) - ((w `| Z) /. x0) as Lipschitzian LinearOperator of S,[:T,U:] by LOPBAN_1:def 9;

now :: thesis: for s being Real st s in PreNorms f10 holds
s <= r0 / 2

let s be Real; :: thesis: ( s in PreNorms f10 implies s <= r0 / 2 )
assume s in PreNorms f10 ; :: thesis: s <= r0 / 2
then consider dx being VECTOR of S such that
A19: ( s = ||.(f10 . dx).|| & ||.dx.|| <= 1 ) ;
A20: s <= (r0 / 2) * ||.dx.|| by A19, A11;
(r0 / 2) * ||.dx.|| <= (r0 / 2) * 1 by A5, A19, XREAL_1:64;
hence s <= r0 / 2 by A20, XXREAL_0:2; :: thesis: verum

end;

then upper_bound (PreNorms f10) <= r0 / 2 by SEQ_4:45;
then ||.(((w `| Z) /. x1) - ((w `| Z) /. x0)).|| <= r0 / 2 by LOPBAN_1:30;
hence ||.(((w `| Z) /. x1) - ((w `| Z) /. x0)).|| < r0 by A5, XXREAL_0:2; :: thesis: verum

end;

hence w `| Z is_continuous_on Z by A3, NFCONT_1:19; :: thesis: verum