reconsider f = id REAL as Function of REAL ,REAL ;
take f ; :: thesis: f is differentiable
reconsider Z = REAL as open Subset of REAL by Th4;
A1: Z = dom f by FUNCT_2:def 1;
then f | Z = id Z by RELAT_1:97;
then f is_differentiable_on Z by A1, Th25;
hence f is differentiable by DifDef, A1; :: thesis: verum