let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { f where f is Function of REAL,REAL : ex a, b being Real st

for th being Real holds f . th = ((1 / 2) * (sin ((a * th) + b))) + (1 / 2) } or x in Membership_Funcs REAL )

assume x in { f where f is Function of REAL,REAL : ex a, b being Real st

for th being Real holds f . th = ((1 / 2) * (sin ((a * th) + b))) + (1 / 2) } ; :: thesis: x in Membership_Funcs REAL

then consider f being Function of REAL,REAL such that

A1: x = f and

A2: ex a, b being Real st

for th being Real holds f . th = ((1 / 2) * (sin ((a * th) + b))) + (1 / 2) ;

rng f c= [.0,1.]

hence x in Membership_Funcs REAL by Def1, A1; :: thesis: verum

for th being Real holds f . th = ((1 / 2) * (sin ((a * th) + b))) + (1 / 2) } or x in Membership_Funcs REAL )

assume x in { f where f is Function of REAL,REAL : ex a, b being Real st

for th being Real holds f . th = ((1 / 2) * (sin ((a * th) + b))) + (1 / 2) } ; :: thesis: x in Membership_Funcs REAL

then consider f being Function of REAL,REAL such that

A1: x = f and

A2: ex a, b being Real st

for th being Real holds f . th = ((1 / 2) * (sin ((a * th) + b))) + (1 / 2) ;

rng f c= [.0,1.]

proof

then
f is [.0,1.] -valued
;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in [.0,1.] )

assume y in rng f ; :: thesis: y in [.0,1.]

then consider th being object such that

B2: th in REAL and

B3: y = f . th by FUNCT_2:11;

reconsider th = th as Real by B2;

consider a, b being Real such that

B1: for th0 being Real holds f . th0 = ((1 / 2) * (sin ((a * th0) + b))) + (1 / 2) by A2;

|.(sin ((a * th) + b)).| <= 1 by SIN_COS:27;

then ( - 1 <= sin ((a * th) + b) & sin ((a * th) + b) <= 1 ) by ABSVALUE:5;

then ( (1 / 2) * (- 1) <= (1 / 2) * (sin ((a * th) + b)) & (1 / 2) * (sin ((a * th) + b)) <= (1 / 2) * 1 ) by XREAL_1:64;

then B4: ( (- (1 / 2)) + (1 / 2) <= (((sin ((a * th) + b)) * 1) / 2) + (1 / 2) & ((1 / 2) * (sin ((a * th) + b))) + (1 / 2) <= (1 / 2) + (1 / 2) ) by XREAL_1:7;

y = ((1 / 2) * (sin ((a * th) + b))) + (1 / 2) by B1, B3;

hence y in [.0,1.] by B4; :: thesis: verum

end;assume y in rng f ; :: thesis: y in [.0,1.]

then consider th being object such that

B2: th in REAL and

B3: y = f . th by FUNCT_2:11;

reconsider th = th as Real by B2;

consider a, b being Real such that

B1: for th0 being Real holds f . th0 = ((1 / 2) * (sin ((a * th0) + b))) + (1 / 2) by A2;

|.(sin ((a * th) + b)).| <= 1 by SIN_COS:27;

then ( - 1 <= sin ((a * th) + b) & sin ((a * th) + b) <= 1 ) by ABSVALUE:5;

then ( (1 / 2) * (- 1) <= (1 / 2) * (sin ((a * th) + b)) & (1 / 2) * (sin ((a * th) + b)) <= (1 / 2) * 1 ) by XREAL_1:64;

then B4: ( (- (1 / 2)) + (1 / 2) <= (((sin ((a * th) + b)) * 1) / 2) + (1 / 2) & ((1 / 2) * (sin ((a * th) + b))) + (1 / 2) <= (1 / 2) + (1 / 2) ) by XREAL_1:7;

y = ((1 / 2) * (sin ((a * th) + b))) + (1 / 2) by B1, B3;

hence y in [.0,1.] by B4; :: thesis: verum

hence x in Membership_Funcs REAL by Def1, A1; :: thesis: verum