set g = id ([#] REAL);

thus dom (id ([#] REAL)) = [#] REAL ; :: thesis: ( ( for x being Real holds (id ([#] REAL)) . x = x ) & ( for x being Real holds

( id ([#] REAL) is_differentiable_in x & diff ((id ([#] REAL)),x) = 1 ) ) )

thus for d being Real holds (id ([#] REAL)) . d = d by FUNCT_1:17, XREAL_0:def 1; :: thesis: for x being Real holds

( id ([#] REAL) is_differentiable_in x & diff ((id ([#] REAL)),x) = 1 )

A6: for d being Real st d in REAL holds

(id ([#] REAL)) . d = (1 * d) + 0 by FUNCT_1:17;

then A7: id ([#] REAL) is_differentiable_on dom (id ([#] REAL)) by FDIFF_1:23;

for x being Real holds

( id ([#] REAL) is_differentiable_in x & diff ((id ([#] REAL)),x) = 1 )

( id ([#] REAL) is_differentiable_in x & diff ((id ([#] REAL)),x) = 1 ) ; :: thesis: verum

thus dom (id ([#] REAL)) = [#] REAL ; :: thesis: ( ( for x being Real holds (id ([#] REAL)) . x = x ) & ( for x being Real holds

( id ([#] REAL) is_differentiable_in x & diff ((id ([#] REAL)),x) = 1 ) ) )

thus for d being Real holds (id ([#] REAL)) . d = d by FUNCT_1:17, XREAL_0:def 1; :: thesis: for x being Real holds

( id ([#] REAL) is_differentiable_in x & diff ((id ([#] REAL)),x) = 1 )

A6: for d being Real st d in REAL holds

(id ([#] REAL)) . d = (1 * d) + 0 by FUNCT_1:17;

then A7: id ([#] REAL) is_differentiable_on dom (id ([#] REAL)) by FDIFF_1:23;

for x being Real holds

( id ([#] REAL) is_differentiable_in x & diff ((id ([#] REAL)),x) = 1 )

proof

hence
for x being Real holds
let dd be Real; :: thesis: ( id ([#] REAL) is_differentiable_in dd & diff ((id ([#] REAL)),dd) = 1 )

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

id ([#] REAL) is_differentiable_in d by A7;

hence id ([#] REAL) is_differentiable_in dd ; :: thesis: diff ((id ([#] REAL)),dd) = 1

thus diff ((id ([#] REAL)),dd) = ((id ([#] REAL)) `| (dom (id ([#] REAL)))) . d by A7, FDIFF_1:def 7

.= 1 by A6, FDIFF_1:23 ; :: thesis: verum

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

id ([#] REAL) is_differentiable_in d by A7;

hence id ([#] REAL) is_differentiable_in dd ; :: thesis: diff ((id ([#] REAL)),dd) = 1

thus diff ((id ([#] REAL)),dd) = ((id ([#] REAL)) `| (dom (id ([#] REAL)))) . d by A7, FDIFF_1:def 7

.= 1 by A6, FDIFF_1:23 ; :: thesis: verum

( id ([#] REAL) is_differentiable_in x & diff ((id ([#] REAL)),x) = 1 ) ; :: thesis: verum