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 FuzzySet of REAL
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 FuzzySet of REAL )
assume A1: b <> 0 ; :: thesis: ( ex x being Real st not f . x = exp_R (- (((x - a) ^2) / (2 * (b ^2)))) or f is FuzzySet of REAL )
assume A2: for x being Real holds f . x = exp_R (- (((x - a) ^2) / (2 * (b ^2)))) ; :: thesis: f is FuzzySet of REAL
rng f c= [.0,1.]

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in rng f or z in [.0,1.] )
assume z in rng f ; :: thesis: z in [.0,1.]
then consider x being object such that
B2: x in REAL and
B3: f . x = z by FUNCT_2:11;
reconsider x = x as Real by B2;
B4: z = exp_R (- (((x - a) ^2) / (2 * (b ^2)))) by B3, A2;
B5: exp_R (- (((x - a) ^2) / (2 * (b ^2)))) <= 1

proof

per cases ( x = a or x <> a ) ;

suppose x = a ; :: thesis: exp_R (- (((x - a) ^2) / (2 * (b ^2)))) <= 1

then exp_R (- (((x - a) ^2) / (2 * (b ^2)))) = 1 by SIN_COS:51;
hence exp_R (- (((x - a) ^2) / (2 * (b ^2)))) <= 1 ; :: thesis: verum

end;

suppose x <> a ; :: thesis: exp_R (- (((x - a) ^2) / (2 * (b ^2)))) <= 1

then x - a <> 0 ;
then ( (x - a) ^2 > 0 & b ^2 > 0 ) by SQUARE_1:12, A1;
then exp_R . (- (((x - a) ^2) / (2 * (b ^2)))) <= 1 by SIN_COS:53;
hence exp_R (- (((x - a) ^2) / (2 * (b ^2)))) <= 1 by SIN_COS:def 23; :: thesis: verum

end;

end;

end;

( 0 <= exp_R (- (((x - a) ^2) / (2 * (b ^2)))) & exp_R (- (((x - a) ^2) / (2 * (b ^2)))) <= 1 ) by B5, SIN_COS:55;
hence z in [.0,1.] by B4; :: thesis: verum

end;

then f is [.0,1.] -valued ;
hence f is FuzzySet of REAL ; :: thesis: verum