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 ) )

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

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 = 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

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 = 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

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 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;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

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