defpred S1[ set ] means $1 in REAL ;
let b be Real; ex g being PartFunc of REAL,REAL st
( dom g = [#] REAL & ( for x being Real holds
( g . x = b - x & ( for x being Real holds
( g is_differentiable_in x & diff (g,x) = - 1 ) ) ) ) )
deffunc H1( Real) -> Element of REAL = In ((b - $1),REAL);
consider g being PartFunc of REAL,REAL such that
A1:
for d being Element of REAL holds
( d in dom g iff S1[d] )
and
A2:
for d being Element of REAL st d in dom g holds
g /. d = H1(d)
from PARTFUN2:sch 2();
take
g
; ( dom g = [#] REAL & ( for x being Real holds
( g . x = b - x & ( for x being Real holds
( g is_differentiable_in x & diff (g,x) = - 1 ) ) ) ) )
for x being object st x in REAL holds
x in dom g
by A1;
then A3:
REAL c= dom g
by TARSKI:def 3;
then A4:
dom g = [#] REAL
by XBOOLE_0:def 10;
A5:
for d being Real holds g . d = b - d
A6:
for d being Real st d in REAL holds
g . d = ((- 1) * d) + b
then A7:
g is_differentiable_on dom g
by A4, FDIFF_1:23;
for x being Real holds
( g is_differentiable_in x & diff (g,x) = - 1 )
hence
( dom g = [#] REAL & ( for x being Real holds
( g . x = b - x & ( for x being Real holds
( g is_differentiable_in x & diff (g,x) = - 1 ) ) ) ) )
by A3, A5, XBOOLE_0:def 10; verum