let F, f, g be Function of REAL,REAL; :: thesis: ( f is continuous & g is continuous & ( for x being Real holds F . x = max ((f . x),(g . x)) ) implies F is continuous )
assume B1a: f is continuous ; :: thesis: ( not g is continuous or ex x being Real st not F . x = max ((f . x),(g . x)) or F is continuous )
assume A1a: g is continuous ; :: thesis: ( ex x being Real st not F . x = max ((f . x),(g . x)) or F is continuous )
assume A0: for x being Real holds F . x = max ((f . x),(g . x)) ; :: thesis: F is continuous
reconsider F = F as PartFunc of REAL,REAL ;
for x0 being Real st x0 in dom F holds
F is_continuous_in x0

proof

let x0 be Real; :: thesis: ( x0 in dom F implies F is_continuous_in x0 )
assume A2: x0 in dom F ; :: thesis: F is_continuous_in x0
B0a: ( dom F = REAL & dom g = REAL & dom f = REAL ) by FUNCT_2:def 1;
for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Real st x1 in dom F & |.(x1 - x0).| < s holds
|.((F . x1) - (F . x0)).| < r ) )

proof

let r be Real; :: thesis: ( 0 < r implies ex s being Real st
( 0 < s & ( for x1 being Real st x1 in dom F & |.(x1 - x0).| < s holds
|.((F . x1) - (F . x0)).| < r ) ) )
assume A4a: 0 < r ; :: thesis: ex s being Real st
( 0 < s & ( for x1 being Real st x1 in dom F & |.(x1 - x0).| < s holds
|.((F . x1) - (F . x0)).| < r ) )
consider sg being Real such that
S1: 0 < sg and
S2: for x1 being Real st x1 in dom g & |.(x1 - x0).| < sg holds
|.((g . x1) - (g . x0)).| < r / 2 by FCONT_1:3, A1a, A2, B0a, A4a;
consider sf being Real such that
P1: 0 < sf and
P2: for x1 being Real st x1 in dom f & |.(x1 - x0).| < sf holds
|.((f . x1) - (f . x0)).| < r / 2 by FCONT_1:3, B0a, B1a, A2, A4a;
reconsider s = min (sf,sg) as Real ;
P8: ( s <= sg & s <= sf ) by XXREAL_0:17;
take s ; :: thesis: ( 0 < s & ( for x1 being Real st x1 in dom F & |.(x1 - x0).| < s holds
|.((F . x1) - (F . x0)).| < r ) )
for x1 being Real st x1 in dom F & |.(x1 - x0).| < s holds
|.((F . x1) - (F . x0)).| < r

proof

let x1 be Real; :: thesis: ( x1 in dom F & |.(x1 - x0).| < s implies |.((F . x1) - (F . x0)).| < r )
assume S6: x1 in dom F ; :: thesis: ( not |.(x1 - x0).| < s or |.((F . x1) - (F . x0)).| < r )
S8a: ( dom F = REAL & dom g = REAL & dom f = REAL ) by FUNCT_2:def 1;
assume |.(x1 - x0).| < s ; :: thesis: |.((F . x1) - (F . x0)).| < r
then ( |.(x1 - x0).| < sg & |.(x1 - x0).| < sf ) by P8, XXREAL_0:2;
then ( |.((g . x1) - (g . x0)).| < r / 2 & |.((f . x1) - (f . x0)).| < r / 2 ) by S2, P2, S8a, S6;
then |.((g . x1) - (g . x0)).| + |.((f . x1) - (f . x0)).| < (r / 2) + (r / 2) by XREAL_1:8;
then SS: (|.((g . x1) - (g . x0)).| + |.((f . x1) - (f . x0)).|) + (|.((g . x1) - (g . x0)).| + |.((f . x1) - (f . x0)).|) < ((r / 2) + (r / 2)) + ((r / 2) + (r / 2)) by XREAL_1:8;
T3: |.((F . x1) - (F . x0)).| = |.((max ((f . x1),(g . x1))) - (F . x0)).| by A0
.= |.((max ((f . x1),(g . x1))) - (max ((f . x0),(g . x0)))).| by A0
.= |.((max ((f . x1),(g . x1))) - ((((f . x0) + (g . x0)) + |.((f . x0) - (g . x0)).|) / 2)).| by COMPLEX1:74
.= |.(((((f . x1) + (g . x1)) + |.((f . x1) - (g . x1)).|) / 2) - ((((f . x0) + (g . x0)) + |.((f . x0) - (g . x0)).|) / 2)).| by COMPLEX1:74
.= |.((((((f . x1) - (f . x0)) + ((g . x1) - (g . x0))) - |.((f . x0) - (g . x0)).|) + |.((f . x1) - (g . x1)).|) / 2).|
.= |.(((((f . x1) - (f . x0)) + ((g . x1) - (g . x0))) - |.((f . x0) - (g . x0)).|) + |.((f . x1) - (g . x1)).|).| / |.2.| by COMPLEX1:67
.= |.(((((f . x1) - (f . x0)) + ((g . x1) - (g . x0))) - |.((f . x0) - (g . x0)).|) + |.((f . x1) - (g . x1)).|).| / 2 by COMPLEX1:43 ;
T1: |.((((f . x1) - (f . x0)) + ((g . x1) - (g . x0))) + ((- |.((f . x0) - (g . x0)).|) + |.((f . x1) - (g . x1)).|)).| <= |.(((f . x1) - (f . x0)) + ((g . x1) - (g . x0))).| + |.((- |.((f . x0) - (g . x0)).|) + |.((f . x1) - (g . x1)).|).| by COMPLEX1:56;
|.(((f . x1) - (f . x0)) + ((g . x1) - (g . x0))).| + |.((- |.((f . x0) - (g . x0)).|) + |.((f . x1) - (g . x1)).|).| <= (|.((f . x1) - (f . x0)).| + |.((g . x1) - (g . x0)).|) + |.((- |.((f . x0) - (g . x0)).|) + |.((f . x1) - (g . x1)).|).| by XREAL_1:6, COMPLEX1:56;
then T2: |.((((f . x1) - (f . x0)) + ((g . x1) - (g . x0))) + ((- |.((f . x0) - (g . x0)).|) + |.((f . x1) - (g . x1)).|)).| <= (|.((f . x1) - (f . x0)).| + |.((g . x1) - (g . x0)).|) + |.((- |.((f . x0) - (g . x0)).|) + |.((f . x1) - (g . x1)).|).| by XXREAL_0:2, T1;
( |.(|.((f . x0) - (g . x0)).| - |.((f . x1) - (g . x1)).|).| = |.(|.((f . x1) - (g . x1)).| - |.((f . x0) - (g . x0)).|).| & |.(|.((f . x0) - (g . x0)).| - |.((f . x1) - (g . x1)).|).| <= |.(((f . x0) - (g . x0)) - ((f . x1) - (g . x1))).| & |.(((f . x0) - (g . x0)) - ((f . x1) - (g . x1))).| = |.(((g . x1) - (g . x0)) - ((f . x1) - (f . x0))).| & |.(((g . x1) - (g . x0)) - ((f . x1) - (f . x0))).| <= |.((g . x1) - (g . x0)).| + |.((f . x1) - (f . x0)).| ) by COMPLEX1:57, COMPLEX1:64, COMPLEX1:60;
then |.(|.((f . x1) - (g . x1)).| - |.((f . x0) - (g . x0)).|).| <= |.((f . x1) - (f . x0)).| + |.((g . x1) - (g . x0)).| by XXREAL_0:2;
then |.(|.((f . x1) - (g . x1)).| - |.((f . x0) - (g . x0)).|).| + (|.((f . x1) - (f . x0)).| + |.((g . x1) - (g . x0)).|) <= (|.((f . x1) - (f . x0)).| + |.((g . x1) - (g . x0)).|) + (|.((f . x1) - (f . x0)).| + |.((g . x1) - (g . x0)).|) by XREAL_1:6;
then |.((((f . x1) - (f . x0)) + ((g . x1) - (g . x0))) + ((- |.((f . x0) - (g . x0)).|) + |.((f . x1) - (g . x1)).|)).| <= ((|.((f . x1) - (f . x0)).| + |.((g . x1) - (g . x0)).|) + |.((f . x1) - (f . x0)).|) + |.((g . x1) - (g . x0)).| by XXREAL_0:2, T2;
then |.((((f . x1) - (f . x0)) + ((g . x1) - (g . x0))) + ((- |.((f . x0) - (g . x0)).|) + |.((f . x1) - (g . x1)).|)).| < ((r / 2) + (r / 2)) + ((r / 2) + (r / 2)) by XXREAL_0:2, SS;
then |.((((f . x1) - (f . x0)) + ((g . x1) - (g . x0))) + ((- |.((f . x0) - (g . x0)).|) + |.((f . x1) - (g . x1)).|)).| / 2 < ((((r / 2) + (r / 2)) + (r / 2)) + (r / 2)) / 2 by XREAL_1:74;
hence |.((F . x1) - (F . x0)).| < r by T3; :: thesis: verum

end;

hence ( 0 < s & ( for x1 being Real st x1 in dom F & |.(x1 - x0).| < s holds
|.((F . x1) - (F . x0)).| < r ) ) by XXREAL_0:21, S1, P1; :: thesis: verum

end;

hence F is_continuous_in x0 by FCONT_1:3; :: thesis: verum

end;

hence F is continuous ; :: thesis: verum