let f be FuzzySet of REAL; :: thesis: ( f in { f where f is Function of REAL,REAL : ex a, b being Real st
( a <> 0 & ( for th being Real holds f . th = ((1 / 2) * (cos ((a * th) + b))) + (1 / 2) ) ) } implies f is normalized )
assume f in { f where f is Function of REAL,REAL : ex a, b being Real st
( a <> 0 & ( for th being Real holds f . th = ((1 / 2) * (cos ((a * th) + b))) + (1 / 2) ) ) } ; :: thesis: f is normalized
then consider f1 being Function of REAL,REAL such that
A1: f1 = f and
A2: ex a, b being Real st
( a <> 0 & ( for th being Real holds f1 . th = ((1 / 2) * (cos ((a * th) + b))) + (1 / 2) ) ) ;
thus f is normalized by A1, TrF22, A2; :: thesis: verum