let x be object ; TARSKI:def 3 ( 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))) }
; 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 ;
TARSKI:def 3 ( not y in rng f or y in [.0,1.] )
assume
y in rng f
;
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;
verum
end;
then
f is [.0,1.] -valued
;
hence
x in Membership_Funcs REAL
by Def1, A1; verum