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 H_{1}( 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 = H_{1}(x)
from FUNCT_2:sch 4();

for x0 being Real st x0 in dom f holds

f is_continuous_in x0

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 H

consider h being Function of REAL,REAL such that

A3: for x being Element of REAL holds h . x = H

for x0 being Real st x0 in dom f holds

f is_continuous_in x0

proof

hence
f is continuous
; :: thesis: verum
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 ) )

end;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

hence
f is_continuous_in x0
by FCONT_1:3; :: thesis: verum
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 ) )

( 0 < d & ( for x1 being Real st x1 in dom f & |.(x1 - x0).| < d holds

|.((f . x1) - (f . x0)).| < e ) ) ; :: thesis: verum

end;( 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

hence
ex d being Real st
for x being Real holds h . x = exp_R (- (((x - a) ^2) / (2 * (b ^2))))

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

|.((f . x1) - (f . x0)).| < e ) ) by A4; :: thesis: verum

end;proof

then
h is continuous
by GauF05, B0;
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 = H_{1}(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;reconsider x = x as Element of REAL by XREAL_0:def 1;

h . x = H

.= exp_R (- (((x - a) ^2) / (2 * (b ^2)))) ;

hence h . x = exp_R (- (((x - a) ^2) / (2 * (b ^2)))) ; :: thesis: verum

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

hence
( 0 < d1 & ( for x1 being Real st x1 in dom f & |.(x1 - x0).| < d1 holds
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)).| = |.(H_{1}(x1) - (h . x0)).|
by A3

.= |.((exp_R (- (((x1 - a) ^2) / (2 * (b ^2))))) - H_{1}(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;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)).| = |.(H

.= |.((exp_R (- (((x1 - a) ^2) / (2 * (b ^2))))) - H

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

|.((f . x1) - (f . x0)).| < e ) ) by A4; :: thesis: verum

( 0 < d & ( for x1 being Real st x1 in dom f & |.(x1 - x0).| < d holds

|.((f . x1) - (f . x0)).| < e ) ) ; :: thesis: verum