let b be Real; :: thesis: 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 ) ) ) ) )
defpred S₁[ set ] means $1 in REAL ;
deffunc H₁( Real) -> Element of REAL = b - $1;
consider g being PartFunc of REAL ,REAL such that
A1: for d being Element of REAL holds
( d in dom g iff S₁[d] ) and
A2: for d being Element of REAL st d in dom g holds
g /. d = H₁(d) from PARTFUN2:sch 2();
take g ; :: thesis: ( 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 ) ) ) ) )
A3: dom g = [#] REAL

proof

for x being set st x in REAL holds
x in dom g by A1;
then REAL c= dom g by TARSKI:def 3;
hence dom g = [#] REAL by XBOOLE_0:def 10; :: thesis: verum

end;

A4: for d being Element of REAL holds g . d = b - d

proof

let d be Element of REAL ; :: thesis: g . d = b - d
g /. d = b - d by A2, A3;
hence g . d = b - d by A3, PARTFUN1:def 8; :: thesis: verum

end;

A5: for d being Real st d in REAL holds
g . d = ((- 1) * d) + b

proof

let d be Real; :: thesis: ( d in REAL implies g . d = ((- 1) * d) + b )
assume d in REAL ; :: thesis: g . d = ((- 1) * d) + b
thus g . d = b - d by A4
.= ((- 1) * d) + b ; :: thesis: verum

end;

then A6: ( g is_differentiable_on dom g & ( for x being Real st x in dom g holds
(g `| (dom g)) . x = - 1 ) ) by A3, FDIFF_1:31;
for x being Real holds
( g is_differentiable_in x & diff g,x = - 1 )

proof

let d be Real; :: thesis: ( g is_differentiable_in d & diff g,d = - 1 )
thus g is_differentiable_in d by A3, A6, FDIFF_1:16; :: thesis: diff g,d = - 1
thus diff g,d = (g `| (dom g)) . d by A3, A6, FDIFF_1:def 8
.= - 1 by A3, A5, FDIFF_1:31 ; :: thesis: verum

end;

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, A4; :: thesis: verum