defpred S_{1}[ 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_{1}( 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_{1}[d] )
and

A2: for d being Element of REAL st d in dom g holds

g /. d = H_{1}(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

g . d = ((- 1) * d) + b

for x being Real holds

( g is_differentiable_in x & diff (g,x) = - 1 )

( 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

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

consider g being PartFunc of REAL,REAL such that

A1: for d being Element of REAL holds

( d in dom g iff S

A2: for d being Element of REAL st d in dom g holds

g /. d = H

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

A6:
for d being Real st d in REAL holds
let d be Real; :: thesis: g . d = b - d

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

g /. d = H_{1}(d)
by A2, A4;

hence g . d = b - d by A4, PARTFUN1:def 6; :: thesis: verum

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

g /. d = H

hence g . d = b - d by A4, PARTFUN1:def 6; :: thesis: verum

g . d = ((- 1) * d) + b

proof

then A7:
g is_differentiable_on dom g
by A4, FDIFF_1:23;
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;assume d in REAL ; :: thesis: g . d = ((- 1) * d) + b

thus g . d = b - d by A5

.= ((- 1) * d) + b ; :: thesis: verum

for x being Real holds

( g is_differentiable_in x & diff (g,x) = - 1 )

proof

hence
( dom g = [#] REAL & ( for x being Real holds
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;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

( 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