let f be FuzzySet of REAL; :: thesis: for a, b being Real st a <> 0 & ( for th being Real holds f . th = ((1 / 2) * (cos ((a * th) + b))) + (1 / 2) ) holds

f is normalized

let a, b be Real; :: thesis: ( a <> 0 & ( for th being Real holds f . th = ((1 / 2) * (cos ((a * th) + b))) + (1 / 2) ) implies f is normalized )

assume A1: a <> 0 ; :: thesis: ( ex th being Real st not f . th = ((1 / 2) * (cos ((a * th) + b))) + (1 / 2) or f is normalized )

assume A2: for th being Real holds f . th = ((1 / 2) * (cos ((a * th) + b))) + (1 / 2) ; :: thesis: f is normalized

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

f is normalized

let a, b be Real; :: thesis: ( a <> 0 & ( for th being Real holds f . th = ((1 / 2) * (cos ((a * th) + b))) + (1 / 2) ) implies f is normalized )

assume A1: a <> 0 ; :: thesis: ( ex th being Real st not f . th = ((1 / 2) * (cos ((a * th) + b))) + (1 / 2) or f is normalized )

assume A2: for th being Real holds f . th = ((1 / 2) * (cos ((a * th) + b))) + (1 / 2) ; :: thesis: f is normalized

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

proof

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

f . ((- b) / a) = ((1 / 2) * (cos ((a * ((- b) / a)) + b))) + (1 / 2) by A2

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

.= ((1 / 2) * (cos ((1 * (- b)) + b))) + (1 / 2) by XCMPLX_1:60, A1

.= 1 by SIN_COS:31 ;

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

end;f . ((- b) / a) = ((1 / 2) * (cos ((a * ((- b) / a)) + b))) + (1 / 2) by A2

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

.= ((1 / 2) * (cos ((1 * (- b)) + b))) + (1 / 2) by XCMPLX_1:60, A1

.= 1 by SIN_COS:31 ;

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