let a, b be Real; :: thesis: for f being Function of REAL,REAL st ( for x being Real holds f . x = max (0,(cos ((a * x) + b))) ) holds

f is FuzzySet of REAL

let f be Function of REAL,REAL; :: thesis: ( ( for x being Real holds f . x = max (0,(cos ((a * x) + b))) ) implies f is FuzzySet of REAL )

assume for th being Real holds f . th = max (0,(cos ((a * th) + b))) ; :: thesis: f is FuzzySet of REAL

then f in { f where f is Function of REAL,REAL : ex a, b being Real st

for th being Real holds f . th = max (0,(cos ((a * th) + b))) } ;

hence f is FuzzySet of REAL by Def1, MM2; :: thesis: verum

f is FuzzySet of REAL

let f be Function of REAL,REAL; :: thesis: ( ( for x being Real holds f . x = max (0,(cos ((a * x) + b))) ) implies f is FuzzySet of REAL )

assume for th being Real holds f . th = max (0,(cos ((a * th) + b))) ; :: thesis: f is FuzzySet of REAL

then f in { f where f is Function of REAL,REAL : ex a, b being Real st

for th being Real holds f . th = max (0,(cos ((a * th) + b))) } ;

hence f is FuzzySet of REAL by Def1, MM2; :: thesis: verum