let g be object ; :: according to TARSKI:def 3 :: thesis: ( not g in { f where f is Function of REAL,REAL, a, b, c, d is Real : for x being Real holds f . x = max (0,(min (1,((c * (sin ((a * x) + b))) + d)))) } or g in Membership_Funcs REAL )

assume g in { f where f is Function of REAL,REAL, a, b, c, d is Real : for x being Real holds f . x = max (0,(min (1,((c * (sin ((a * x) + b))) + d)))) } ; :: thesis: g in Membership_Funcs REAL

then consider f being Function of REAL,REAL, a, b, c, d being Real such that

A1: f = g and

A2: for x being Real holds f . x = max (0,(min (1,((c * (sin ((a * x) + b))) + d)))) ;

f is FuzzySet of REAL

assume g in { f where f is Function of REAL,REAL, a, b, c, d is Real : for x being Real holds f . x = max (0,(min (1,((c * (sin ((a * x) + b))) + d)))) } ; :: thesis: g in Membership_Funcs REAL

then consider f being Function of REAL,REAL, a, b, c, d being Real such that

A1: f = g and

A2: for x being Real holds f . x = max (0,(min (1,((c * (sin ((a * x) + b))) + d)))) ;

f is FuzzySet of REAL

proof

hence
g in Membership_Funcs REAL
by Def1, A1; :: thesis: verum
rng f c= [.0,1.]

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

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

B2: x in REAL and

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

reconsider x = x as Real by B2;

B4: y = max (0,(min (1,((c * (sin ((a * x) + b))) + d)))) by A2, B3;

min (1,((c * (sin ((a * x) + b))) + d)) <= 1 by XXREAL_0:17;

then ( 0 <= max (0,(min (1,((c * (sin ((a * x) + b))) + d)))) & max (0,(min (1,((c * (sin ((a * x) + b))) + d)))) <= 1 ) by XXREAL_0:28, XXREAL_0:25;

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

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

then consider x being object such that

B2: x in REAL and

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

reconsider x = x as Real by B2;

B4: y = max (0,(min (1,((c * (sin ((a * x) + b))) + d)))) by A2, B3;

min (1,((c * (sin ((a * x) + b))) + d)) <= 1 by XXREAL_0:17;

then ( 0 <= max (0,(min (1,((c * (sin ((a * x) + b))) + d)))) & max (0,(min (1,((c * (sin ((a * x) + b))) + d)))) <= 1 ) by XXREAL_0:28, XXREAL_0:25;

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

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