let a, b be Real; :: thesis: for f being Function of REAL,REAL st b <> 0 & ( for x being Real holds f . x = exp_R (- (((x - a) ^2) / (2 * (b ^2)))) ) holds
f is continuous
let f be Function of REAL,REAL; :: thesis: ( b <> 0 & ( for x being Real holds f . x = exp_R (- (((x - a) ^2) / (2 * (b ^2)))) ) implies f is continuous )
assume b <> 0 ; :: thesis: ( ex x being Real st not f . x = exp_R (- (((x - a) ^2) / (2 * (b ^2)))) or f is continuous )
assume A1: for x being Real holds f . x = exp_R (- (((x - a) ^2) / (2 * (b ^2)))) ; :: thesis: f is continuous
set h = AffineMap (1,(- a));
set g = (((- 1) / (2 * (b ^2))) (#) (AffineMap (1,(- a)))) (#) (AffineMap (1,(- a)));
D1: dom ((((- 1) / (2 * (b ^2))) (#) (AffineMap (1,(- a)))) (#) (AffineMap (1,(- a)))) = REAL /\ REAL by FUNCT_2:def 1;
f = exp_R * ((((- 1) / (2 * (b ^2))) (#) (AffineMap (1,(- a)))) (#) (AffineMap (1,(- a))))
proof
dom (exp_R * ((((- 1) / (2 * (b ^2))) (#) (AffineMap (1,(- a)))) (#) (AffineMap (1,(- a))))) = REAL by FUNCT_2:def 1;
then A21: dom f = dom (exp_R * ((((- 1) / (2 * (b ^2))) (#) (AffineMap (1,(- a)))) (#) (AffineMap (1,(- a))))) by FUNCT_2:def 1;
for x being object st x in dom f holds
f . x = (exp_R * ((((- 1) / (2 * (b ^2))) (#) (AffineMap (1,(- a)))) (#) (AffineMap (1,(- a))))) . x
proof
let x be object ; :: thesis: ( x in dom f implies f . x = (exp_R * ((((- 1) / (2 * (b ^2))) (#) (AffineMap (1,(- a)))) (#) (AffineMap (1,(- a))))) . x )
assume S2a: x in dom f ; :: thesis: f . x = (exp_R * ((((- 1) / (2 * (b ^2))) (#) (AffineMap (1,(- a)))) (#) (AffineMap (1,(- a))))) . x
then x in REAL by FUNCT_2:def 1;
then reconsider x = x as Real ;
S1: x in dom ((((- 1) / (2 * (b ^2))) (#) (AffineMap (1,(- a)))) (#) (AffineMap (1,(- a)))) by D1, FUNCT_2:def 1, S2a;
(exp_R * ((((- 1) / (2 * (b ^2))) (#) (AffineMap (1,(- a)))) (#) (AffineMap (1,(- a))))) . x = exp_R . (((((- 1) / (2 * (b ^2))) (#) (AffineMap (1,(- a)))) (#) (AffineMap (1,(- a)))) . x) by FUNCT_1:13, S1
.= exp_R . (((((- 1) / (2 * (b ^2))) (#) (AffineMap (1,(- a)))) . x) * ((AffineMap (1,(- a))) . x)) by VALUED_1:5
.= exp_R . ((((- 1) / (2 * (b ^2))) * ((AffineMap (1,(- a))) . x)) * ((AffineMap (1,(- a))) . x)) by VALUED_1:6
.= exp_R . ((((- 1) / (2 * (b ^2))) * ((AffineMap (1,(- a))) . x)) * ((1 * x) + (- a))) by FCONT_1:def 4
.= exp_R . ((((- 1) / (2 * (b ^2))) * ((1 * x) + (- a))) * (x - a)) by FCONT_1:def 4
.= exp_R (((- 1) / (2 * (b ^2))) * ((x - a) * (x - a))) by SIN_COS:def 23
.= exp_R ((((x - a) * (x - a)) / (2 * (b ^2))) * (- 1)) by XCMPLX_1:75
.= exp_R (- (((x - a) ^2) / (2 * (b ^2)))) ;
hence f . x = (exp_R * ((((- 1) / (2 * (b ^2))) (#) (AffineMap (1,(- a)))) (#) (AffineMap (1,(- a))))) . x by A1; :: thesis: verum
end;
hence f = exp_R * ((((- 1) / (2 * (b ^2))) (#) (AffineMap (1,(- a)))) (#) (AffineMap (1,(- a)))) by FUNCT_1:2, A21; :: thesis: verum
end;
hence f is continuous ; :: thesis: verum