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 = max (0,(sin ((a * th) + b))) } 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 = max (0,(sin ((a * th) + b))) } ; :: 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 = max (0,(sin ((a * th) + b))) ;
rng f c= [.0,1.]

proof

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 = max (0,(sin ((a * th0) + b))) by A2;
sin ((a * th) + b) <= 1 by SIN_COS6:4;
then B4: ( 0 <= max (0,(sin ((a * th) + b))) & max (0,(sin ((a * th) + b))) <= 1 ) by XXREAL_0:25, XXREAL_0:28;
y = max (0,(sin ((a * th) + b))) by B1, B3;
hence y in [.0,1.] by B4; :: thesis: verum

end;

then f is [.0,1.] -valued ;
hence x in Membership_Funcs REAL by Def1, A1; :: thesis: verum