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) * (sin ((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) * (sin ((a * th) + b))) + (1 / 2) ) ) } ; :: thesis: f is normalized

then consider f2 being Function of REAL,REAL such that

A3: f = f2 and

A4: ex a, b being Real st

( a <> 0 & ( for th being Real holds f2 . th = ((1 / 2) * (sin ((a * th) + b))) + (1 / 2) ) ) ;

consider a, b being Real such that

A7: a <> 0 and

A5: for th being Real holds f2 . th = ((1 / 2) * (sin ((a * th) + b))) + (1 / 2) by A4;

reconsider a = a as Element of REAL by XREAL_0:def 1;

ex x being Element of REAL st f . x = 1

( a <> 0 & ( for th being Real holds f . th = ((1 / 2) * (sin ((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) * (sin ((a * th) + b))) + (1 / 2) ) ) } ; :: thesis: f is normalized

then consider f2 being Function of REAL,REAL such that

A3: f = f2 and

A4: ex a, b being Real st

( a <> 0 & ( for th being Real holds f2 . th = ((1 / 2) * (sin ((a * th) + b))) + (1 / 2) ) ) ;

consider a, b being Real such that

A7: a <> 0 and

A5: for th being Real holds f2 . th = ((1 / 2) * (sin ((a * th) + b))) + (1 / 2) by A4;

reconsider a = a as Element of REAL by XREAL_0:def 1;

ex x being Element of REAL st f . x = 1

proof

hence
f is normalized
; :: thesis: verum
take
((PI / 2) - b) / a
; :: thesis: ( ((PI / 2) - b) / a is Element of REAL & f . (((PI / 2) - b) / a) = 1 )

f . (((PI / 2) - b) / a) = ((1 / 2) * (sin ((a * (((PI / 2) - b) / a)) + b))) + (1 / 2) by A5, A3

.= ((1 / 2) * (sin (((a / a) * ((PI / 2) - b)) + b))) + (1 / 2) by XCMPLX_1:75

.= ((1 / 2) * (sin ((1 * ((PI / 2) - b)) + b))) + (1 / 2) by XCMPLX_1:60, A7

.= 1 by SIN_COS:77 ;

hence ( ((PI / 2) - b) / a is Element of REAL & f . (((PI / 2) - b) / a) = 1 ) by XREAL_0:def 1; :: thesis: verum

end;f . (((PI / 2) - b) / a) = ((1 / 2) * (sin ((a * (((PI / 2) - b) / a)) + b))) + (1 / 2) by A5, A3

.= ((1 / 2) * (sin (((a / a) * ((PI / 2) - b)) + b))) + (1 / 2) by XCMPLX_1:75

.= ((1 / 2) * (sin ((1 * ((PI / 2) - b)) + b))) + (1 / 2) by XCMPLX_1:60, A7

.= 1 by SIN_COS:77 ;

hence ( ((PI / 2) - b) / a is Element of REAL & f . (((PI / 2) - b) / a) = 1 ) by XREAL_0:def 1; :: thesis: verum