let f, g be Function of REAL,REAL; :: thesis: for a being Real st g is continuous & ( for x being Real holds f . x = min (a,(g . x)) ) holds
f is continuous
let a be Real; :: thesis: ( g is continuous & ( for x being Real holds f . x = min (a,(g . x)) ) implies f is continuous )
assume A1a: g is continuous ; :: thesis: ( ex x being Real st not f . x = min (a,(g . x)) or f is continuous )
assume A0: for x being Real holds f . x = min (a,(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
A3a: ( dom f = REAL & dom g = 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 A4: 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 s being Real such that
S1: 0 < s and
S2: for x1 being Real st x1 in dom g & |.(x1 - x0).| < s holds
|.((g . x1) - (g . x0)).| < r by A3a, FCONT_1:3, A1a, A2, A4;
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 ) by FUNCT_2:def 1;
assume S7: |.(x1 - x0).| < s ; :: thesis: |.((f . x1) - (f . x0)).| < r
S5: 2 * |.((f . x1) - (f . x0)).| = 2 * |.((f . x1) - (min (a,(g . x0)))).| by A0
.= 2 * |.((min (a,(g . x1))) - (min (a,(g . x0)))).| by A0
.= 2 * |.((min (a,(g . x1))) - (((a + (g . x0)) - |.(a - (g . x0)).|) / 2)).| by COMPLEX1:73
.= 2 * |.((((a + (g . x1)) - |.(a - (g . x1)).|) / 2) - (((a + (g . x0)) - |.(a - (g . x0)).|) / 2)).| by COMPLEX1:73
.= 2 * |.((((a + (g . x1)) - |.(a - (g . x1)).|) - ((a + (g . x0)) - |.(a - (g . x0)).|)) / 2).|
.= 2 * (|.(((a + (g . x1)) - |.(a - (g . x1)).|) - ((a + (g . x0)) - |.(a - (g . x0)).|)).| / |.2.|) by COMPLEX1:67
.= 2 * (|.(((a + (g . x1)) - |.(a - (g . x1)).|) - ((a + (g . x0)) - |.(a - (g . x0)).|)).| / 2) by COMPLEX1:43
.= |.(((g . x1) - (g . x0)) + (|.(a - (g . x0)).| - |.(a - (g . x1)).|)).| ;
|.((g . x1) - (g . x0)).| < r by S2, S7, S8a, S6;
then S4: |.((g . x1) - (g . x0)).| + |.((g . x1) - (g . x0)).| < r + r by XREAL_1:8;
S3: |.(((g . x1) - (g . x0)) + (|.(a - (g . x0)).| - |.(a - (g . x1)).|)).| <= |.((g . x1) - (g . x0)).| + |.(|.(a - (g . x0)).| - |.(a - (g . x1)).|).| by COMPLEX1:56;
|.(|.(a - (g . x0)).| - |.(a - (g . x1)).|).| <= |.((a - (g . x0)) - (a - (g . x1))).| by COMPLEX1:64;
then |.((g . x1) - (g . x0)).| + |.(|.(a - (g . x0)).| - |.(a - (g . x1)).|).| <= |.((g . x1) - (g . x0)).| + |.((- (g . x0)) + (g . x1)).| by XREAL_1:7;
then |.((g . x1) - (g . x0)).| + |.(|.(a - (g . x0)).| - |.(a - (g . x1)).|).| < 2 * r by S4, XXREAL_0:2;
then 2 * |.((f . x1) - (f . x0)).| < 2 * r by S5, S3, XXREAL_0:2;
then (2 * |.((f . x1) - (f . x0)).|) / 2 < (2 * r) / 2 by XREAL_1:74;
hence |.((f . x1) - (f . x0)).| < r ; :: 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 S1; :: thesis: verum

end;

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

end;

hence f is continuous ; :: thesis: verum