let a, b be Real; :: thesis: for f being Function of REAL,REAL st ( for x being Real holds f . x = max (0,(1 - |.((x - a) / b).|)) ) holds

f is FuzzySet of REAL

let f be Function of REAL,REAL; :: thesis: ( ( for x being Real holds f . x = max (0,(1 - |.((x - a) / b).|)) ) implies f is FuzzySet of REAL )

assume B2: for x being Real holds f . x = max (0,(1 - |.((x - a) / b).|)) ; :: thesis: f is FuzzySet of REAL

rng f c= [.0,1.]

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

f is FuzzySet of REAL

let f be Function of REAL,REAL; :: thesis: ( ( for x being Real holds f . x = max (0,(1 - |.((x - a) / b).|)) ) implies f is FuzzySet of REAL )

assume B2: for x being Real holds f . x = max (0,(1 - |.((x - a) / b).|)) ; :: thesis: f is FuzzySet of REAL

rng f c= [.0,1.]

proof

then
f is [.0,1.] -valued
;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in [.0,1.] )

assume y in rng f ; :: thesis: y in [.0,1.]

then consider x being object such that

B1: x in REAL and

B3: y = f . x by FUNCT_2:11;

reconsider x = x as Real by B1;

( 0 <= max (0,(1 - |.((x - a) / b).|)) & max (0,(1 - |.((x - a) / b).|)) <= 1 )

hence y in [.0,1.] by B3; :: thesis: verum

end;assume y in rng f ; :: thesis: y in [.0,1.]

then consider x being object such that

B1: x in REAL and

B3: y = f . x by FUNCT_2:11;

reconsider x = x as Real by B1;

( 0 <= max (0,(1 - |.((x - a) / b).|)) & max (0,(1 - |.((x - a) / b).|)) <= 1 )

proof

then
( 0 <= f . x & f . x <= 1 )
by B2;
0 <= |.((x - a) / b).|
by COMPLEX1:46;

then 1 + 0 <= 1 + |.((x - a) / b).| by XREAL_1:7;

then 1 - |.((x - a) / b).| <= (1 + |.((x - a) / b).|) - |.((x - a) / b).| by XREAL_1:9;

hence ( 0 <= max (0,(1 - |.((x - a) / b).|)) & max (0,(1 - |.((x - a) / b).|)) <= 1 ) by XXREAL_0:28, XXREAL_0:25; :: thesis: verum

end;then 1 + 0 <= 1 + |.((x - a) / b).| by XREAL_1:7;

then 1 - |.((x - a) / b).| <= (1 + |.((x - a) / b).|) - |.((x - a) / b).| by XREAL_1:9;

hence ( 0 <= max (0,(1 - |.((x - a) / b).|)) & max (0,(1 - |.((x - a) / b).|)) <= 1 ) by XXREAL_0:28, XXREAL_0:25; :: thesis: verum

hence y in [.0,1.] by B3; :: thesis: verum

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