let E, F, G be RealNormSpace; :: thesis: for Z being Subset of E
for T being Subset of F
for u being PartFunc of E,F
for v being PartFunc of F,G st u .: Z c= T & u is_differentiable_on Z & u `| Z is_continuous_on Z & v is_differentiable_on T & v `| T is_continuous_on T holds
( v * u is_differentiable_on Z & (v * u) `| Z is_continuous_on Z )
let Z be Subset of E; :: thesis: for T being Subset of F
for u being PartFunc of E,F
for v being PartFunc of F,G st u .: Z c= T & u is_differentiable_on Z & u `| Z is_continuous_on Z & v is_differentiable_on T & v `| T is_continuous_on T holds
( v * u is_differentiable_on Z & (v * u) `| Z is_continuous_on Z )
let T be Subset of F; :: thesis: for u being PartFunc of E,F
for v being PartFunc of F,G st u .: Z c= T & u is_differentiable_on Z & u `| Z is_continuous_on Z & v is_differentiable_on T & v `| T is_continuous_on T holds
( v * u is_differentiable_on Z & (v * u) `| Z is_continuous_on Z )
let u be PartFunc of E,F; :: thesis: for v being PartFunc of F,G st u .: Z c= T & u is_differentiable_on Z & u `| Z is_continuous_on Z & v is_differentiable_on T & v `| T is_continuous_on T holds
( v * u is_differentiable_on Z & (v * u) `| Z is_continuous_on Z )
let v be PartFunc of F,G; :: thesis: ( u .: Z c= T & u is_differentiable_on Z & u `| Z is_continuous_on Z & v is_differentiable_on T & v `| T is_continuous_on T implies ( v * u is_differentiable_on Z & (v * u) `| Z is_continuous_on Z ) )
assume that
A1: u .: Z c= T and
A2: ( u is_differentiable_on Z & u `| Z is_continuous_on Z ) and
A3: ( v is_differentiable_on T & v `| T is_continuous_on T ) ; :: thesis: ( v * u is_differentiable_on Z & (v * u) `| Z is_continuous_on Z )
A4: u is_continuous_on Z by A2, NDIFF_1:45;
A5: ( v * u is_differentiable_on Z & ( for x being Point of E st x in Z holds
((v * u) `| Z) /. x = ((v `| T) /. (u /. x)) * ((u `| Z) /. x) ) ) by A1, A2, A3, Th19;
set f = (v * u) `| Z;
set g = u `| Z;
set h = v `| T;

A6: now :: thesis: for x0, x1 being Point of E st x0 in Z & x1 in Z holds
||.((((v * u) `| Z) /. x1) - (((v * u) `| Z) /. x0)).|| <= (||.(((v `| T) /. (u /. x1)) - ((v `| T) /. (u /. x0))).|| * ||.((u `| Z) /. x1).||) + (||.((v `| T) /. (u /. x0)).|| * ||.(((u `| Z) /. x1) - ((u `| Z) /. x0)).||)

let x0, x1 be Point of E; :: thesis: ( x0 in Z & x1 in Z implies ||.((((v * u) `| Z) /. x1) - (((v * u) `| Z) /. x0)).|| <= (||.(((v `| T) /. (u /. x1)) - ((v `| T) /. (u /. x0))).|| * ||.((u `| Z) /. x1).||) + (||.((v `| T) /. (u /. x0)).|| * ||.(((u `| Z) /. x1) - ((u `| Z) /. x0)).||) )
assume A7: ( x0 in Z & x1 in Z ) ; :: thesis: ||.((((v * u) `| Z) /. x1) - (((v * u) `| Z) /. x0)).|| <= (||.(((v `| T) /. (u /. x1)) - ((v `| T) /. (u /. x0))).|| * ||.((u `| Z) /. x1).||) + (||.((v `| T) /. (u /. x0)).|| * ||.(((u `| Z) /. x1) - ((u `| Z) /. x0)).||)

A8: now :: thesis: for dx being Point of E st ||.dx.|| <= 1 holds
||.(((((v * u) `| Z) /. x1) - (((v * u) `| Z) /. x0)) . dx).|| <= (||.(((v `| T) /. (u /. x1)) - ((v `| T) /. (u /. x0))).|| * ||.((u `| Z) /. x1).||) + (||.((v `| T) /. (u /. x0)).|| * ||.(((u `| Z) /. x1) - ((u `| Z) /. x0)).||)

let dx be Point of E; :: thesis: ( ||.dx.|| <= 1 implies ||.(((((v * u) `| Z) /. x1) - (((v * u) `| Z) /. x0)) . dx).|| <= (||.(((v `| T) /. (u /. x1)) - ((v `| T) /. (u /. x0))).|| * ||.((u `| Z) /. x1).||) + (||.((v `| T) /. (u /. x0)).|| * ||.(((u `| Z) /. x1) - ((u `| Z) /. x0)).||) )
assume A9: ||.dx.|| <= 1 ; :: thesis: ||.(((((v * u) `| Z) /. x1) - (((v * u) `| Z) /. x0)) . dx).|| <= (||.(((v `| T) /. (u /. x1)) - ((v `| T) /. (u /. x0))).|| * ||.((u `| Z) /. x1).||) + (||.((v `| T) /. (u /. x0)).|| * ||.(((u `| Z) /. x1) - ((u `| Z) /. x0)).||)
reconsider gx1 = (u `| Z) /. x1 as Lipschitzian LinearOperator of E,F by LOPBAN_1:def 9;
A10: dom gx1 = the carrier of E by FUNCT_2:def 1;
reconsider hux1 = (v `| T) /. (u /. x1) as Lipschitzian LinearOperator of F,G by LOPBAN_1:def 9;
reconsider hux0 = (v `| T) /. (u /. x0) as Lipschitzian LinearOperator of F,G by LOPBAN_1:def 9;
A11: modetrans (((v `| T) /. (u /. x1)),F,G) = hux1 by LOPBAN_1:def 11;
A12: hux0 is additive ;
A13: (((v * u) `| Z) /. x1) . dx = (((v `| T) /. (u /. x1)) * ((u `| Z) /. x1)) . dx by A1, A2, A3, A7, Th19
.= (hux1 * gx1) . dx by A11, LOPBAN_1:def 11
.= ((v `| T) /. (u /. x1)) . (((u `| Z) /. x1) . dx) by A10, FUNCT_1:13 ;
reconsider gx0 = (u `| Z) /. x0 as Lipschitzian LinearOperator of E,F by LOPBAN_1:def 9;
reconsider gx1 = (u `| Z) /. x1 as Lipschitzian LinearOperator of E,F by LOPBAN_1:def 9;
A14: dom gx0 = the carrier of E by FUNCT_2:def 1;
A15: modetrans (((u `| Z) /. x0),E,F) = gx0 by LOPBAN_1:def 11;
A16: (((v * u) `| Z) /. x0) . dx = (((v `| T) /. (u /. x0)) * ((u `| Z) /. x0)) . dx by A1, A2, A3, A7, Th19
.= (hux0 * gx0) . dx by A15, LOPBAN_1:def 11
.= ((v `| T) /. (u /. x0)) . (((u `| Z) /. x0) . dx) by A14, FUNCT_1:13 ;
A17: ((((v * u) `| Z) /. x1) - (((v * u) `| Z) /. x0)) . dx = ((((v * u) `| Z) /. x1) . dx) - ((((v * u) `| Z) /. x0) . dx) by LOPBAN_1:40
.= (((((v `| T) /. (u /. x1)) . (((u `| Z) /. x1) . dx)) - (((v `| T) /. (u /. x0)) . (((u `| Z) /. x1) . dx))) + (((v `| T) /. (u /. x0)) . (((u `| Z) /. x1) . dx))) - (((v `| T) /. (u /. x0)) . (((u `| Z) /. x0) . dx)) by A13, A16, RLVECT_4:1
.= ((((v `| T) /. (u /. x1)) . (((u `| Z) /. x1) . dx)) - (((v `| T) /. (u /. x0)) . (((u `| Z) /. x1) . dx))) + ((((v `| T) /. (u /. x0)) . (((u `| Z) /. x1) . dx)) - (((v `| T) /. (u /. x0)) . (((u `| Z) /. x0) . dx))) by RLVECT_1:28
.= ((((v `| T) /. (u /. x1)) - ((v `| T) /. (u /. x0))) . (((u `| Z) /. x1) . dx)) + ((((v `| T) /. (u /. x0)) . (((u `| Z) /. x1) . dx)) - (((v `| T) /. (u /. x0)) . (((u `| Z) /. x0) . dx))) by LOPBAN_1:40
.= ((((v `| T) /. (u /. x1)) - ((v `| T) /. (u /. x0))) . (((u `| Z) /. x1) . dx)) + ((((v `| T) /. (u /. x0)) . (((u `| Z) /. x1) . dx)) + ((- 1) * (((v `| T) /. (u /. x0)) . (((u `| Z) /. x0) . dx)))) by RLVECT_1:16
.= ((((v `| T) /. (u /. x1)) - ((v `| T) /. (u /. x0))) . (((u `| Z) /. x1) . dx)) + ((hux0 . (((u `| Z) /. x1) . dx)) + (hux0 . ((- 1) * (((u `| Z) /. x0) . dx)))) by LOPBAN_1:def 5
.= ((((v `| T) /. (u /. x1)) - ((v `| T) /. (u /. x0))) . (((u `| Z) /. x1) . dx)) + (hux0 . ((((u `| Z) /. x1) . dx) + ((- 1) * (((u `| Z) /. x0) . dx)))) by A12
.= ((((v `| T) /. (u /. x1)) - ((v `| T) /. (u /. x0))) . (((u `| Z) /. x1) . dx)) + (((v `| T) /. (u /. x0)) . ((((u `| Z) /. x1) . dx) - (((u `| Z) /. x0) . dx))) by RLVECT_1:16
.= ((((v `| T) /. (u /. x1)) - ((v `| T) /. (u /. x0))) . (((u `| Z) /. x1) . dx)) + (((v `| T) /. (u /. x0)) . ((((u `| Z) /. x1) - ((u `| Z) /. x0)) . dx)) by LOPBAN_1:40 ;
reconsider h10 = ((v `| T) /. (u /. x1)) - ((v `| T) /. (u /. x0)) as Lipschitzian LinearOperator of F,G by LOPBAN_1:def 9;
reconsider g10 = ((u `| Z) /. x1) - ((u `| Z) /. x0) as Lipschitzian LinearOperator of E,F by LOPBAN_1:def 9;
A18: ||.(((((v * u) `| Z) /. x1) - (((v * u) `| Z) /. x0)) . dx).|| <= ||.(h10 . (gx1 . dx)).|| + ||.(hux0 . (g10 . dx)).|| by A17, NORMSP_1:def 1;
A19: ||.(h10 . (gx1 . dx)).|| <= ||.(((v `| T) /. (u /. x1)) - ((v `| T) /. (u /. x0))).|| * ||.(gx1 . dx).|| by LOPBAN_1:32;
0 <= ||.(((v `| T) /. (u /. x1)) - ((v `| T) /. (u /. x0))).|| by NORMSP_1:4;
then ||.(((v `| T) /. (u /. x1)) - ((v `| T) /. (u /. x0))).|| * ||.(gx1 . dx).|| <= ||.(((v `| T) /. (u /. x1)) - ((v `| T) /. (u /. x0))).|| * (||.((u `| Z) /. x1).|| * ||.dx.||) by LOPBAN_1:32, XREAL_1:64;
then A20: ||.(h10 . (gx1 . dx)).|| <= (||.(((v `| T) /. (u /. x1)) - ((v `| T) /. (u /. x0))).|| * ||.((u `| Z) /. x1).||) * ||.dx.|| by A19, XXREAL_0:2;
A21: ||.(hux0 . (g10 . dx)).|| <= ||.((v `| T) /. (u /. x0)).|| * ||.(g10 . dx).|| by LOPBAN_1:32;
0 <= ||.((v `| T) /. (u /. x0)).|| by NORMSP_1:4;
then ||.((v `| T) /. (u /. x0)).|| * ||.(g10 . dx).|| <= ||.((v `| T) /. (u /. x0)).|| * (||.(((u `| Z) /. x1) - ((u `| Z) /. x0)).|| * ||.dx.||) by LOPBAN_1:32, XREAL_1:64;
then ||.(hux0 . (g10 . dx)).|| <= (||.((v `| T) /. (u /. x0)).|| * ||.(((u `| Z) /. x1) - ((u `| Z) /. x0)).||) * ||.dx.|| by A21, XXREAL_0:2;
then ||.(h10 . (gx1 . dx)).|| + ||.(hux0 . (g10 . dx)).|| <= ((||.(((v `| T) /. (u /. x1)) - ((v `| T) /. (u /. x0))).|| * ||.((u `| Z) /. x1).||) * ||.dx.||) + ((||.((v `| T) /. (u /. x0)).|| * ||.(((u `| Z) /. x1) - ((u `| Z) /. x0)).||) * ||.dx.||) by A20, XREAL_1:7;
then A22: ||.(((((v * u) `| Z) /. x1) - (((v * u) `| Z) /. x0)) . dx).|| <= ((||.(((v `| T) /. (u /. x1)) - ((v `| T) /. (u /. x0))).|| * ||.((u `| Z) /. x1).||) + (||.((v `| T) /. (u /. x0)).|| * ||.(((u `| Z) /. x1) - ((u `| Z) /. x0)).||)) * ||.dx.|| by A18, XXREAL_0:2;
( 0 <= ||.(((v `| T) /. (u /. x1)) - ((v `| T) /. (u /. x0))).|| & 0 <= ||.((u `| Z) /. x1).|| ) by NORMSP_1:4;
then A23: 0 * ||.((u `| Z) /. x1).|| <= ||.(((v `| T) /. (u /. x1)) - ((v `| T) /. (u /. x0))).|| * ||.((u `| Z) /. x1).|| by XREAL_1:64;
( 0 <= ||.((v `| T) /. (u /. x0)).|| & 0 <= ||.(((u `| Z) /. x1) - ((u `| Z) /. x0)).|| ) by NORMSP_1:4;
then 0 * ||.(((u `| Z) /. x1) - ((u `| Z) /. x0)).|| <= ||.((v `| T) /. (u /. x0)).|| * ||.(((u `| Z) /. x1) - ((u `| Z) /. x0)).|| by XREAL_1:64;
then 0 + 0 <= (||.(((v `| T) /. (u /. x1)) - ((v `| T) /. (u /. x0))).|| * ||.((u `| Z) /. x1).||) + (||.((v `| T) /. (u /. x0)).|| * ||.(((u `| Z) /. x1) - ((u `| Z) /. x0)).||) by A23, XREAL_1:7;
then ((||.(((v `| T) /. (u /. x1)) - ((v `| T) /. (u /. x0))).|| * ||.((u `| Z) /. x1).||) + (||.((v `| T) /. (u /. x0)).|| * ||.(((u `| Z) /. x1) - ((u `| Z) /. x0)).||)) * ||.dx.|| <= ((||.(((v `| T) /. (u /. x1)) - ((v `| T) /. (u /. x0))).|| * ||.((u `| Z) /. x1).||) + (||.((v `| T) /. (u /. x0)).|| * ||.(((u `| Z) /. x1) - ((u `| Z) /. x0)).||)) * 1 by A9, XREAL_1:64;
hence ||.(((((v * u) `| Z) /. x1) - (((v * u) `| Z) /. x0)) . dx).|| <= (||.(((v `| T) /. (u /. x1)) - ((v `| T) /. (u /. x0))).|| * ||.((u `| Z) /. x1).||) + (||.((v `| T) /. (u /. x0)).|| * ||.(((u `| Z) /. x1) - ((u `| Z) /. x0)).||) by A22, XXREAL_0:2; :: thesis: verum

end;

set K = (||.(((v `| T) /. (u /. x1)) - ((v `| T) /. (u /. x0))).|| * ||.((u `| Z) /. x1).||) + (||.((v `| T) /. (u /. x0)).|| * ||.(((u `| Z) /. x1) - ((u `| Z) /. x0)).||);
reconsider f10 = (((v * u) `| Z) /. x1) - (((v * u) `| Z) /. x0) as Lipschitzian LinearOperator of E,G by LOPBAN_1:def 9;
A24: ( ( for s being Real st s in PreNorms f10 holds
s <= (||.(((v `| T) /. (u /. x1)) - ((v `| T) /. (u /. x0))).|| * ||.((u `| Z) /. x1).||) + (||.((v `| T) /. (u /. x0)).|| * ||.(((u `| Z) /. x1) - ((u `| Z) /. x0)).||) ) implies upper_bound (PreNorms f10) <= (||.(((v `| T) /. (u /. x1)) - ((v `| T) /. (u /. x0))).|| * ||.((u `| Z) /. x1).||) + (||.((v `| T) /. (u /. x0)).|| * ||.(((u `| Z) /. x1) - ((u `| Z) /. x0)).||) ) by SEQ_4:45;

now :: thesis: for s being Real st s in PreNorms f10 holds
s <= (||.(((v `| T) /. (u /. x1)) - ((v `| T) /. (u /. x0))).|| * ||.((u `| Z) /. x1).||) + (||.((v `| T) /. (u /. x0)).|| * ||.(((u `| Z) /. x1) - ((u `| Z) /. x0)).||)

let s be Real; :: thesis: ( s in PreNorms f10 implies s <= (||.(((v `| T) /. (u /. x1)) - ((v `| T) /. (u /. x0))).|| * ||.((u `| Z) /. x1).||) + (||.((v `| T) /. (u /. x0)).|| * ||.(((u `| Z) /. x1) - ((u `| Z) /. x0)).||) )
assume s in PreNorms f10 ; :: thesis: s <= (||.(((v `| T) /. (u /. x1)) - ((v `| T) /. (u /. x0))).|| * ||.((u `| Z) /. x1).||) + (||.((v `| T) /. (u /. x0)).|| * ||.(((u `| Z) /. x1) - ((u `| Z) /. x0)).||)
then consider dx being VECTOR of E such that
A25: ( s = ||.(f10 . dx).|| & ||.dx.|| <= 1 ) ;
thus s <= (||.(((v `| T) /. (u /. x1)) - ((v `| T) /. (u /. x0))).|| * ||.((u `| Z) /. x1).||) + (||.((v `| T) /. (u /. x0)).|| * ||.(((u `| Z) /. x1) - ((u `| Z) /. x0)).||) by A8, A25; :: thesis: verum

end;

hence ||.((((v * u) `| Z) /. x1) - (((v * u) `| Z) /. x0)).|| <= (||.(((v `| T) /. (u /. x1)) - ((v `| T) /. (u /. x0))).|| * ||.((u `| Z) /. x1).||) + (||.((v `| T) /. (u /. x0)).|| * ||.(((u `| Z) /. x1) - ((u `| Z) /. x0)).||) by A24, LOPBAN_1:30; :: thesis: verum

end;

A26: Z = dom ((v * u) `| Z) by A5, NDIFF_1:def 9;
for x0 being Point of E
for r being Real st x0 in Z & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Point of E st x1 in Z & ||.(x1 - x0).|| < s holds
||.((((v * u) `| Z) /. x1) - (((v * u) `| Z) /. x0)).|| < r ) )

proof

let x0 be Point of E; :: thesis: for r being Real st x0 in Z & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Point of E st x1 in Z & ||.(x1 - x0).|| < s holds
||.((((v * u) `| Z) /. x1) - (((v * u) `| Z) /. x0)).|| < r ) )
let r be Real; :: thesis: ( x0 in Z & 0 < r implies ex s being Real st
( 0 < s & ( for x1 being Point of E st x1 in Z & ||.(x1 - x0).|| < s holds
||.((((v * u) `| Z) /. x1) - (((v * u) `| Z) /. x0)).|| < r ) ) )
assume A27: ( x0 in Z & 0 < r ) ; :: thesis: ex s being Real st
( 0 < s & ( for x1 being Point of E st x1 in Z & ||.(x1 - x0).|| < s holds
||.((((v * u) `| Z) /. x1) - (((v * u) `| Z) /. x0)).|| < r ) )
set r0 = r / 2;
A28: ( 0 < r / 2 & r / 2 < r ) by A27, XREAL_1:215, XREAL_1:216;
set r1 = (r / 2) / 2;
A29: ( 0 < (r / 2) / 2 & (r / 2) / 2 < r / 2 ) by A28, XREAL_1:215, XREAL_1:216;
consider s10 being Real such that
A30: ( 0 < s10 & ( for x1 being Point of E st x1 in Z & ||.(x1 - x0).|| < s10 holds
||.(((u `| Z) /. x1) - ((u `| Z) /. x0)).|| < 1 ) ) by A2, A27, NFCONT_1:19;

A31: now :: thesis: for x1 being Point of E st x1 in Z & ||.(x1 - x0).|| < s10 holds
||.((u `| Z) /. x1).|| <= 1 + ||.((u `| Z) /. x0).||

let x1 be Point of E; :: thesis: ( x1 in Z & ||.(x1 - x0).|| < s10 implies ||.((u `| Z) /. x1).|| <= 1 + ||.((u `| Z) /. x0).|| )
assume ( x1 in Z & ||.(x1 - x0).|| < s10 ) ; :: thesis: ||.((u `| Z) /. x1).|| <= 1 + ||.((u `| Z) /. x0).||
then A32: ||.(((u `| Z) /. x1) - ((u `| Z) /. x0)).|| < 1 by A30;
(u `| Z) /. x1 = (((u `| Z) /. x1) - ((u `| Z) /. x0)) + ((u `| Z) /. x0) by RLVECT_4:1;
then A33: ||.((u `| Z) /. x1).|| <= ||.(((u `| Z) /. x1) - ((u `| Z) /. x0)).|| + ||.((u `| Z) /. x0).|| by NORMSP_1:def 1;
||.(((u `| Z) /. x1) - ((u `| Z) /. x0)).|| + ||.((u `| Z) /. x0).|| <= 1 + ||.((u `| Z) /. x0).|| by A32, XREAL_1:7;
hence ||.((u `| Z) /. x1).|| <= 1 + ||.((u `| Z) /. x0).|| by A33, XXREAL_0:2; :: thesis: verum

end;

A34: 0 + 0 < 1 + ||.((u `| Z) /. x0).|| by XREAL_1:8, NORMSP_1:4;
set r10 = ((r / 2) / 2) / (1 + ||.((u `| Z) /. x0).||);
u . x0 in u .: Z by A2, A27, FUNCT_1:def 6;
then u . x0 in T by A1;
then u /. x0 in T by A2, A27, PARTFUN1:def 6;
then consider d being Real such that
A35: ( 0 < d & ( for y1 being Point of F st y1 in T & ||.(y1 - (u /. x0)).|| < d holds
||.(((v `| T) /. y1) - ((v `| T) /. (u /. x0))).|| < ((r / 2) / 2) / (1 + ||.((u `| Z) /. x0).||) ) ) by A3, A29, A34, XREAL_1:139, NFCONT_1:19;
consider s11 being Real such that
A36: ( 0 < s11 & ( for x1 being Point of E st x1 in Z & ||.(x1 - x0).|| < s11 holds
||.((u /. x1) - (u /. x0)).|| < d ) ) by A4, A27, A35, NFCONT_1:19;

A37: now :: thesis: for x1 being Point of E st x1 in Z & ||.(x1 - x0).|| < s11 holds
||.(((v `| T) /. (u /. x1)) - ((v `| T) /. (u /. x0))).|| < ((r / 2) / 2) / (1 + ||.((u `| Z) /. x0).||)

let x1 be Point of E; :: thesis: ( x1 in Z & ||.(x1 - x0).|| < s11 implies ||.(((v `| T) /. (u /. x1)) - ((v `| T) /. (u /. x0))).|| < ((r / 2) / 2) / (1 + ||.((u `| Z) /. x0).||) )
assume A38: ( x1 in Z & ||.(x1 - x0).|| < s11 ) ; :: thesis: ||.(((v `| T) /. (u /. x1)) - ((v `| T) /. (u /. x0))).|| < ((r / 2) / 2) / (1 + ||.((u `| Z) /. x0).||)
then A39: ||.((u /. x1) - (u /. x0)).|| < d by A36;
u . x1 in u .: Z by A2, A38, FUNCT_1:def 6;
then u . x1 in T by A1;
then u /. x1 in T by A2, A38, PARTFUN1:def 6;
hence ||.(((v `| T) /. (u /. x1)) - ((v `| T) /. (u /. x0))).|| < ((r / 2) / 2) / (1 + ||.((u `| Z) /. x0).||) by A35, A39; :: thesis: verum

end;

reconsider s1 = min (s10,s11) as Real ;
A40: ( 0 < s1 & ( for x1 being Point of E st x1 in Z & ||.(x1 - x0).|| < s1 holds
||.(((v `| T) /. (u /. x1)) - ((v `| T) /. (u /. x0))).|| * ||.((u `| Z) /. x1).|| <= (r / 2) / 2 ) )

proof

thus 0 < s1 by A30, A36, XXREAL_0:15; :: thesis: for x1 being Point of E st x1 in Z & ||.(x1 - x0).|| < s1 holds
||.(((v `| T) /. (u /. x1)) - ((v `| T) /. (u /. x0))).|| * ||.((u `| Z) /. x1).|| <= (r / 2) / 2
let x1 be Point of E; :: thesis: ( x1 in Z & ||.(x1 - x0).|| < s1 implies ||.(((v `| T) /. (u /. x1)) - ((v `| T) /. (u /. x0))).|| * ||.((u `| Z) /. x1).|| <= (r / 2) / 2 )
assume A41: ( x1 in Z & ||.(x1 - x0).|| < s1 ) ; :: thesis: ||.(((v `| T) /. (u /. x1)) - ((v `| T) /. (u /. x0))).|| * ||.((u `| Z) /. x1).|| <= (r / 2) / 2
s1 <= s10 by XXREAL_0:17;
then ||.(x1 - x0).|| < s10 by A41, XXREAL_0:2;
then A42: ||.((u `| Z) /. x1).|| <= 1 + ||.((u `| Z) /. x0).|| by A31, A41;
s1 <= s11 by XXREAL_0:17;
then ||.(x1 - x0).|| < s11 by A41, XXREAL_0:2;
then A43: ||.(((v `| T) /. (u /. x1)) - ((v `| T) /. (u /. x0))).|| < ((r / 2) / 2) / (1 + ||.((u `| Z) /. x0).||) by A37, A41;
( 0 <= ||.((u `| Z) /. x1).|| & 0 <= ||.(((v `| T) /. (u /. x1)) - ((v `| T) /. (u /. x0))).|| ) by NORMSP_1:4;
then ||.(((v `| T) /. (u /. x1)) - ((v `| T) /. (u /. x0))).|| * ||.((u `| Z) /. x1).|| <= (((r / 2) / 2) / (1 + ||.((u `| Z) /. x0).||)) * (1 + ||.((u `| Z) /. x0).||) by A42, A43, XREAL_1:66;
hence ||.(((v `| T) /. (u /. x1)) - ((v `| T) /. (u /. x0))).|| * ||.((u `| Z) /. x1).|| <= (r / 2) / 2 by A34, XCMPLX_1:87; :: thesis: verum

end;

A44: 0 + 0 < 1 + ||.((v `| T) /. (u /. x0)).|| by NORMSP_1:4, XREAL_1:8;
set r10 = ((r / 2) / 2) / (1 + ||.((v `| T) /. (u /. x0)).||);
A45: 0 < ((r / 2) / 2) / (1 + ||.((v `| T) /. (u /. x0)).||) by A29, A44, XREAL_1:139;
consider s2 being Real such that
A46: ( 0 < s2 & ( for x1 being Point of E st x1 in Z & ||.(x1 - x0).|| < s2 holds
||.(((u `| Z) /. x1) - ((u `| Z) /. x0)).|| < ((r / 2) / 2) / (1 + ||.((v `| T) /. (u /. x0)).||) ) ) by A2, A27, A29, A44, NFCONT_1:19, XREAL_1:139;
A47: ( 0 < s2 & ( for x1 being Point of E st x1 in Z & ||.(x1 - x0).|| < s2 holds
||.((v `| T) /. (u /. x0)).|| * ||.(((u `| Z) /. x1) - ((u `| Z) /. x0)).|| <= (r / 2) / 2 ) )

proof

thus 0 < s2 by A46; :: thesis: for x1 being Point of E st x1 in Z & ||.(x1 - x0).|| < s2 holds
||.((v `| T) /. (u /. x0)).|| * ||.(((u `| Z) /. x1) - ((u `| Z) /. x0)).|| <= (r / 2) / 2
let x1 be Point of E; :: thesis: ( x1 in Z & ||.(x1 - x0).|| < s2 implies ||.((v `| T) /. (u /. x0)).|| * ||.(((u `| Z) /. x1) - ((u `| Z) /. x0)).|| <= (r / 2) / 2 )
assume ( x1 in Z & ||.(x1 - x0).|| < s2 ) ; :: thesis: ||.((v `| T) /. (u /. x0)).|| * ||.(((u `| Z) /. x1) - ((u `| Z) /. x0)).|| <= (r / 2) / 2
then A48: ||.(((u `| Z) /. x1) - ((u `| Z) /. x0)).|| < ((r / 2) / 2) / (1 + ||.((v `| T) /. (u /. x0)).||) by A46;
( 0 <= ||.(((u `| Z) /. x1) - ((u `| Z) /. x0)).|| & 0 <= ||.((v `| T) /. (u /. x0)).|| ) by NORMSP_1:4;
then A49: ||.((v `| T) /. (u /. x0)).|| * ||.(((u `| Z) /. x1) - ((u `| Z) /. x0)).|| <= ||.((v `| T) /. (u /. x0)).|| * (((r / 2) / 2) / (1 + ||.((v `| T) /. (u /. x0)).||)) by A48, XREAL_1:64;
0 + ||.((v `| T) /. (u /. x0)).|| <= ||.((v `| T) /. (u /. x0)).|| + 1 by XREAL_1:7;
then ||.((v `| T) /. (u /. x0)).|| * (((r / 2) / 2) / (1 + ||.((v `| T) /. (u /. x0)).||)) <= (||.((v `| T) /. (u /. x0)).|| + 1) * (((r / 2) / 2) / (1 + ||.((v `| T) /. (u /. x0)).||)) by A45, XREAL_1:64;
then ||.((v `| T) /. (u /. x0)).|| * (((r / 2) / 2) / (1 + ||.((v `| T) /. (u /. x0)).||)) <= (r / 2) / 2 by A44, XCMPLX_1:87;
hence ||.((v `| T) /. (u /. x0)).|| * ||.(((u `| Z) /. x1) - ((u `| Z) /. x0)).|| <= (r / 2) / 2 by A49, XXREAL_0:2; :: thesis: verum

end;

reconsider s = min (s1,s2) as Real ;
take s ; :: thesis: ( 0 < s & ( for x1 being Point of E st x1 in Z & ||.(x1 - x0).|| < s holds
||.((((v * u) `| Z) /. x1) - (((v * u) `| Z) /. x0)).|| < r ) )
thus 0 < s by A40, A47, XXREAL_0:15; :: thesis: for x1 being Point of E st x1 in Z & ||.(x1 - x0).|| < s holds
||.((((v * u) `| Z) /. x1) - (((v * u) `| Z) /. x0)).|| < r
let x1 be Point of E; :: thesis: ( x1 in Z & ||.(x1 - x0).|| < s implies ||.((((v * u) `| Z) /. x1) - (((v * u) `| Z) /. x0)).|| < r )
assume A50: ( x1 in Z & ||.(x1 - x0).|| < s ) ; :: thesis: ||.((((v * u) `| Z) /. x1) - (((v * u) `| Z) /. x0)).|| < r
s <= s1 by XXREAL_0:17;
then ||.(x1 - x0).|| < s1 by A50, XXREAL_0:2;
then A51: ||.(((v `| T) /. (u /. x1)) - ((v `| T) /. (u /. x0))).|| * ||.((u `| Z) /. x1).|| <= (r / 2) / 2 by A40, A50;
s <= s2 by XXREAL_0:17;
then ||.(x1 - x0).|| < s2 by A50, XXREAL_0:2;
then ||.((v `| T) /. (u /. x0)).|| * ||.(((u `| Z) /. x1) - ((u `| Z) /. x0)).|| <= (r / 2) / 2 by A47, A50;
then A52: (||.(((v `| T) /. (u /. x1)) - ((v `| T) /. (u /. x0))).|| * ||.((u `| Z) /. x1).||) + (||.((v `| T) /. (u /. x0)).|| * ||.(((u `| Z) /. x1) - ((u `| Z) /. x0)).||) <= ((r / 2) / 2) + ((r / 2) / 2) by A51, XREAL_1:7;
||.((((v * u) `| Z) /. x1) - (((v * u) `| Z) /. x0)).|| <= (||.(((v `| T) /. (u /. x1)) - ((v `| T) /. (u /. x0))).|| * ||.((u `| Z) /. x1).||) + (||.((v `| T) /. (u /. x0)).|| * ||.(((u `| Z) /. x1) - ((u `| Z) /. x0)).||) by A6, A27, A50;
then ||.((((v * u) `| Z) /. x1) - (((v * u) `| Z) /. x0)).|| <= r / 2 by A52, XXREAL_0:2;
hence ||.((((v * u) `| Z) /. x1) - (((v * u) `| Z) /. x0)).|| < r by A28, XXREAL_0:2; :: thesis: verum

end;

hence ( v * u is_differentiable_on Z & (v * u) `| Z is_continuous_on Z ) by A1, A2, A3, A26, Th19, NFCONT_1:19; :: thesis: verum