let a, b, c be Real; :: thesis: for f being Function of REAL,REAL st b > 1 & ( for x being Real holds f . x = min (1,(max (0,(b - |.((b * (x - a)) / c).|)))) ) holds
f is normalized FuzzySet of REAL
let f be Function of REAL,REAL; :: thesis: ( b > 1 & ( for x being Real holds f . x = min (1,(max (0,(b - |.((b * (x - a)) / c).|)))) ) implies f is normalized FuzzySet of REAL )
assume A2: b > 1 ; :: thesis: ( ex x being Real st not f . x = min (1,(max (0,(b - |.((b * (x - a)) / c).|)))) or f is normalized FuzzySet of REAL )
assume A1: for x being Real holds f . x = min (1,(max (0,(b - |.((b * (x - a)) / c).|)))) ; :: thesis: f is normalized FuzzySet of REAL
deffunc H₁( Element of REAL ) -> Element of REAL = In ((b - |.((b * ($1 - a)) / c).|),REAL);
consider h being Function of REAL,REAL such that
A3: for x being Element of REAL holds h . x = H₁(x) from FUNCT_2:sch 4();
for x being Real holds f . x = min (1,(max (0,(h . x))))

proof

let x be Real; :: thesis: f . x = min (1,(max (0,(h . x))))
reconsider x = x as Element of REAL by XREAL_0:def 1;
min (1,(max (0,(h . x)))) = min (1,(max (0,H₁(x)))) by A3
.= f . x by A1 ;
hence f . x = min (1,(max (0,(h . x)))) ; :: thesis: verum

end;

then reconsider f = f as FuzzySet of REAL by FUZZY_5:26;
f is normalized

proof

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 = min (1,(max (0,(b - |.((b * (a - a)) / c).|)))) by A1
.= min (1,(max (0,(b - 0)))) by ABSVALUE:def 1
.= min (1,b) by XXREAL_0:def 10, A2
.= 1 by XXREAL_0:def 9, A2 ;
hence ( a is set & a is Element of REAL & f . a = 1 ) by A6; :: thesis: verum

end;

hence f is normalized ; :: thesis: verum

end;

hence f is normalized FuzzySet of REAL ; :: thesis: verum