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 ) )
proof
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
proof
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;
hence ( a is set & a is Element of REAL & f . a = 1 & ( for y being Element of REAL st f . y = 1 holds
y = a ) ) by A4, A3; :: thesis: verum
end;
hence f is strictly-normalized ; :: thesis: verum