let S, T be RealNormSpace; :: thesis: for f being PartFunc of S,T
for p, q being Point of S
for M being Real st [.p,q.] c= dom f & ( for x being Point of S st x in [.p,q.] holds
f is_continuous_in x ) & ( for x being Point of S st x in ].p,q.[ holds
f is_differentiable_in x ) & ( for x being Point of S st x in ].p,q.[ holds
||.(diff (f,x)).|| <= M ) holds
||.((f /. q) - (f /. p)).|| <= M * ||.(q - p).||
let f be PartFunc of S,T; :: thesis: for p, q being Point of S
for M being Real st [.p,q.] c= dom f & ( for x being Point of S st x in [.p,q.] holds
f is_continuous_in x ) & ( for x being Point of S st x in ].p,q.[ holds
f is_differentiable_in x ) & ( for x being Point of S st x in ].p,q.[ holds
||.(diff (f,x)).|| <= M ) holds
||.((f /. q) - (f /. p)).|| <= M * ||.(q - p).||
let p, q be Point of S; :: thesis: for M being Real st [.p,q.] c= dom f & ( for x being Point of S st x in [.p,q.] holds
f is_continuous_in x ) & ( for x being Point of S st x in ].p,q.[ holds
f is_differentiable_in x ) & ( for x being Point of S st x in ].p,q.[ holds
||.(diff (f,x)).|| <= M ) holds
||.((f /. q) - (f /. p)).|| <= M * ||.(q - p).||
let M be Real; :: thesis: ( [.p,q.] c= dom f & ( for x being Point of S st x in [.p,q.] holds
f is_continuous_in x ) & ( for x being Point of S st x in ].p,q.[ holds
f is_differentiable_in x ) & ( for x being Point of S st x in ].p,q.[ holds
||.(diff (f,x)).|| <= M ) implies ||.((f /. q) - (f /. p)).|| <= M * ||.(q - p).|| )
assume A1: ( [.p,q.] c= dom f & ( for x being Point of S st x in [.p,q.] holds
f is_continuous_in x ) & ( for x being Point of S st x in ].p,q.[ holds
f is_differentiable_in x ) & ( for x being Point of S st x in ].p,q.[ holds
||.(diff (f,x)).|| <= M ) ) ; :: thesis: ||.((f /. q) - (f /. p)).|| <= M * ||.(q - p).||

per cases ( p = q or p <> q ) ;

suppose B2: p = q ; :: thesis: ||.((f /. q) - (f /. p)).|| <= M * ||.(q - p).||

B3: ||.((f /. q) - (f /. p)).|| = ||.(0. T).|| by B2, RLVECT_1:15
.= 0 ;
M * ||.(q - p).|| = M * ||.(0. S).|| by B2, RLVECT_1:15
.= 0 ;
hence ||.((f /. q) - (f /. p)).|| <= M * ||.(q - p).|| by B3; :: thesis: verum

end;

suppose p <> q ; :: thesis: ||.((f /. q) - (f /. p)).|| <= M * ||.(q - p).||

then X1: ].p,q.[ = { (p + (t * (q - p))) where t is Real : ( 0 < t & t < 1 ) } by LMOPN;
deffunc H₁( Real) -> Element of the carrier of S = ($1 * (q - p)) + p;
consider pt0 being Function of REAL, the carrier of S such that
A2: for t being Element of REAL holds pt0 . t = H₁(t) from FUNCT_2:sch 4();
A3: for t being Real holds pt0 . t = H₁(t)

proof

let t be Real; :: thesis: pt0 . t = H₁(t)
reconsider t = t as Element of REAL by XREAL_0:def 1;
pt0 . t = H₁(t) by A2;
hence pt0 . t = H₁(t) ; :: thesis: verum

end;

set pt = pt0 | [.0,1.];
A4: dom pt0 = REAL by FUNCT_2:def 1;
then A5: dom (pt0 | [.0,1.]) = [.0,1.] by RELAT_1:62;

A6: now :: thesis: for t being Real st t in [.0,1.] holds
pt0 /. t = (t * (q - p)) + p

let t be Real; :: thesis: ( t in [.0,1.] implies pt0 /. t = (t * (q - p)) + p )
assume t in [.0,1.] ; :: thesis: pt0 /. t = (t * (q - p)) + p
pt0 /. t = pt0 . t by A4, PARTFUN1:def 6, XREAL_0:def 1;
hence pt0 /. t = (t * (q - p)) + p by A3; :: thesis: verum

end;

A7: ].0,1.[ c= [.0,1.] by XXREAL_1:25;

A8: now :: thesis: for t being Real st t in ].0,1.[ holds
(pt0 | [.0,1.]) /. t = (t * (q - p)) + p

let t be Real; :: thesis: ( t in ].0,1.[ implies (pt0 | [.0,1.]) /. t = (t * (q - p)) + p )
assume t in ].0,1.[ ; :: thesis: (pt0 | [.0,1.]) /. t = (t * (q - p)) + p
hence (pt0 | [.0,1.]) /. t = pt0 /. t by A5, A7, PARTFUN2:15
.= pt0 . t by A4, PARTFUN1:def 6, XREAL_0:def 1
.= (t * (q - p)) + p by A3 ;
:: thesis: verum

end;

then A10: ( pt0 | [.0,1.] is_differentiable_on ].0,1.[ & ( for t being Real st t in ].0,1.[ holds
((pt0 | [.0,1.]) `| ].0,1.[) . t = q - p ) ) by A5, A7, NDIFF_3:21;
reconsider phi = f * (pt0 | [.0,1.]) as PartFunc of REAL,T ;
A11: rng (pt0 | [.0,1.]) c= [.p,q.]

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (pt0 | [.0,1.]) or y in [.p,q.] )
assume y in rng (pt0 | [.0,1.]) ; :: thesis: y in [.p,q.]
then consider x being object such that
A12: ( x in dom (pt0 | [.0,1.]) & y = (pt0 | [.0,1.]) . x ) by FUNCT_1:def 3;
A13: y = pt0 . x by A12, FUNCT_1:47;
reconsider x = x as Element of REAL by A12;
consider r being Real such that
A14: ( x = r & 0 <= r & r <= 1 ) by A12, A5;
y = p + (x * (q - p)) by A3, A13
.= ((1 - x) * p) + (x * q) by Lm2 ;
then y in { (((1 - r1) * p) + (r1 * q)) where r1 is Real : ( 0 <= r1 & r1 <= 1 ) } by A14;
hence y in [.p,q.] by RLTOPSP1:def 2; :: thesis: verum

end;

then rng (pt0 | [.0,1.]) c= dom f by A1;
then A15: dom phi = [.0,1.] by A5, RELAT_1:27;
A16: for t being Real st t in [.0,1.] holds
phi /. t = f /. (p + (t * (q - p)))

proof

let t be Real; :: thesis: ( t in [.0,1.] implies phi /. t = f /. (p + (t * (q - p))) )
assume A17: t in [.0,1.] ; :: thesis: phi /. t = f /. (p + (t * (q - p)))
then A18: phi /. t = phi . t by A15, PARTFUN1:def 6
.= f . ((pt0 | [.0,1.]) . t) by A17, A15, FUNCT_1:12 ;
A19: (pt0 | [.0,1.]) . t in rng (pt0 | [.0,1.]) by A17, A5, FUNCT_1:def 3;
(pt0 | [.0,1.]) . t = pt0 . t by A17, A5, FUNCT_1:47
.= p + (t * (q - p)) by A3 ;
hence phi /. t = f /. (p + (t * (q - p))) by A18, A11, A19, A1, PARTFUN1:def 6; :: thesis: verum

end;

now :: thesis: for x0 being Real st x0 in dom phi holds
phi is_continuous_in x0

let x0 be Real; :: thesis: ( x0 in dom phi implies phi is_continuous_in x0 )
assume A20: x0 in dom phi ; :: thesis: phi is_continuous_in x0
then A21: pt0 | [.0,1.] is_continuous_in x0 by A5, A6, A15, NFCONT_3:33, NFCONT_3:def 2;
(pt0 | [.0,1.]) . x0 in rng (pt0 | [.0,1.]) by A5, A20, A15, FUNCT_1:def 3;
then (pt0 | [.0,1.]) . x0 in [.p,q.] by A11;
then (pt0 | [.0,1.]) /. x0 in [.p,q.] by A20, A15, A5, PARTFUN1:def 6;
hence phi is_continuous_in x0 by A1, A20, A21, NFCONT_3:15; :: thesis: verum

end;

then phi is continuous by NFCONT_3:def 2;
then A22: phi | [.0,1.] is continuous ;

A23: now :: thesis: for x being Real st x in ].0,1.[ holds
( phi is_differentiable_in x & diff (phi,x) = (diff (f,(p + (x * (q - p))))) . (q - p) )

let x be Real; :: thesis: ( x in ].0,1.[ implies ( phi is_differentiable_in x & diff (phi,x) = (diff (f,(p + (x * (q - p))))) . (q - p) ) )
assume A24: x in ].0,1.[ ; :: thesis: ( phi is_differentiable_in x & diff (phi,x) = (diff (f,(p + (x * (q - p))))) . (q - p) )
then A25: pt0 | [.0,1.] is_differentiable_in x by A10, NDIFF_3:10;
((pt0 | [.0,1.]) `| ].0,1.[) . x = q - p by A24, A8, A5, A7, NDIFF_3:21;
then A26: diff ((pt0 | [.0,1.]),x) = q - p by A10, A24, NDIFF_3:def 6;
A27: (pt0 | [.0,1.]) . x = (pt0 | [.0,1.]) /. x by A24, A7, A5, PARTFUN1:def 6;
A28: ex r being Real st
( x = r & 0 < r & r < 1 ) by A24;
A29: (pt0 | [.0,1.]) . x = pt0 . x by A24, A7, A5, FUNCT_1:47;
A30: pt0 . x = p + (x * (q - p)) by A3;
(pt0 | [.0,1.]) . x in ].p,q.[ by X1, A28, A29, A30;
then A31: f is_differentiable_in (pt0 | [.0,1.]) /. x by A27, A1;
hence phi is_differentiable_in x by A25, Th6; :: thesis: diff (phi,x) = (diff (f,(p + (x * (q - p))))) . (q - p)
thus diff (phi,x) = (diff (f,(p + (x * (q - p))))) . (q - p) by A26, A27, A29, A30, A31, A25, Th6; :: thesis: verum

end;

then ( ].0,1.[ c= dom phi & ( for x being Real st x in ].0,1.[ holds
phi is_differentiable_in x ) ) by A15, XXREAL_1:25;
then A32: phi is_differentiable_on ].0,1.[ by NDIFF_3:10;
deffunc H₂( Real) -> Element of REAL = In (((M * ||.(q - p).||) * $1),REAL);
consider g0 being Function of REAL,REAL such that
A33: for t being Element of REAL holds g0 . t = H₂(t) from FUNCT_2:sch 4();
A34: for t being Real holds g0 . t = H₂(t)

proof

let t be Real; :: thesis: g0 . t = H₂(t)
reconsider t = t as Element of REAL by XREAL_0:def 1;
g0 . t = H₂(t) by A33;
hence g0 . t = H₂(t) ; :: thesis: verum

end;

set g = g0 | [.0,1.];
A35: for t being Real st t in [.0,1.] holds
g0 . t = ((M * ||.(q - p).||) * t) + 0

proof

let t be Real; :: thesis: ( t in [.0,1.] implies g0 . t = ((M * ||.(q - p).||) * t) + 0 )
assume t in [.0,1.] ; :: thesis: g0 . t = ((M * ||.(q - p).||) * t) + 0
thus g0 . t = H₂(t) by A34
.= ((M * ||.(q - p).||) * t) + 0 ; :: thesis: verum

end;

dom g0 = REAL by FUNCT_2:def 1;
then A36: dom (g0 | [.0,1.]) = [.0,1.] by RELAT_1:62;
A37: (g0 | [.0,1.]) | [.0,1.] is continuous by A35, FCONT_1:41;

A38: now :: thesis: for t being Real st t in ].0,1.[ holds
(g0 | [.0,1.]) . t = ((M * ||.(q - p).||) * t) + 0

let t be Real; :: thesis: ( t in ].0,1.[ implies (g0 | [.0,1.]) . t = ((M * ||.(q - p).||) * t) + 0 )
assume t in ].0,1.[ ; :: thesis: (g0 | [.0,1.]) . t = ((M * ||.(q - p).||) * t) + 0
hence (g0 | [.0,1.]) . t = g0 . t by A36, A7, FUNCT_1:47
.= H₂(t) by A34
.= ((M * ||.(q - p).||) * t) + 0 ;
:: thesis: verum

end;

then A39: ( g0 | [.0,1.] is_differentiable_on ].0,1.[ & ( for t being Real st t in ].0,1.[ holds
((g0 | [.0,1.]) `| ].0,1.[) . t = M * ||.(q - p).|| ) ) by A36, A7, FDIFF_1:23;
for t being Real st t in ].0,1.[ holds
||.(diff (phi,t)).|| <= diff ((g0 | [.0,1.]),t)

proof

let t be Real; :: thesis: ( t in ].0,1.[ implies ||.(diff (phi,t)).|| <= diff ((g0 | [.0,1.]),t) )
assume A40: t in ].0,1.[ ; :: thesis: ||.(diff (phi,t)).|| <= diff ((g0 | [.0,1.]),t)
then A41: ||.(diff (phi,t)).|| = ||.((diff (f,(p + (t * (q - p))))) . (q - p)).|| by A23;
reconsider L = diff (f,(p + (t * (q - p)))) as Lipschitzian LinearOperator of S,T by LOPBAN_1:def 9;
A42: ||.(L . (q - p)).|| <= ||.(diff (f,(p + (t * (q - p))))).|| * ||.(q - p).|| by LOPBAN_1:32;
A43: ex r being Real st
( t = r & 0 < r & r < 1 ) by A40;
p + (t * (q - p)) in ].p,q.[ by A43, X1;
then A44: ||.(diff (f,(p + (t * (q - p))))).|| * ||.(q - p).|| <= M * ||.(q - p).|| by A1, XREAL_1:64;
diff ((g0 | [.0,1.]),t) = ((g0 | [.0,1.]) `| ].0,1.[) . t by A40, A39, FDIFF_1:def 7;
then diff ((g0 | [.0,1.]),t) = M * ||.(q - p).|| by A40, A38, A36, A7, FDIFF_1:23;
hence ||.(diff (phi,t)).|| <= diff ((g0 | [.0,1.]),t) by A44, A42, A41, XXREAL_0:2; :: thesis: verum

end;

then A45: ||.((phi /. 1) - (phi /. 0)).|| <= ((g0 | [.0,1.]) /. 1) - ((g0 | [.0,1.]) /. 0) by Lm4, A15, A22, A32, A36, A37, A38, A7, FDIFF_1:23;
A46: ( 1 in [.0,1.] & 0 in [.0,1.] ) ;
then A47: (g0 | [.0,1.]) /. 1 = (g0 | [.0,1.]) . 1 by A36, PARTFUN1:def 6
.= g0 . 1 by A36, A46, FUNCT_1:47
.= H₂(1) by A34
.= (M * ||.(q - p).||) * 1 ;
A48: (g0 | [.0,1.]) /. 0 = (g0 | [.0,1.]) . 0 by A36, A46, PARTFUN1:def 6
.= g0 . 0 by A36, A46, FUNCT_1:47
.= H₂( 0 ) by A34
.= (M * ||.(q - p).||) * 0 ;
A49: phi /. 1 = f /. (p + (1 * (q - p))) by A16, A46
.= f /. (p + (q - p)) by RLVECT_1:def 8
.= f /. (q - (p - p)) by RLVECT_1:29
.= f /. (q - (0. S)) by RLVECT_1:15
.= f /. q by RLVECT_1:13 ;
phi /. 0 = f /. (p + (0 * (q - p))) by A16, A46
.= f /. (p + (0. S)) by RLVECT_1:10
.= f /. p by RLVECT_1:4 ;
hence ||.((f /. q) - (f /. p)).|| <= M * ||.(q - p).|| by A45, A47, A48, A49; :: thesis: verum

end;

end;