let a, b, c be Real; :: thesis: for f, g, h, F being Function of REAL,REAL st a <= b & b <= c & f is continuous & g is continuous & h | [.a,c.] = (f | [.a,b.]) +* (g | [.b,c.]) & f . b = g . b & F = h | [.a,c.] holds
F is continuous
let f, g, h, F be Function of REAL,REAL; :: thesis: ( a <= b & b <= c & f is continuous & g is continuous & h | [.a,c.] = (f | [.a,b.]) +* (g | [.b,c.]) & f . b = g . b & F = h | [.a,c.] implies F is continuous )
assume that
A1: ( a <= b & b <= c ) and
A2: ( f is continuous & g is continuous ) and
A3: h | [.a,c.] = (f | [.a,b.]) +* (g | [.b,c.]) and
A4: f . b = g . b and
A99: F = h | [.a,c.] ; :: thesis: F is continuous
A6: ( dom f = REAL & dom g = REAL ) by FUNCT_2:def 1;
A5a: dom h = REAL by FUNCT_2:def 1;
DGG: dom (g | [.b,c.]) = [.b,c.] by FUNCT_2:def 1;
Bin: ( b in [.a,b.] & b in [.b,c.] ) by A1;
reconsider f = f as PartFunc of REAL,REAL ;
reconsider g = g as PartFunc of REAL,REAL ;
reconsider h = h as PartFunc of REAL,REAL ;
A2a: ( f | [.a,b.] is continuous & g | [.b,c.] is continuous ) by A2;
for x0, r being Real st x0 in [.a,c.] & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Real st x1 in [.a,c.] & |.(x1 - x0).| < s holds
|.((h . x1) - (h . x0)).| < r ) )

proof

let x0, r be Real; :: thesis: ( x0 in [.a,c.] & 0 < r implies ex s being Real st
( 0 < s & ( for x1 being Real st x1 in [.a,c.] & |.(x1 - x0).| < s holds
|.((h . x1) - (h . x0)).| < r ) ) )
assume P1a: x0 in [.a,c.] ; :: thesis: ( not 0 < r or ex s being Real st
( 0 < s & ( for x1 being Real st x1 in [.a,c.] & |.(x1 - x0).| < s holds
|.((h . x1) - (h . x0)).| < r ) ) )
assume P2: 0 < r ; :: thesis: ex s being Real st
( 0 < s & ( for x1 being Real st x1 in [.a,c.] & |.(x1 - x0).| < s holds
|.((h . x1) - (h . x0)).| < r ) )
P1: ( a <= x0 & x0 <= c ) by P1a, XXREAL_1:1;
ex s being Real st
( 0 < s & ( for x1 being Real st x1 in [.a,c.] & |.(x1 - x0).| < s holds
|.((h . x1) - (h . x0)).| < r ) )

proof

per cases ( x0 < b or b <= x0 ) ;

suppose B1: x0 < b ; :: thesis: ex s being Real st
( 0 < s & ( for x1 being Real st x1 in [.a,c.] & |.(x1 - x0).| < s holds
|.((h . x1) - (h . x0)).| < r ) )

then B1a: x0 in [.a,b.] by P1;
then consider sf being Real such that
P3: 0 < sf and
P4: for x1 being Real st x1 in [.a,b.] & |.(x1 - x0).| < sf holds
|.((f . x1) - (f . x0)).| < r / 2 by P2, FCONT_1:14, A2a, A6;
consider sg being Real such that
Q1: 0 < sg and
Q2: for x1 being Real st x1 in [.b,c.] & |.(x1 - b).| < sg holds
|.((g . x1) - (g . b)).| < r / 2 by P2, Bin, FCONT_1:14, A2a, A6;
take min (sf,sg) ; :: thesis: ( 0 < min (sf,sg) & ( for x1 being Real st x1 in [.a,c.] & |.(x1 - x0).| < min (sf,sg) holds
|.((h . x1) - (h . x0)).| < r ) )
for x1 being Real st x1 in [.a,c.] & |.(x1 - x0).| < min (sf,sg) holds
|.((h . x1) - (h . x0)).| < r

proof

let x1 be Real; :: thesis: ( x1 in [.a,c.] & |.(x1 - x0).| < min (sf,sg) implies |.((h . x1) - (h . x0)).| < r )
assume that
P5: x1 in [.a,c.] and
P6: |.(x1 - x0).| < min (sf,sg) ; :: thesis: |.((h . x1) - (h . x0)).| < r
RMin: ( min (sf,sg) <= sf & min (sf,sg) <= sg ) by XXREAL_0:17;
P5a: ( a <= x1 & x1 <= c ) by P5, XXREAL_1:1;

per cases ( x1 >= b or x1 < b ) ;

suppose R1: x1 >= b ; :: thesis: |.((h . x1) - (h . x0)).| < r

then R2: x1 in [.b,c.] by P5a;
R1a: x1 - b >= b - b by XREAL_1:13, R1;
then x1 - x0 > 0 by B1, XREAL_1:15;
then R4: ( x1 - b = |.(x1 - b).| & |.(x1 - x0).| = x1 - x0 ) by R1a, COMPLEX1:43;
then |.(x1 - b).| < |.(x1 - x0).| by B1, XREAL_1:15;
then |.(x1 - b).| < min (sf,sg) by P6, XXREAL_0:2;
then |.(x1 - b).| < sg by RMin, XXREAL_0:2;
then R6: |.((g . x1) - (g . b)).| < r / 2 by R2, Q2;
b - x0 > x0 - x0 by B1, XREAL_1:14;
then R7b: b - x0 = |.(b - x0).| by COMPLEX1:43;
|.(b - x0).| <= |.(x1 - x0).| by R1, XREAL_1:9, R7b, R4;
then |.(b - x0).| < min (sf,sg) by P6, XXREAL_0:2;
then |.(b - x0).| < sf by RMin, XXREAL_0:2;
then R7: |.((f . b) - (f . x0)).| < r / 2 by Bin, P4;
G1i: x1 in dom (g | [.b,c.]) by R1, P5a, DGG;
G0n: not x0 in dom (g | [.b,c.]) by DGG, B1, XXREAL_1:1;
R8: |.(((g . x1) - (g . b)) + ((f . b) - (f . x0))).| <= |.((g . x1) - (g . b)).| + |.((f . b) - (f . x0)).| by COMPLEX1:56;
R99: |.((g . x1) - (g . b)).| + |.((f . b) - (f . x0)).| < (r / 2) + (r / 2) by R7, R6, XREAL_1:8;
|.((h . x1) - (h . x0)).| = |.((((f | [.a,b.]) +* (g | [.b,c.])) . x1) - (h . x0)).| by A3, FUNCT_1:49, P5
.= |.(((g | [.b,c.]) . x1) - (h . x0)).| by G1i, FUNCT_4:13
.= |.((g . x1) - (h . x0)).| by FUNCT_1:49, R2
.= |.((g . x1) - (((f | [.a,b.]) +* (g | [.b,c.])) . x0)).| by A3, FUNCT_1:49, P1a
.= |.((g . x1) - ((f | [.a,b.]) . x0)).| by G0n, FUNCT_4:11
.= |.((((g . x1) - (g . b)) + (f . b)) - (f . x0)).| by A4, FUNCT_1:49, B1a ;
hence |.((h . x1) - (h . x0)).| < r by R99, R8, XXREAL_0:2; :: thesis: verum

end;

suppose S1: x1 < b ; :: thesis: |.((h . x1) - (h . x0)).| < r

then P7: not x1 in dom (g | [.b,c.]) by DGG, XXREAL_1:1;
P7a: not x0 in dom (g | [.b,c.]) by DGG, B1, XXREAL_1:1;
P8: x1 in [.a,b.] by P5a, S1;
P9a: (r / 2) + 0 < (r / 2) + (r / 2) by P2, XREAL_1:8;
|.(x1 - x0).| < sf by P6, RMin, XXREAL_0:2;
then |.((f . x1) - (f . x0)).| < r / 2 by P8, P4;
then P9: |.((f . x1) - (f . x0)).| < r by XXREAL_0:2, P9a;
|.((h . x1) - (h . x0)).| = |.(((h | [.a,c.]) . x1) - (h . x0)).| by FUNCT_1:49, P5
.= |.(((f | [.a,b.]) . x1) - (h . x0)).| by P7, FUNCT_4:11, A3
.= |.((f . x1) - (h . x0)).| by FUNCT_1:49, P8
.= |.((f . x1) - (((f | [.a,b.]) +* (g | [.b,c.])) . x0)).| by A3, FUNCT_1:49, P1a
.= |.((f . x1) - ((f | [.a,b.]) . x0)).| by P7a, FUNCT_4:11 ;
hence |.((h . x1) - (h . x0)).| < r by P9, FUNCT_1:49, B1a; :: thesis: verum

end;

end;

end;

hence ( 0 < min (sf,sg) & ( for x1 being Real st x1 in [.a,c.] & |.(x1 - x0).| < min (sf,sg) holds
|.((h . x1) - (h . x0)).| < r ) ) by P3, Q1, XXREAL_0:21; :: thesis: verum

end;

suppose B2: b <= x0 ; :: thesis: ex s being Real st
( 0 < s & ( for x1 being Real st x1 in [.a,c.] & |.(x1 - x0).| < s holds
|.((h . x1) - (h . x0)).| < r ) )

then x0 in [.b,c.] by P1;
then consider sg being Real such that
S1a: 0 < sg and
S1: for x1 being Real st x1 in [.b,c.] & |.(x1 - x0).| < sg holds
|.((g . x1) - (g . x0)).| < r / 2 by FCONT_1:14, A2a, A6, P2;
consider sf being Real such that
S2a: 0 < sf and
S2: for x1 being Real st x1 in [.a,b.] & |.(x1 - b).| < sf holds
|.((f . x1) - (f . b)).| < r / 2 by P2, FCONT_1:14, A2a, A6, Bin;
RMin: ( min (sf,sg) <= sf & min (sf,sg) <= sg ) by XXREAL_0:17;
take min (sf,sg) ; :: thesis: ( 0 < min (sf,sg) & ( for x1 being Real st x1 in [.a,c.] & |.(x1 - x0).| < min (sf,sg) holds
|.((h . x1) - (h . x0)).| < r ) )
for x1 being Real st x1 in [.a,c.] & |.(x1 - x0).| < min (sf,sg) holds
|.((h . x1) - (h . x0)).| < r

proof

let x1 be Real; :: thesis: ( x1 in [.a,c.] & |.(x1 - x0).| < min (sf,sg) implies |.((h . x1) - (h . x0)).| < r )
assume that
S3: x1 in [.a,c.] and
S4: |.(x1 - x0).| < min (sf,sg) ; :: thesis: |.((h . x1) - (h . x0)).| < r
S3a: ( a <= x1 & x1 <= c ) by S3, XXREAL_1:1;

per cases ( x1 < b or b <= x1 ) ;

suppose Q1: x1 < b ; :: thesis: |.((h . x1) - (h . x0)).| < r

then X11: not x1 in dom (g | [.b,c.]) by DGG, XXREAL_1:1;
X12: x1 in [.a,b.] by S3a, Q1;
X03: x0 in dom (g | [.b,c.]) by B2, P1, DGG;
BB0: x0 - b >= b - b by XREAL_1:13, B2;
then x0 - x1 > 0 by Q1, XREAL_1:15;
then Xabs: ( x0 - b = |.(x0 - b).| & |.(x0 - x1).| = x0 - x1 ) by BB0, COMPLEX1:43;
then |.(x0 - b).| < |.(x0 - x1).| by Q1, XREAL_1:15;
then |.(x0 - b).| < |.(- (x0 - x1)).| by COMPLEX1:52;
then |.(- (x0 - b)).| < |.(x1 - x0).| by COMPLEX1:52;
then |.(b - x0).| < min (sf,sg) by S4, XXREAL_0:2;
then |.(b - x0).| < sg by RMin, XXREAL_0:2;
then S1a: |.((g . b) - (g . x0)).| < r / 2 by S1, Bin;
b - x1 > x1 - x1 by Q1, XREAL_1:14;
then R7b: b - x1 = |.(b - x1).| by COMPLEX1:43;
|.(b - x1).| <= |.(x0 - x1).| by B2, XREAL_1:9, R7b, Xabs;
then |.(b - x1).| <= |.(- (x0 - x1)).| by COMPLEX1:52;
then |.(b - x1).| < min (sf,sg) by S4, XXREAL_0:2;
then |.(b - x1).| < sf by RMin, XXREAL_0:2;
then |.(- (b - x1)).| < sf by COMPLEX1:52;
then |.(x1 - b).| < sf ;
then S2a: |.((f . x1) - (f . b)).| < r / 2 by S2, X12;
HH: |.((h . x1) - (h . x0)).| = |.((((f | [.a,b.]) +* (g | [.b,c.])) . x1) - (h . x0)).| by A3, FUNCT_1:49, S3
.= |.(((f | [.a,b.]) . x1) - (h . x0)).| by X11, FUNCT_4:11
.= |.((f . x1) - (h . x0)).| by FUNCT_1:49, S3a, Q1, XXREAL_1:1
.= |.((f . x1) - (((f | [.a,b.]) +* (g | [.b,c.])) . x0)).| by A3, FUNCT_1:49, P1a
.= |.((f . x1) - ((g | [.b,c.]) . x0)).| by X03, FUNCT_4:13
.= |.((((f . x1) - (f . b)) + (g . b)) - (g . x0)).| by A4, FUNCT_1:49, B2, P1, XXREAL_1:1 ;
C156: |.(((f . x1) - (f . b)) + ((g . b) - (g . x0))).| <= |.((f . x1) - (f . b)).| + |.((g . b) - (g . x0)).| by COMPLEX1:56;
|.((f . x1) - (f . b)).| + |.((g . b) - (g . x0)).| < (r / 2) + (r / 2) by S1a, S2a, XREAL_1:8;
hence |.((h . x1) - (h . x0)).| < r by HH, C156, XXREAL_0:2; :: thesis: verum

end;

suppose b <= x1 ; :: thesis: |.((h . x1) - (h . x0)).| < r

then QX1: x1 in [.b,c.] by S3a;
QX0: x0 in [.b,c.] by B2, P1;
P9a: (r / 2) + 0 < (r / 2) + (r / 2) by P2, XREAL_1:8;
|.(x1 - x0).| < sg by S4, RMin, XXREAL_0:2;
then P9j: |.((g . x1) - (g . x0)).| < r / 2 by S1, QX1;
|.((h . x1) - (h . x0)).| = |.(((h | [.a,c.]) . x1) - (h . x0)).| by FUNCT_1:49, S3
.= |.(((g | [.b,c.]) . x1) - (h . x0)).| by FUNCT_4:13, DGG, QX1, A3
.= |.((g . x1) - (h . x0)).| by FUNCT_1:49, QX1
.= |.((g . x1) - ((h | [.a,c.]) . x0)).| by FUNCT_1:49, P1a
.= |.((g . x1) - ((g | [.b,c.]) . x0)).| by DGG, QX0, FUNCT_4:13, A3
.= |.((g . x1) - (g . x0)).| by FUNCT_1:49, QX0 ;
hence |.((h . x1) - (h . x0)).| < r by P9j, P9a, XXREAL_0:2; :: thesis: verum

end;

end;

end;

hence ( 0 < min (sf,sg) & ( for x1 being Real st x1 in [.a,c.] & |.(x1 - x0).| < min (sf,sg) holds
|.((h . x1) - (h . x0)).| < r ) ) by S1a, S2a, XXREAL_0:21; :: thesis: verum

end;

end;

end;

hence ex s being Real st
( 0 < s & ( for x1 being Real st x1 in [.a,c.] & |.(x1 - x0).| < s holds
|.((h . x1) - (h . x0)).| < r ) ) ; :: thesis: verum

end;

hence F is continuous by A99, FCONT_1:14, A5a; :: thesis: verum