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

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

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

then consider g being Function of REAL,REAL such that
deffunc H_{1}( 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_{1}(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

end;consider f being Function of REAL,REAL such that

A1: for x being Element of REAL holds f . x = H

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

hence
for x being Real holds f . x = (exp_R (- (((x - a) ^2) / (2 * (b ^2))))) + c
; :: thesis: verum
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_{1}(x)
by A1;

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

end;reconsider x = x as Element of REAL by XREAL_0:def 1;

f . x = H

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

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

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