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 )

proof

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;

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