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.]

proof

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 )

proof

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 ( 0 <= f . x & f . x <= 1 ) by B2;
hence y in [.0,1.] by B3; :: thesis: verum

end;

then f is [.0,1.] -valued ;
hence f is FuzzySet of REAL ; :: thesis: verum