let Y be RealNormSpace; :: thesis:
let g be PartFunc of REAL, the carrier of Y; :: thesis:
let a, b, M be Real; :: thesis:
assume AS0: a <= b ; :: thesis:
assume AS1: [.a,b.] c= dom g ; :: thesis:
assume AS2: for x being Real st x in [.a,b.] holds
g is_continuous_in x ; :: thesis:
assume AS3: for x being Real st x in ].a,b.[ holds
g is_differentiable_in x ; :: thesis:
assume AS4: for x being Real st x in ].a,b.[ holds
||.(diff (g,x)).|| <= M ; :: thesis:
the carrier of (REAL-NS 1) = REAL 1 by REAL_NS1:def 4;
then reconsider J = proj (1,1) as Function of (REAL-NS 1),REAL ;
reconsider f = g * J as PartFunc of (REAL-NS 1),Y ;
reconsider I = (proj (1,1)) " as Function of REAL,(REAL-NS 1) by PDIFF_1:2, REAL_NS1:def 4;

now :: thesis:

let r be Real; :: thesis:
r is Element of REAL by XREAL_0:def 1;
then <*r*> in REAL 1 by FINSEQ_2:98;
hence <*r*> is Point of (REAL-NS 1) by REAL_NS1:def 4; :: thesis:

end;

then reconsider p = <*a*>, q = <*b*> as Point of (REAL-NS 1) ;
Y0: ].a,b.[ c= [.a,b.] by XXREAL_1:25;
DX1: J * I = id REAL by Lm2, FUNCT_1:39;
DX2: f * I = g * (id REAL) by DX1, RELAT_1:36
.= g by FUNCT_2:17 ;
dom f = J " (dom g) by RELAT_1:147
.= I .: (dom g) by FUNCT_1:85 ;
then I .: [.a,b.] c= dom f by AS1, RELAT_1:123;
then X0: [.p,q.] c= dom f by AS0, LM519D;
X1: for x being Point of (REAL-NS 1) st x in [.p,q.] holds
f is_continuous_in x

proof

let x be Point of (REAL-NS 1); :: thesis:
assume X11: x in [.p,q.] ; :: thesis:
consider z being Real such that
X12: x = <*z*> by LM519A;
z in [.a,b.] by AS0, LM519C1, X11, X12;
then g is_continuous_in z by AS2;
hence f is_continuous_in x by NDIFF435, X12, X0, X11; :: thesis:

end;

X2: for x being Point of (REAL-NS 1) st x in ].p,q.[ holds
f is_differentiable_in x

proof

let x be Point of (REAL-NS 1); :: thesis:
assume X11: x in ].p,q.[ ; :: thesis:
then X15: x in [.p,q.] by XBOOLE_0:def 5;
consider z being Real such that
X12: x = <*z*> by LM519A;

per cases ;

suppose a = b ; :: thesis:

hence f is_differentiable_in x by X11, X12, LM519B1; :: thesis:

end;

suppose a <> b ; :: thesis:

then a < b by AS0, XXREAL_0:1;
then z in ].a,b.[ by LM519B1, X11, X12;
then ( z in dom g & g is_differentiable_in z ) by AS1, Y0, AS3;
hence f is_differentiable_in x by FTh44, X12, X0, X15; :: thesis:

end;

end;

end;

X3: for x being Point of (REAL-NS 1) st x in ].p,q.[ holds
||.(diff (f,x)).|| <= M

proof

let x be Point of (REAL-NS 1); :: thesis:
assume X11: x in ].p,q.[ ; :: thesis:
then B11: x in [.p,q.] by XBOOLE_0:def 5;
consider z being Real such that
X12: x = <*z*> by LM519A;

per cases ;

suppose a = b ; :: thesis:

hence ||.(diff (f,x)).|| <= M by X11, X12, LM519B1; :: thesis:

end;

suppose a <> b ; :: thesis:

then a < b by AS0, XXREAL_0:1;
then X13: z in ].a,b.[ by LM519B1, X11, X12;
then X14: ||.(diff (g,z)).|| <= M by AS4;
f is_differentiable_in x by X2, X11;
hence ||.(diff (f,x)).|| <= M by B11, Y0, X0, X12, DX2, X14, FTh42A, AS1, X13; :: thesis:

end;

end;

end;

S0: dom I = REAL by FUNCT_2:def 1;
S1: ( p = I . a & q = I . b ) by PDIFF_1:1;
S2: ( p in dom f & q in dom f ) by X0, RLTOPSP1:68;
( a in [.a,b.] & b in [.a,b.] ) by AS0;
then ( g /. a = g . a & g /. b = g . b ) by PARTFUN1:def 6, AS1;
then ( g /. a = f . (I . a) & g /. b = f . (I . b) ) by DX2, FUNCT_1:13, S0, XREAL_0:def 1;
then S3: ( g /. a = f /. p & g /. b = f /. q ) by S1, S2, PARTFUN1:def 6;
q - p = I . (b - a) by S1, Lm1, PDIFF_1:3;
then ||.(q - p).|| = |.(b - a).| by Lm1, PDIFF_1:3;
hence ||.((g /. b) - (g /. a)).|| <= M * |.(b - a).| by NDIFF_5:19, X0, X1, X2, X3, S3; :: thesis: