let a, b, c be Real; :: thesis: for f being Function of REAL,REAL st b <> 0 & ( for x being Real holds f . x = max (0,(min (1,((exp_R (- (((x - a) ^2) / (2 * (b ^2))))) + c)))) ) holds
f is FuzzySet of REAL
let f be Function of REAL,REAL; :: thesis: ( b <> 0 & ( for x being Real holds f . x = max (0,(min (1,((exp_R (- (((x - a) ^2) / (2 * (b ^2))))) + c)))) ) implies f is FuzzySet of REAL )
assume b <> 0 ; :: thesis: ( ex x being Real st not f . x = max (0,(min (1,((exp_R (- (((x - a) ^2) / (2 * (b ^2))))) + c)))) or f is FuzzySet of REAL )
assume A2: for x being Real holds f . x = max (0,(min (1,((exp_R (- (((x - a) ^2) / (2 * (b ^2))))) + c)))) ; :: thesis: f is FuzzySet of REAL
ex g being Function of REAL,REAL st
for x being Real holds g . x = (exp_R (- (((x - a) ^2) / (2 * (b ^2))))) + c

proof

deffunc H₁( Element of REAL ) -> Element of REAL = In (((exp_R (- ((($1 - a) ^2) / (2 * (b ^2))))) + c),REAL);
consider f being Function of REAL,REAL such that
A1: for x being Element of REAL holds f . x = H₁(x) from FUNCT_2:sch 4();
take f ; :: thesis: for x being Real holds f . x = (exp_R (- (((x - a) ^2) / (2 * (b ^2))))) + c
for x being Real holds f . x = (exp_R (- (((x - a) ^2) / (2 * (b ^2))))) + c

proof

let x be Real; :: thesis: f . x = (exp_R (- (((x - a) ^2) / (2 * (b ^2))))) + c
reconsider x = x as Element of REAL by XREAL_0:def 1;
f . x = H₁(x) by A1;
hence f . x = (exp_R (- (((x - a) ^2) / (2 * (b ^2))))) + c ; :: thesis: verum

end;

hence for x being Real holds f . x = (exp_R (- (((x - a) ^2) / (2 * (b ^2))))) + c ; :: thesis: verum

end;

then consider g being Function of REAL,REAL such that
A4: for x being Real holds g . x = (exp_R (- (((x - a) ^2) / (2 * (b ^2))))) + c ;
for x being Real holds f . x = max (0,(min (1,(g . x))))

proof

let x be Real; :: thesis: f . x = max (0,(min (1,(g . x))))
f . x = max (0,(min (1,((exp_R (- (((x - a) ^2) / (2 * (b ^2))))) + c)))) by A2
.= max (0,(min (1,(g . x)))) by A4 ;
hence f . x = max (0,(min (1,(g . x)))) ; :: thesis: verum

end;

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