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

proof

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;

hence f is normalized ; :: thesis: verum