let a, b be Real; :: thesis: for f being FuzzySet of REAL st b > 0 & ( for x being Real holds f . x = max (0,(1 - |.((x - a) / b).|)) ) holds
f is strictly-normalized
let f be FuzzySet of REAL; :: thesis: ( b > 0 & ( for x being Real holds f . x = max (0,(1 - |.((x - a) / b).|)) ) implies f is strictly-normalized )
assume A1: b > 0 ; :: thesis: ( ex x being Real st not f . x = max (0,(1 - |.((x - a) / b).|)) or f is strictly-normalized )
assume A2: for x being Real holds f . x = max (0,(1 - |.((x - a) / b).|)) ; :: 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 = max (0,(1 - |.((a - a) / b).|)) by A2
.= max (0,(1 - 0)) by ABSVALUE:def 1
.= 1 by XXREAL_0:def 10 ;
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 max (0,(1 - |.((y - a) / b).|)) = 1 by A2;
then 1 - |.((y - a) / b).| = 1 by XXREAL_0:16;
then y - a = 0 by A1, ABSVALUE:2;
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