let S, E, F be RealNormSpace; :: thesis: for u being PartFunc of S,E
for v being PartFunc of S,F
for w being PartFunc of S,[:E,F:]
for Z being Subset of S
for i being Nat st w = <:u,v:> & u is_differentiable_on i + 1,Z & diff (u,(i + 1),Z) is_continuous_on Z & v is_differentiable_on i + 1,Z & diff (v,(i + 1),Z) is_continuous_on Z holds
( w is_differentiable_on i + 1,Z & diff (w,(i + 1),Z) is_continuous_on Z )
let u be PartFunc of S,E; :: thesis: for v being PartFunc of S,F
for w being PartFunc of S,[:E,F:]
for Z being Subset of S
for i being Nat st w = <:u,v:> & u is_differentiable_on i + 1,Z & diff (u,(i + 1),Z) is_continuous_on Z & v is_differentiable_on i + 1,Z & diff (v,(i + 1),Z) is_continuous_on Z holds
( w is_differentiable_on i + 1,Z & diff (w,(i + 1),Z) is_continuous_on Z )
let v be PartFunc of S,F; :: thesis: for w being PartFunc of S,[:E,F:]
for Z being Subset of S
for i being Nat st w = <:u,v:> & u is_differentiable_on i + 1,Z & diff (u,(i + 1),Z) is_continuous_on Z & v is_differentiable_on i + 1,Z & diff (v,(i + 1),Z) is_continuous_on Z holds
( w is_differentiable_on i + 1,Z & diff (w,(i + 1),Z) is_continuous_on Z )
let w be PartFunc of S,[:E,F:]; :: thesis: for Z being Subset of S
for i being Nat st w = <:u,v:> & u is_differentiable_on i + 1,Z & diff (u,(i + 1),Z) is_continuous_on Z & v is_differentiable_on i + 1,Z & diff (v,(i + 1),Z) is_continuous_on Z holds
( w is_differentiable_on i + 1,Z & diff (w,(i + 1),Z) is_continuous_on Z )
let Z be Subset of S; :: thesis: for i being Nat st w = <:u,v:> & u is_differentiable_on i + 1,Z & diff (u,(i + 1),Z) is_continuous_on Z & v is_differentiable_on i + 1,Z & diff (v,(i + 1),Z) is_continuous_on Z holds
( w is_differentiable_on i + 1,Z & diff (w,(i + 1),Z) is_continuous_on Z )
let i be Nat; :: thesis: ( w = <:u,v:> & u is_differentiable_on i + 1,Z & diff (u,(i + 1),Z) is_continuous_on Z & v is_differentiable_on i + 1,Z & diff (v,(i + 1),Z) is_continuous_on Z implies ( w is_differentiable_on i + 1,Z & diff (w,(i + 1),Z) is_continuous_on Z ) )
assume A1: w = <:u,v:> ; :: thesis: ( not u is_differentiable_on i + 1,Z or not diff (u,(i + 1),Z) is_continuous_on Z or not v is_differentiable_on i + 1,Z or not diff (v,(i + 1),Z) is_continuous_on Z or ( w is_differentiable_on i + 1,Z & diff (w,(i + 1),Z) is_continuous_on Z ) )
assume A2: ( u is_differentiable_on i + 1,Z & diff (u,(i + 1),Z) is_continuous_on Z & v is_differentiable_on i + 1,Z & diff (v,(i + 1),Z) is_continuous_on Z ) ; :: thesis: ( w is_differentiable_on i + 1,Z & diff (w,(i + 1),Z) is_continuous_on Z )
consider T being Lipschitzian LinearOperator of [:(diff_SP ((i + 1),S,E)),(diff_SP ((i + 1),S,F)):],(diff_SP ((i + 1),S,[:E,F:])) such that
A3: diff (w,(i + 1),Z) = T * <:(diff (u,(i + 1),Z)),(diff (v,(i + 1),Z)):> by A1, A2, Th60;
set E1 = diff_SP ((i + 1),S,E);
set F1 = diff_SP ((i + 1),S,F);
set u1 = diff (u,(i + 1),Z);
set v1 = diff (v,(i + 1),Z);
set G = <:(diff (u,(i + 1),Z)),(diff (v,(i + 1),Z)):>;
A4: ( diff (u,i,Z) is_differentiable_on Z & diff (v,i,Z) is_differentiable_on Z ) by A2, NDIFF_6:14;
diff (u,(i + 1),Z) = (diff (u,i,Z)) `| Z by NDIFF_6:13;
then A5: dom (diff (u,(i + 1),Z)) = Z by A4, NDIFF_1:def 9;
diff (v,(i + 1),Z) = (diff (v,i,Z)) `| Z by NDIFF_6:13;
then A6: dom (diff (v,(i + 1),Z)) = Z by A4, NDIFF_1:def 9;
A7: dom <:(diff (u,(i + 1),Z)),(diff (v,(i + 1),Z)):> = (dom (diff (u,(i + 1),Z))) /\ (dom (diff (v,(i + 1),Z))) by FUNCT_3:def 7
.= Z by A5, A6 ;
A8: [:(rng (diff (u,(i + 1),Z))),(rng (diff (v,(i + 1),Z))):] c= [#] [:(diff_SP ((i + 1),S,E)),(diff_SP ((i + 1),S,F)):] by ZFMISC_1:96;
rng <:(diff (u,(i + 1),Z)),(diff (v,(i + 1),Z)):> c= [:(rng (diff (u,(i + 1),Z))),(rng (diff (v,(i + 1),Z))):] by FUNCT_3:51;
then rng <:(diff (u,(i + 1),Z)),(diff (v,(i + 1),Z)):> c= [#] [:(diff_SP ((i + 1),S,E)),(diff_SP ((i + 1),S,F)):] by A8, XBOOLE_1:1;
then reconsider G = <:(diff (u,(i + 1),Z)),(diff (v,(i + 1),Z)):> as PartFunc of S,[:(diff_SP ((i + 1),S,E)),(diff_SP ((i + 1),S,F)):] by A7, RELSET_1:4;
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
||.((G /. x1) - (G /. x0)).|| < r ) )

proof

let z0 be Point of S; :: thesis: for r being Real st z0 in Z & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Point of S st x1 in Z & ||.(x1 - z0).|| < s holds
||.((G /. x1) - (G /. z0)).|| < r ) )
let r0 be Real; :: thesis: ( z0 in Z & 0 < r0 implies ex s being Real st
( 0 < s & ( for x1 being Point of S st x1 in Z & ||.(x1 - z0).|| < s holds
||.((G /. x1) - (G /. z0)).|| < r0 ) ) )
assume A9: ( z0 in Z & 0 < r0 ) ; :: thesis: ex s being Real st
( 0 < s & ( for x1 being Point of S st x1 in Z & ||.(x1 - z0).|| < s holds
||.((G /. x1) - (G /. z0)).|| < r0 ) )
set r = r0 / 2;
A10: for z being Point of S st z in Z holds
G /. z = [((diff (u,(i + 1),Z)) /. z),((diff (v,(i + 1),Z)) /. z)]

proof

let z be Point of S; :: thesis: ( z in Z implies G /. z = [((diff (u,(i + 1),Z)) /. z),((diff (v,(i + 1),Z)) /. z)] )
assume A11: z in Z ; :: thesis: G /. z = [((diff (u,(i + 1),Z)) /. z),((diff (v,(i + 1),Z)) /. z)]
hence G /. z = G . z by A7, PARTFUN1:def 6
.= [((diff (u,(i + 1),Z)) . z),((diff (v,(i + 1),Z)) . z)] by A7, A11, FUNCT_3:def 7
.= [((diff (u,(i + 1),Z)) /. z),((diff (v,(i + 1),Z)) . z)] by A5, A11, PARTFUN1:def 6
.= [((diff (u,(i + 1),Z)) /. z),((diff (v,(i + 1),Z)) /. z)] by A6, A11, PARTFUN1:def 6 ;
:: thesis: verum

end;

consider d1 being Real such that
A12: ( d1 > 0 & ( for z being Point of S st z in Z & ||.(z - z0).|| < d1 holds
||.(((diff (u,(i + 1),Z)) /. z) - ((diff (u,(i + 1),Z)) /. z0)).|| < r0 / 2 ) ) by A2, A9, NFCONT_1:19, XREAL_1:215;
consider d2 being Real such that
A13: ( d2 > 0 & ( for z being Point of S st z in Z & ||.(z - z0).|| < d2 holds
||.(((diff (v,(i + 1),Z)) /. z) - ((diff (v,(i + 1),Z)) /. z0)).|| < r0 / 2 ) ) by A2, A9, NFCONT_1:19, XREAL_1:215;
reconsider d = min (d1,d2) as Real ;
take d ; :: thesis: ( 0 < d & ( for x1 being Point of S st x1 in Z & ||.(x1 - z0).|| < d holds
||.((G /. x1) - (G /. z0)).|| < r0 ) )
thus 0 < d by A12, A13, XXREAL_0:15; :: thesis: for x1 being Point of S st x1 in Z & ||.(x1 - z0).|| < d holds
||.((G /. x1) - (G /. z0)).|| < r0
let z be Point of S; :: thesis: ( z in Z & ||.(z - z0).|| < d implies ||.((G /. z) - (G /. z0)).|| < r0 )
assume A14: ( z in Z & ||.(z - z0).|| < d ) ; :: thesis: ||.((G /. z) - (G /. z0)).|| < r0
d <= d1 by XXREAL_0:17;
then ||.(z - z0).|| < d1 by A14, XXREAL_0:2;
then A15: ||.(((diff (u,(i + 1),Z)) /. z) - ((diff (u,(i + 1),Z)) /. z0)).|| < r0 / 2 by A12, A14;
d <= d2 by XXREAL_0:17;
then ||.(z - z0).|| < d2 by A14, XXREAL_0:2;
then A16: ||.(((diff (v,(i + 1),Z)) /. z) - ((diff (v,(i + 1),Z)) /. z0)).|| < r0 / 2 by A13, A14;
A17: G /. z = [((diff (u,(i + 1),Z)) /. z),((diff (v,(i + 1),Z)) /. z)] by A10, A14;
G /. z0 = [((diff (u,(i + 1),Z)) /. z0),((diff (v,(i + 1),Z)) /. z0)] by A9, A10;
then - (G /. z0) = [(- ((diff (u,(i + 1),Z)) /. z0)),(- ((diff (v,(i + 1),Z)) /. z0))] by PRVECT_3:18;
then (G /. z) + (- (G /. z0)) = [(((diff (u,(i + 1),Z)) /. z) + (- ((diff (u,(i + 1),Z)) /. z0))),(((diff (v,(i + 1),Z)) /. z) + (- ((diff (v,(i + 1),Z)) /. z0)))] by A17, PRVECT_3:18;
then A18: ||.((G /. z) - (G /. z0)).|| <= ||.(((diff (u,(i + 1),Z)) /. z) - ((diff (u,(i + 1),Z)) /. z0)).|| + ||.(((diff (v,(i + 1),Z)) /. z) - ((diff (v,(i + 1),Z)) /. z0)).|| by Th17;
||.(((diff (u,(i + 1),Z)) /. z) - ((diff (u,(i + 1),Z)) /. z0)).|| + ||.(((diff (v,(i + 1),Z)) /. z) - ((diff (v,(i + 1),Z)) /. z0)).|| < (r0 / 2) + (r0 / 2) by A15, A16, XREAL_1:8;
hence ||.((G /. z) - (G /. z0)).|| < r0 by A18, XXREAL_0:2; :: thesis: verum

end;

then A19: G is_continuous_on Z by A7, NFCONT_1:19;
A20: G .: Z c= [#] [:(diff_SP ((i + 1),S,E)),(diff_SP ((i + 1),S,F)):] ;
T is_continuous_on [#] [:(diff_SP ((i + 1),S,E)),(diff_SP ((i + 1),S,F)):] by NDIFF_1:45, Th20;
hence ( w is_differentiable_on i + 1,Z & diff (w,(i + 1),Z) is_continuous_on Z ) by A1, A2, A3, A19, A20, Th16, Th60; :: thesis: verum