defpred S₁[ set ] means $1 in REAL ;
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 ) ) ) ) )
deffunc H₁( 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 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 ) ) ) ) )
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

proof

let d be Real; :: thesis: g . d = b - d
reconsider d = d as Element of REAL by XREAL_0:def 1;
g /. d = H₁(d) by A2, A4;
hence g . d = b - d by A4, PARTFUN1:def 6; :: thesis: verum

end;

A6: 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 A5
.= ((- 1) * d) + b ; :: thesis: verum

end;

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 )

proof

let dd be Real; :: thesis: ( g is_differentiable_in dd & diff (g,dd) = - 1 )
reconsider d = dd as Element of REAL by XREAL_0:def 1;
g is_differentiable_in d by A4, A7, FDIFF_1:9;
hence g is_differentiable_in dd ; :: thesis: diff (g,dd) = - 1
thus diff (g,dd) = (g `| (dom g)) . d by A4, A7, FDIFF_1:def 7
.= - 1 by A4, A6, FDIFF_1:23 ; :: 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, A5, XBOOLE_0:def 10; :: thesis: verum