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))))

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

hence
f is FuzzySet of REAL
by GauF04, A1; :: thesis: verum
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;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