let a be Real; :: thesis: for g being Function of REAL,REAL st ( for x being Real holds g . x = x - a ) holds
for x being Real holds
( g is_differentiable_in x & diff (g,x) = 1 )
let g be Function of REAL,REAL; :: thesis: ( ( for x being Real holds g . x = x - a ) implies for x being Real holds
( g is_differentiable_in x & diff (g,x) = 1 ) )
A1: dom g = [#] REAL by FUNCT_2:def 1;
assume A2: for x being Real holds g . x = x - a ; :: thesis: for x being Real holds
( g is_differentiable_in x & diff (g,x) = 1 )
A3: for d being Real st d in [#] REAL holds
g . d = (1 * d) + (- (1 * a))

proof

let d be Real; :: thesis: ( d in [#] REAL implies g . d = (1 * d) + (- (1 * a)) )
assume d in [#] REAL ; :: thesis: g . d = (1 * d) + (- (1 * a))
thus g . d = d - a by A2
.= (1 * d) + (- (1 * a)) ; :: thesis: verum

end;

then A4: g is_differentiable_on dom g by A1, FDIFF_1:23;
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 A1, A4, XREAL_0:def 1; :: thesis: diff (g,d) = 1
d in REAL by XREAL_0:def 1;
hence diff (g,d) = (g `| (dom g)) . d by A1, A4, FDIFF_1:def 7
.= 1 by A1, A3, FDIFF_1:23, XREAL_0:def 1 ;
:: thesis: verum

end;

hence for x being Real holds
( g is_differentiable_in x & diff (g,x) = 1 ) ; :: thesis: verum