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 ;
f is_differentiable_on Z by A1, Th17;
hence f is differentiable ; :: thesis: verum