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.]

hence f is FuzzySet of REAL ; :: thesis: verum

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

then
f is [.0,1.] -valued
;
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

hence z in [.0,1.] by B4; :: thesis: verum

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

hence f is FuzzySet of REAL ; :: thesis: verum