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 * (arctan ((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 * (arctan ((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 * (arctan ((a * x) + b))) + d)))) ;

ex g being Function of REAL,REAL st

for x being Real holds g . x = (c * (arctan ((a * x) + b))) + d

A4: for x being Real holds g . x = (c * (arctan ((a * x) + b))) + d ;

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 * (arctan ((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 * (arctan ((a * x) + b))) + d)))) ;

ex g being Function of REAL,REAL st

for x being Real holds g . x = (c * (arctan ((a * x) + b))) + d

proof

then consider g being Function of REAL,REAL such that
deffunc H_{1}( Element of REAL ) -> Element of REAL = In (((c * (arctan ((a * $1) + b))) + d),REAL);

ex f being Function of REAL,REAL st

for x being Element of REAL holds f . x = H_{1}(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_{1}(x)
;

take f ; :: thesis: for x being Real holds f . x = (c * (arctan ((a * x) + b))) + d

for x being Real holds f . x = (c * (arctan ((a * x) + b))) + d

end;ex f being Function of REAL,REAL st

for x being Element of REAL holds f . x = H

then consider f being Function of REAL,REAL such that

A1: for x being Element of REAL holds f . x = H

take f ; :: thesis: for x being Real holds f . x = (c * (arctan ((a * x) + b))) + d

for x being Real holds f . x = (c * (arctan ((a * x) + b))) + d

proof

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

reconsider x = x as Element of REAL by XREAL_0:def 1;

f . x = H_{1}(x)
by A1;

hence f . x = (c * (arctan ((a * x) + b))) + d ; :: thesis: verum

end;reconsider x = x as Element of REAL by XREAL_0:def 1;

f . x = H

hence f . x = (c * (arctan ((a * x) + b))) + d ; :: thesis: verum

A4: for x being Real holds g . x = (c * (arctan ((a * x) + b))) + d ;

for x being Real holds f . x = max (0,(min (1,(g . x))))

proof

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
let x be Real; :: thesis: f . x = max (0,(min (1,(g . x))))

f . x = max (0,(min (1,((c * (arctan ((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;f . x = max (0,(min (1,((c * (arctan ((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