let a, b be Real; :: thesis: for f being FuzzySet of REAL st ( for x being Real holds f . x = exp (- (((x - a) ^2) / (2 * (b ^2)))) ) holds

f is normalized

let f be FuzzySet of REAL; :: thesis: ( ( for x being Real holds f . x = exp (- (((x - a) ^2) / (2 * (b ^2)))) ) implies f is normalized )

assume A2: for x being Real holds f . x = exp (- (((x - a) ^2) / (2 * (b ^2)))) ; :: thesis: f is normalized

ex x being Element of REAL st f . x = 1

f is normalized

let f be FuzzySet of REAL; :: thesis: ( ( for x being Real holds f . x = exp (- (((x - a) ^2) / (2 * (b ^2)))) ) implies f is normalized )

assume A2: for x being Real holds f . x = exp (- (((x - a) ^2) / (2 * (b ^2)))) ; :: thesis: f is normalized

ex x being Element of REAL st f . x = 1

proof

hence
f is normalized
; :: thesis: verum
A6:
a is Element of REAL
by XREAL_0:def 1;

take a ; :: thesis: ( a is set & a is Element of REAL & f . a = 1 )

f . a = exp (- (((a - a) ^2) / (2 * (b ^2)))) by A2

.= 1 by SIN_COS3:20 ;

hence ( a is set & a is Element of REAL & f . a = 1 ) by A6; :: thesis: verum

end;take a ; :: thesis: ( a is set & a is Element of REAL & f . a = 1 )

f . a = exp (- (((a - a) ^2) / (2 * (b ^2)))) by A2

.= 1 by SIN_COS3:20 ;

hence ( a is set & a is Element of REAL & f . a = 1 ) by A6; :: thesis: verum