let a, b be Real; :: thesis: for f being FuzzySet of REAL st a <> 0 & ( for th being Real holds f . th = ((1 / 2) * (sin ((a * th) + b))) + (1 / 2) ) holds
f is normalized
let f be FuzzySet of REAL; :: thesis: ( a <> 0 & ( for th being Real holds f . th = ((1 / 2) * (sin ((a * th) + b))) + (1 / 2) ) implies f is normalized )
assume A1: a <> 0 ; :: thesis: ( ex th being Real st not f . th = ((1 / 2) * (sin ((a * th) + b))) + (1 / 2) or f is normalized )
assume A2: for th being Real holds f . th = ((1 / 2) * (sin ((a * th) + b))) + (1 / 2) ; :: thesis: f is normalized
ex x being Element of REAL st f . x = 1
proof
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 A2
.= ((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, A1
.= 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;
hence f is normalized ; :: thesis: verum