let a, b be Real; :: thesis: for f being Function of REAL,REAL st b <> 0 & ( for x being Real holds f . x = exp (- (((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 (- (((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 (- (((x - a) ^2) / (2 * (b ^2)))) or f is FuzzySet of REAL )
assume A2: for x being Real holds f . x = exp (- (((x - a) ^2) / (2 * (b ^2)))) ; :: thesis: f is FuzzySet of REAL
for x being Real holds f . x = exp_R (- (((x - a) ^2) / (2 * (b ^2))))
proof
let x be Real; :: thesis: f . x = exp_R (- (((x - a) ^2) / (2 * (b ^2))))
f . x = exp (- (((x - a) ^2) / (2 * (b ^2)))) by A2
.= exp_R (- (((x - a) ^2) / (2 * (b ^2)))) by SIN_COS:49 ;
hence f . x = exp_R (- (((x - a) ^2) / (2 * (b ^2)))) ; :: thesis: verum
end;
hence f is FuzzySet of REAL by GauF04, A1; :: thesis: verum