let a, b, c, r, s be Real; :: thesis: for f being Function of REAL,REAL st b <> 0 & ( for x being Real holds f . x = max (r,(min (s,((exp_R (- (((x - a) ^2) / (2 * (b ^2))))) + c)))) ) holds
f is continuous
let f be Function of REAL,REAL; :: thesis: ( b <> 0 & ( for x being Real holds f . x = max (r,(min (s,((exp_R (- (((x - a) ^2) / (2 * (b ^2))))) + c)))) ) implies f is continuous )
assume B0: b <> 0 ; :: thesis: ( ex x being Real st not f . x = max (r,(min (s,((exp_R (- (((x - a) ^2) / (2 * (b ^2))))) + c)))) or f is continuous )
assume A1: for x being Real holds f . x = max (r,(min (s,((exp_R (- (((x - a) ^2) / (2 * (b ^2))))) + c)))) ; :: thesis: f is continuous
deffunc H1( Element of REAL ) -> Element of REAL = In ((exp_R (- ((($1 - a) ^2) / (2 * (b ^2))))),REAL);
consider h being Function of REAL,REAL such that
A3: for x being Element of REAL holds h . x = H1(x) from FUNCT_2:sch 4();
 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 x0 in dom f ; :: thesis: f is_continuous_in x0
then x0 in REAL by FUNCT_2:def 1;
then B1: x0 in dom h by FUNCT_2:def 1;
for e being Real st 0 < e holds
ex d being Real st
( 0 < d & ( for x1 being Real st x1 in dom f & |.(x1 - x0).| < d holds
|.((f . x1) - (f . x0)).| < e ) )
proof
let e be Real; :: thesis: ( 0 < e implies ex d being Real st
( 0 < d & ( for x1 being Real st x1 in dom f & |.(x1 - x0).| < d holds
|.((f . x1) - (f . x0)).| < e ) ) )
assume A2: 0 < e ; :: thesis: ex d being Real st
( 0 < d & ( for x1 being Real st x1 in dom f & |.(x1 - x0).| < d holds
|.((f . x1) - (f . x0)).| < e ) )
ex d being Real st
( 0 < d & ( for x1 being Real st x1 in dom f & |.(x1 - x0).| < d holds
|.((f . x1) - (f . x0)).| < e ) )
proof
for x being Real holds h . x = exp_R (- (((x - a) ^2) / (2 * (b ^2))))
proof
let x be Real; :: thesis: h . x = exp_R (- (((x - a) ^2) / (2 * (b ^2))))
reconsider x = x as Element of REAL by XREAL_0:def 1;
h . x = H1(x) by A3
.= exp_R (- (((x - a) ^2) / (2 * (b ^2)))) ;
hence h . x = exp_R (- (((x - a) ^2) / (2 * (b ^2)))) ; :: thesis: verum
end;
then h is continuous by GauF05, B0;
then consider d1 being Real such that
A4: d1 > 0 and
A7: for x1 being Real st x1 in dom h & |.(x1 - x0).| < d1 holds
|.((h . x1) - (h . x0)).| < e by A2, FCONT_1:3, B1;
take d1 ; :: thesis: ( 0 < d1 & ( for x1 being Real st x1 in dom f & |.(x1 - x0).| < d1 holds
|.((f . x1) - (f . x0)).| < e ) )
for x1 being Real st x1 in dom f & |.(x1 - x0).| < d1 holds
|.((f . x1) - (f . x0)).| < e
proof
let x1 be Real; :: thesis: ( x1 in dom f & |.(x1 - x0).| < d1 implies |.((f . x1) - (f . x0)).| < e )
assume x1 in dom f ; :: thesis: ( not |.(x1 - x0).| < d1 or |.((f . x1) - (f . x0)).| < e )
then x1 in REAL by FUNCT_2:def 1;
then A8: x1 in dom h by FUNCT_2:def 1;
assume A6: |.(x1 - x0).| < d1 ; :: thesis: |.((f . x1) - (f . x0)).| < e
|.((f . x1) - (f . x0)).| = |.((max (r,(min (s,((exp_R (- (((x1 - a) ^2) / (2 * (b ^2))))) + c))))) - (f . x0)).| by A1
.= |.((max (r,(min (s,((exp_R (- (((x1 - a) ^2) / (2 * (b ^2))))) + c))))) - (max (r,(min (s,((exp_R (- (((x0 - a) ^2) / (2 * (b ^2))))) + c)))))).| by A1 ;
then A9: |.((f . x1) - (f . x0)).| <= |.(((exp_R (- (((x1 - a) ^2) / (2 * (b ^2))))) + c) - ((exp_R (- (((x0 - a) ^2) / (2 * (b ^2))))) + c)).| by LeMM01;
reconsider x1 = x1 as Element of REAL by XREAL_0:def 1;
reconsider x0 = x0 as Element of REAL by XREAL_0:def 1;
|.((h . x1) - (h . x0)).| = |.(H1(x1) - (h . x0)).| by A3
.= |.((exp_R (- (((x1 - a) ^2) / (2 * (b ^2))))) - H1(x0)).| by A3 ;
then |.((exp_R (- (((x1 - a) ^2) / (2 * (b ^2))))) - (exp_R (- (((x0 - a) ^2) / (2 * (b ^2)))))).| < e by A8, A6, A7;
hence |.((f . x1) - (f . x0)).| < e by A9, XXREAL_0:2; :: thesis: verum
end;
hence ( 0 < d1 & ( for x1 being Real st x1 in dom f & |.(x1 - x0).| < d1 holds
|.((f . x1) - (f . x0)).| < e ) ) by A4; :: thesis: verum
end;
hence ex d being Real st
( 0 < d & ( for x1 being Real st x1 in dom f & |.(x1 - x0).| < d holds
|.((f . x1) - (f . x0)).| < e ) ) ; :: thesis: verum
end;
hence f is_continuous_in x0 by FCONT_1:3; :: thesis: verum
end;
hence f is continuous ; :: thesis: verum