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

f is strictly-normalized

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

assume A1: b <> 0 ; :: thesis: ( ex x being Real st not f . x = exp (- (((x - a) ^2) / (2 * (b ^2)))) or f is strictly-normalized )

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

ex x being Element of REAL st

( f . x = 1 & ( for y being Element of REAL st f . y = 1 holds

y = x ) )

f is strictly-normalized

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

assume A1: b <> 0 ; :: thesis: ( ex x being Real st not f . x = exp (- (((x - a) ^2) / (2 * (b ^2)))) or f is strictly-normalized )

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

ex x being Element of REAL st

( f . x = 1 & ( for y being Element of REAL st f . y = 1 holds

y = x ) )

proof

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

take a ; :: thesis: ( a is set & a is Element of REAL & f . a = 1 & ( for y being Element of REAL st f . y = 1 holds

y = a ) )

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

.= 1 by SIN_COS3:20 ;

for y being Element of REAL st f . y = 1 holds

y = a

y = a ) ) by A4, A3; :: thesis: verum

end;take a ; :: thesis: ( a is set & a is Element of REAL & f . a = 1 & ( for y being Element of REAL st f . y = 1 holds

y = a ) )

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

.= 1 by SIN_COS3:20 ;

for y being Element of REAL st f . y = 1 holds

y = a

proof

hence
( a is set & a is Element of REAL & f . a = 1 & ( for y being Element of REAL st f . y = 1 holds
let y be Element of REAL ; :: thesis: ( f . y = 1 implies y = a )

assume f . y = 1 ; :: thesis: y = a

then exp (- (((y - a) ^2) / (2 * (b ^2)))) = 1 by A2;

then y - a = 0 by A1, EXpReq12;

hence y = a ; :: thesis: verum

end;assume f . y = 1 ; :: thesis: y = a

then exp (- (((y - a) ^2) / (2 * (b ^2)))) = 1 by A2;

then y - a = 0 by A1, EXpReq12;

hence y = a ; :: thesis: verum

y = a ) ) by A4, A3; :: thesis: verum