let g be object ; :: according to TARSKI:def 3 :: thesis: ( not g in { f where f is Function of REAL,REAL, a, b, c, d is Real : for x being Real holds f . x = max (0,(min (1,((c * (sin ((a * x) + b))) + d)))) } or g in { f where f, g is Function of REAL,REAL : for x being Real holds f . x = max (0,(min (1,(g . x)))) } )
assume g in { f where f is Function of REAL,REAL, a, b, c, d is Real : for x being Real holds f . x = max (0,(min (1,((c * (sin ((a * x) + b))) + d)))) } ; :: thesis: g in { f where f, g is Function of REAL,REAL : for x being Real holds f . x = max (0,(min (1,(g . x)))) }
then consider f being Function of REAL,REAL, a, b, c, d being Real such that
A1: f = g and
A2: for x being Real holds f . x = max (0,(min (1,((c * (sin ((a * x) + b))) + d)))) ;
ex g being Function of REAL,REAL st
for x being Real holds g . x = (c * (sin ((a * x) + b))) + d

proof

deffunc H₁( Element of REAL ) -> Element of REAL = In (((c * (sin ((a * $1) + b))) + d),REAL);
ex f being Function of REAL,REAL st
for x being Element of REAL holds f . x = H₁(x) from FUNCT_2:sch 4();
then consider f being Function of REAL,REAL such that
A1: for x being Element of REAL holds f . x = H₁(x) ;
take f ; :: thesis: for x being Real holds f . x = (c * (sin ((a * x) + b))) + d
for x being Real holds f . x = (c * (sin ((a * x) + b))) + d

proof

let x be Real; :: thesis: f . x = (c * (sin ((a * x) + b))) + d
reconsider x = x as Element of REAL by XREAL_0:def 1;
f . x = H₁(x) by A1;
hence f . x = (c * (sin ((a * x) + b))) + d ; :: thesis: verum

end;

hence for x being Real holds f . x = (c * (sin ((a * x) + b))) + d ; :: thesis: verum

end;

then consider g being Function of REAL,REAL such that
A4: for x being Real holds g . x = (c * (sin ((a * x) + b))) + d ;
for x being Real holds f . x = max (0,(min (1,(g . x))))

proof

let x be Real; :: thesis: f . x = max (0,(min (1,(g . x))))
f . x = max (0,(min (1,((c * (sin ((a * x) + b))) + d)))) by A2
.= max (0,(min (1,(g . x)))) by A4 ;
hence f . x = max (0,(min (1,(g . x)))) ; :: thesis: verum

end;

hence g in { f where f, g is Function of REAL,REAL : for x being Real holds f . x = max (0,(min (1,(g . x)))) } by A1; :: thesis: verum