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