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

( 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